[Merged by Bors] - feat: generalize Topology/OpenPartialHomeomorph/Basic to PartialHomeomorph#41045
Closed
scholzhannah wants to merge 8 commits into
Closed
[Merged by Bors] - feat: generalize Topology/OpenPartialHomeomorph/Basic to PartialHomeomorph#41045scholzhannah wants to merge 8 commits into
Topology/OpenPartialHomeomorph/Basic to PartialHomeomorph#41045scholzhannah wants to merge 8 commits into
Conversation
PR summary 19350313ddImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5015 | 1 | exposed public sections |
Current commit 19350313dd
Reference commit c732b96d05
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
grunweg
reviewed
Jun 29, 2026
grunweg
left a comment
grunweg
left a comment
Contributor
There was a problem hiding this comment.
Just today, we were looking at making manifolds nicer to use and stumbled on your PR --- which proved just the lemma I wanted. In other words, thanks a lot for doing this, it's great. I hope to review this soon (but given that so many things in Paris cry for being discussed in person, this might take until next week).
I just have one comment for now.
grunweg
reviewed
Jul 10, 2026
grunweg
left a comment
grunweg
left a comment
Contributor
There was a problem hiding this comment.
Not in this PR: the module doc-string for OpenPartialHomeomorph/Basic.lean should be slightly updated now, to say something like
"Topology.IsOpenEmbedding.toOpenPartialHomeomorph: construct an open partial homeomorphism from an open embedding"
grunweg
reviewed
Jul 10, 2026
grunweg
left a comment
grunweg
left a comment
Contributor
There was a problem hiding this comment.
Thanks for doing this! I only have minor comments.
Can you also mention IsEmbedding.toPartialHomeomorph is the module doc-string?
grunweg
added
the
awaiting-author
scholzhannah
added
t-topology
grunweg
reviewed
Jul 17, 2026
| rfl | ||
|
|
||
| lemma toEquiv_symm_eq_codRestrict_restrict : | ||
| e.toEquiv.symm = codRestrict (e.target.restrict e.invFun) e.source (by simp) := by |
Contributor
There was a problem hiding this comment.
Should this use e.symm instead?
Collaborator
Author
There was a problem hiding this comment.
That has a different type. I could do e.symm.toEquiv but I want this lemma to show something about PartialEquiv.toEquiv, so I don't think that is sensible. Or do you mean something else?
Contributor
There was a problem hiding this comment.
Ah, that's fair. In this case, let's merge as-is.
Contributor
|
Thanks - one last comment! |
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Jul 17, 2026
As requested in a PR review [here](#41045 (comment)). I also included a correction of a different docstring.
Contributor
|
Can you fix the deprecation warnings? It seems there are still some. (Then, I'll merge this PR.) |
Contributor
|
One line length warning, then you should be good to go. |
mathlib-bors
Bot
added
the
delegated
Contributor
|
✌️ scholzhannah can now approve this pull request until 2026-08-03 12:11 UTC (in 2 weeks). To approve and merge, reply with
|
Collaborator
Author
|
Thank you for your patience! bors r+ |
mathlib-bors
Bot
added
the
bors-staging
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
Topology/OpenPartialHomeomorph/Basic to PartialHomeomorphTopology/OpenPartialHomeomorph/Basic to PartialHomeomorph
mathlib-bors
Bot
removed
the
delegated
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is a continuation of #39084.