-
Notifications
You must be signed in to change notification settings - Fork 297
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/discrete_quotient): add two lemmas #8464
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, will let someone more familiar with this ping bors
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
src/topology/discrete_quotient.lean
Outdated
@[simp] lemma is_clopen_discrete [discrete_topology X] (x : set X) : is_clopen x := | ||
⟨is_open_discrete _, is_closed_discrete _⟩ |
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.
This lemma should go after is_closed_discrete
in topology/order.lean
.
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.
Ok, thanks, I'll move 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 don't know if is_clopen
is available yet there...
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.
Eric is probably right... If this is the case, I guess this lemma could go near where is_clopen
is defined.
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.
Should I put it in topology/subset_properties.lean
alongside other properties of clopen
sets?
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.
Yes, I think that's a reasonable place for 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.
Ok, done.
Looks good to me. I'll activate bors once the CI is happy. |
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
bors r+ |
Add lemmas `proj_bot_injective` and `proj_bot_bijective`, the former needed for the latter, and the latter needed in LTE. Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Add lemmas
proj_bot_injective
andproj_bot_bijective
, the former needed for the latter, and the latter needed in LTE.