Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: three tiny homeomorph lemmas #9166

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat: three tiny homeomorph lemmas #9166

wants to merge 3 commits into from

Conversation

PatrickMassot
Copy link
Member

Requested on Zulip.

Open in Gitpod

@PatrickMassot PatrickMassot added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters labels Dec 20, 2023
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 21, 2023
@PatrickMassot @Ruben-VandeVelde
Update Mathlib/Topology/Algebra/Group/Basic.lean
b50dce8 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@PatrickMassot PatrickMassot added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 14, 2024
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jan 14, 2024
View reviewed changes
Mathlib/Topology/Algebra/Group/Basic.lean Outdated
@@ -334,6 +334,10 @@ protected def Homeomorph.inv (G : Type*) [TopologicalSpace G] [InvolutiveInv G]
#align homeomorph.inv Homeomorph.inv
#align homeomorph.neg Homeomorph.neg

@[to_additive (attr := simp)]
lemma Homeomorph.coe_inv {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G]
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
lemma Homeomorph.coe_inv {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G]
lemma Homeomorph.coe_inv {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

@ADedecker
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 15, 2024
@PatrickMassot
feat: three tiny homeomorph lemmas (#9166)
b1ff86d
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: three tiny homeomorph lemmas [Merged by Bors] - feat: three tiny homeomorph lemmas Jan 15, 2024
@mathlib-bors mathlib-bors bot closed this Jan 15, 2024
@mathlib-bors mathlib-bors bot deleted the pm_homeo_lemmas branch January 15, 2024 17:33
linesthatinterlace pushed a commit that referenced this pull request Jan 16, 2024
@PatrickMassot @linesthatinterlace
feat: three tiny homeomorph lemmas (#9166)
bb58ad1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth left review comments

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.

None yet
5 participants
@PatrickMassot @ADedecker @Ruben-VandeVelde @MichaelStollBayreuth @sgouezel