Skip to content

feat(Topology): a coinducing map with connected fibers induces a homeomorphism on connected components#37515

Open
chrisflav wants to merge 5 commits intoleanprover-community:masterfrom
chrisflav:homeo-pi0-coinducing
Open

feat(Topology): a coinducing map with connected fibers induces a homeomorphism on connected components#37515
chrisflav wants to merge 5 commits intoleanprover-community:masterfrom
chrisflav:homeo-pi0-coinducing

Conversation

@chrisflav
Copy link
Copy Markdown
Member

@chrisflav chrisflav commented Apr 1, 2026

Open in Gitpod

@chrisflav chrisflav added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Apr 1, 2026
@chrisflav chrisflav mentioned this pull request Apr 1, 2026
Open
2 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 1, 2026 •
edited
Loading

PR summary 3bd2603b81

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Continuous.connectedComponentsMap_mk
+ Continuous.connectedComponentsMap_surjective
+ Topology.IsCoinducing.connectedComponentsEquiv
+ Topology.IsCoinducing.connectedComponentsEquiv_mk
+ Topology.IsCoinducing.connectedComponentsEquiv_symm_mk_apply
+ Topology.IsCoinducing.connectedComponentsMap
+ isOpenMap_of_injective

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

scholzhannah
scholzhannah approved these changes Apr 2, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your PR! I just have some minor style comments.

grunweg
grunweg reviewed Apr 2, 2026
View reviewed changes
Mathlib/Topology/Homeomorph/Lemmas.lean Outdated
Continuous.connectedComponentsMap_surjective _ fun y ↦ (hf' y).nonempty⟩
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
simp at h
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 2, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like a non-terminal simp to me. @adomani Do you have any idea why the flexible linter does not warn here?

Copy link
Copy Markdown
Member Author

@chrisflav chrisflav Apr 2, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is followed by a flexible tactic, is it not?

Copy link
Copy Markdown
Member Author

@chrisflav chrisflav Apr 2, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(in any case, I accepted Hannah's suggestion, so this potential issue does not exist anymore)

Re flexible: I also think simp at h; simp [h] is much better than the similar (but not applicable here) simpa using h, which the flexible linter happily accepts.

@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented Apr 2, 2026

Thanks for the review @scholzhannah!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

+1 more reviewer

@scholzhannah scholzhannah scholzhannah approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@j-loreaux j-loreaux

Labels

t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@chrisflav @grunweg @scholzhannah @j-loreaux