Skip to content

chore: rename some OpenPartialHomeomorph declarations#39565

Open
scholzhannah wants to merge 4 commits into
leanprover-community:masterfrom
scholzhannah:scholzhannah/openPartialHomeomorphRenames
Open

chore: rename some OpenPartialHomeomorph declarations#39565
scholzhannah wants to merge 4 commits into
leanprover-community:masterfrom
scholzhannah:scholzhannah/openPartialHomeomorphRenames

Conversation

@scholzhannah
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah commented May 19, 2026 •
edited
Loading

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
Copy link
Copy Markdown

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

PR summary 08b3d12774

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_toPartialEquiv
+ coe_toPartialEquiv_symm
+ replacePartialEquiv
++ 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
Open
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
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

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

@[deprecated (since := "2026-05-19")] alias replaceEquiv := replacePartialEquiv

theorem replaceEquiv_eq_self (e' : PartialEquiv X Y)
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 19, 2026

Choose a reason for hiding this comment

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

Can you update this lemma also (and perhaps any similar ones below)?

Comment thread Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
@[simp, mfld_simps]
theorem mk_coe (e : PartialEquiv X Y) (a b c d) :
(OpenPartialHomeomorph.mk e a b c d : X → Y) = e :=
theorem mk_coe (e : PartialEquiv X Y) (h1 h2 h3 h4) :
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 19, 2026

Choose a reason for hiding this comment

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

optional: use unicode superscript, i.e. h₁ etc.

Copy link
Copy Markdown
Collaborator

@themathqueen themathqueen May 19, 2026

Choose a reason for hiding this comment

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

Also, shouldn't this be called coe_mk?

@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
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

awaiting-author A reviewer has asked the author a question or requested changes.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@scholzhannah @grunweg @themathqueen