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.
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
[Merged by Bors] - feat(topology/algebra/group): added (right/left)_coset_(open/closed) #11876
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
src/topology/algebra/group.lean
Outdated
@@ -67,10 +67,18 @@ by { ext, refl } | |||
lemma is_open_map_mul_left (a : G) : is_open_map (λ x, a * x) := | |||
(homeomorph.mul_left a).is_open_map | |||
|
|||
@[to_additive is_open.left_add_coset] | |||
lemma is_open.left_coset {U : set G} (x : G) (h : is_open U) : is_open (left_coset x U) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think you need to swap the order of the arguments for dot notation to work:
lemma is_open.left_coset {U : set G} (x : G) (h : is_open U) : is_open (left_coset x U) := | |
lemma is_open.left_coset {U : set G} (h : is_open U) (x : G) : is_open (left_coset x U) := |
and likewise with the other lemmas below
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Dot notation doesn't care about the argument order here, the original was fine
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it does matter in some situations. For example the following:
example {U : set G} (h : is_open U) : ∀ x, is_open (left_coset x U) := h.left_coset
only works when is_open.left_coset
is defined with x
following h
.
I admit that the ordering does not matter for something of the form:
example {U : set G} (h : is_open U) (x : G) : is_open (left_coset x U) := h.left_coset x
which is likely to be the more typical usage.
I'm happy to be corrected if there's more to it!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we should swap the argument orders as indicated and then this will be good to go.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors d+
✌️ Sebastian-Monnet can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…11876) Added lemmas saying that, in a topological group, cosets of an open (resp. closed) set are open (resp. closed).
Pull request successfully merged into master. Build succeeded: |
Added lemmas saying that, in a topological group, cosets of an open (resp. closed) set are open (resp. closed).