Skip to content

[Merged by Bors] - chore: last LocalHomeomorph -> PartialHomeomorph renames#9238

Closed
grunweg wants to merge 5 commits intomasterfrom
MR-localhomeo-rename
Closed

[Merged by Bors] - chore: last LocalHomeomorph -> PartialHomeomorph renames#9238
grunweg wants to merge 5 commits intomasterfrom
MR-localhomeo-rename

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Dec 23, 2023 •
edited
Loading

Follow-up to #8982; a few lemma names were still wrong.

  • I'm open to dropping or paring down the second commit.

@grunweg
Some PartialHomeomorph renames I missed.
04772e8
@grunweg
Rename FiberwiseLinear.localHomeomorph to partialHomeomorph,
3c6055b 
as it is all about a partial homeomorphism. The same applies to all
doc comments in this file.

Fix line length. Not the happiest with my formatting.
@grunweg grunweg added awaiting-review t-topology Topological spaces, uniform spaces, metric spaces, filters labels Dec 23, 2023
@grunweg grunweg mentioned this pull request Dec 23, 2023
Closed
@grunweg grunweg force-pushed the MR-localhomeo-rename branch from 2950c67 to 3c6055b Compare December 23, 2023 17:48
@grunweg grunweg mentioned this pull request Dec 23, 2023
Closed
4 tasks
mathlib-bors bot pushed a commit that referenced this pull request Dec 26, 2023
@grunweg
chore: audit remaining uses of "local homeomorphism" in comments (#9245)
a76fbc3 
Almost all of them should speak about partial homeomorphisms instead.
In two cases, I decided removing the "local" was clearer than adding "partial".

Follow-up to #8982; complements #9238.
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 27, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 29, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 5, 2024
@grunweg grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 7, 2024
jcommelin
jcommelin approved these changes Jan 8, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 8, 2024
@grunweg @winstonyin
chore: last LocalHomeomorph -> PartialHomeomorph renames (#9238)
9df25a9 
Follow-up to #8982; a few lemma names were still wrong.



Co-authored-by: Winston Yin <winstonyin@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: last LocalHomeomorph -> PartialHomeomorph renames [Merged by Bors] - chore: last LocalHomeomorph -> PartialHomeomorph renames Jan 8, 2024
@mathlib-bors mathlib-bors bot closed this Jan 8, 2024
@mathlib-bors mathlib-bors bot deleted the MR-localhomeo-rename branch January 8, 2024 14:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

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

@grunweg @jcommelin @winstonyin