-
Notifications
You must be signed in to change notification settings - Fork 299
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] - chore(topology/order): relate Sup and Inf of topologies to generate_from
#9045
Conversation
src/topology/order.lean
Outdated
@galois_insertion.u_le_u_iff _ _ _ _ _ | ||
(@partial_order.to_preorder _ | ||
(@semilattice_sup.to_partial_order _ | ||
(@lattice.to_semilattice_sup _ | ||
(@bounded_lattice.to_lattice _ | ||
(@complete_lattice.to_bounded_lattice _ tmp_complete_lattice))))) | ||
(gi_generate_from α) a b |
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.
@galois_insertion.u_le_u_iff _ _ _ _ _ | |
(@partial_order.to_preorder _ | |
(@semilattice_sup.to_partial_order _ | |
(@lattice.to_semilattice_sup _ | |
(@bounded_lattice.to_lattice _ | |
(@complete_lattice.to_bounded_lattice _ tmp_complete_lattice))))) | |
(gi_generate_from α) a b | |
@galois_insertion.u_le_u_iff _ (order_dual (topological_space α)) _ _ _ _ (gi_generate_from α) a b |
Hopefully the same works 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.
Thanks, yes! I've changed throughout. I'm suprised because order_dual (topological_space α)
actually carries the dual of the dual of tmp_order
, whereas the Galois insertion is stated for tmp_order
. I had assumed that an order was not defeq to its double dual.
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!
Thanks 🎉 bors merge |
…from` (#9045) Since there is a Galois insertion between `generate_from : set (set α) → topological_space α` and the "forgetful functor" `topological_space α → set (set α)`, all kinds of lemmas about the interaction of `generate_from` and the ordering on topologies automatically follow. But it is hard to use the Galois insertion lemmas directly, because the Galois insertion is actually provided for the dual order on topologies, which confuses Lean. Here we re-state most of the Galois insertion API in this special case. Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
generate_from
generate_from
Since there is a Galois insertion between
generate_from : set (set α) → topological_space α
and the "forgetful functor"topological_space α → set (set α)
, all kinds of lemmas about the interaction ofgenerate_from
and the ordering on topologies automatically follow. But it is hard to use the Galois insertion lemmas directly, because the Galois insertion is actually provided for the dual order on topologies, which confuses Lean. Here we re-state most of the Galois insertion API in this special case.