Skip to content

[Merged by Bors] - chore: rename some OpenPartialHomeomorph declarations#39565

Closed
scholzhannah wants to merge 9 commits into
leanprover-community:masterfrom
scholzhannah:scholzhannah/openPartialHomeomorphRenames
Closed

[Merged by Bors] - chore: rename some OpenPartialHomeomorph declarations#39565
scholzhannah wants to merge 9 commits into
leanprover-community:masterfrom
scholzhannah:scholzhannah/openPartialHomeomorphRenames

Conversation

@scholzhannah

@scholzhannah scholzhannah commented May 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

In the review of #39084, a few suggested renames relating to OpenPartialHomeomorph came up which I am doing in this PR.

Open in Gitpod

@github-actions

github-actions Bot commented May 19, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary ec66ed9183

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_mk
+ coe_mk_symm
+ coe_toPartialEquiv
+ coe_toPartialEquiv_symm
+ replacePartialEquiv
+ replacePartialEquiv_eq_self
++ mapsTo_symm
+-- symm_mapsTo

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@scholzhannah scholzhannah mentioned this pull request May 19, 2026
Closed
1 task
@scholzhannah
scholzhannah marked this pull request as ready for review May 19, 2026 09:45
grunweg
grunweg reviewed May 19, 2026
View reviewed changes

@grunweg grunweg left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks for splitting this out; I only have two minor comments.

Comment thread Mathlib/Topology/OpenPartialHomeomorph/Defs.lean Outdated
Comment thread Mathlib/Topology/OpenPartialHomeomorph/Defs.lean Outdated
@grunweg grunweg self-assigned this May 19, 2026
@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 19, 2026
@scholzhannah scholzhannah added t-topology Topological spaces, uniform spaces, metric spaces, filters and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 20, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 23, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented May 23, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

grunweg
grunweg reviewed May 26, 2026
View reviewed changes

@grunweg grunweg left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks! You have a merge conflict to fix, otherwise this is good to go!
bors d+

@mathlib-bors

mathlib-bors Bot commented May 26, 2026

Copy link
Copy Markdown
Contributor

✌️ scholzhannah can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 28, 2026
@grunweg

grunweg commented May 28, 2026

Copy link
Copy Markdown
Contributor

Thanks!
bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 28, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 28, 2026
@scholzhannah
chore: rename some OpenPartialHomeomorph declarations (#39565)
106cea4 
In the review of #39084, a few suggested renames relating to `OpenPartialHomeomorph` came up which I am doing in this PR.
@scholzhannah scholzhannah mentioned this pull request May 28, 2026
Closed
1 task
@scholzhannah

scholzhannah commented May 28, 2026

Copy link
Copy Markdown
Collaborator Author

I forgot to add a deprecation for OpenPartialHomeomorph.mapsTo_symm. I don't know what the procedure is when a PR has already been sent to bors so I created a separate PR #39968 .

@grunweg

grunweg commented May 28, 2026

Copy link
Copy Markdown
Contributor

Sorry, I had assumed the PR was ready to go. I delegated the follow-up PR.

@mathlib-bors

mathlib-bors Bot commented May 28, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: rename some OpenPartialHomeomorph declarations [Merged by Bors] - chore: rename some OpenPartialHomeomorph declarations May 28, 2026
@mathlib-bors mathlib-bors Bot closed this May 28, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 28, 2026
@scholzhannah @themathqueen
chore(OpenPartialHomeomorph): add missing deprecation (#39968)
ec33b54 
Add deprecation that I forgot in #39565.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026
@scholzhannah @grunweg
chore: rename some OpenPartialHomeomorph declarations (leanprover-com…
ecadea7 
…munity#39565)

In the review of leanprover-community#39084, a few suggested renames relating to `OpenPartialHomeomorph` came up which I am doing in this PR.
grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026
@scholzhannah @themathqueen @grunweg
chore(OpenPartialHomeomorph): add missing deprecation (leanprover-com…
a7d30c2 
…munity#39968)

Add deprecation that I forgot in leanprover-community#39565.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@scholzhannah @b-mehta
chore: rename some OpenPartialHomeomorph declarations (leanprover-com…
615b6e2 
…munity#39565)

In the review of leanprover-community#39084, a few suggested renames relating to `OpenPartialHomeomorph` came up which I am doing in this PR.
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@scholzhannah @themathqueen @b-mehta
chore(OpenPartialHomeomorph): add missing deprecation (leanprover-com…
70be6f6 
…munity#39968)

Add deprecation that I forgot in leanprover-community#39565.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@scholzhannah @Bergschaf
chore: rename some OpenPartialHomeomorph declarations (leanprover-com…
30cacfd 
…munity#39565)

In the review of leanprover-community#39084, a few suggested renames relating to `OpenPartialHomeomorph` came up which I am doing in this PR.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@scholzhannah @themathqueen @Bergschaf
chore(OpenPartialHomeomorph): add missing deprecation (leanprover-com…
53fd774 
…munity#39968)

Add deprecation that I forgot in leanprover-community#39565.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
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
@themathqueen themathqueen themathqueen left review comments

Assignees

@grunweg grunweg

Labels

ready-to-merge This PR has been sent to bors. 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.

3 participants

@scholzhannah @grunweg @themathqueen