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(order/galois_connection): formula for upper_bounds (l '' s)
#8478
Conversation
* upgrade `galois_connection.upper_bounds_l_image_subset` and `galois_connection.lower_bounds_u_image` to equalities; * prove `bdd_above (l '' s) ↔ bdd_above s` and `bdd_below (u '' s) ↔ bdd_below s`; * move `galois_connection.dual` to the top and use it in some proofs; * use `order_iso.to_galois_connection` to transfer some of these results to `order_iso`s; * rename `rel_iso.to_galois_insertion` to `order_iso.to_galois_insertion`.
src/order/galois_connection.lean
Outdated
@@ -67,6 +67,11 @@ lemma monotone_intro (hu : monotone u) (hl : monotone l) | |||
|
|||
include gc | |||
|
|||
protected lemma dual [pα : preorder α] [pβ : preorder β] | |||
{l : α → β} {u : β → α} (gc : galois_connection l u) : | |||
@galois_connection (order_dual β) (order_dual α) _ _ u l := |
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.
Shouldn't l
and u
be composed with to_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.
I moved this lemma without touching the code. I mostly use order_dual
for @dual_lemma (order_dual α) _ _
proofs, so I don't care about to_dual
. Feel free to add it if you want to. I guess, something like
@galois_connection (order_dual β) (order_dual α) _ _ u l := | |
galois_connection (order_dual.to_dual ∘ u ∘ order_dual.of_dual) | |
(order_dual.to_dual ∘ l ∘ order_dual.of_dual) := |
should work.
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.
Oh, I missed that this lemma was moved. Yeah, that's basically what I was thinking . You'll need to import order.order_dual
, but that seems like a good change to make to me.
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.
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…8478) * upgrade `galois_connection.upper_bounds_l_image_subset` and `galois_connection.lower_bounds_u_image` to equalities; * prove `bdd_above (l '' s) ↔ bdd_above s` and `bdd_below (u '' s) ↔ bdd_below s`; * move `galois_connection.dual` to the top and use it in some proofs; * use `order_iso.to_galois_connection` to transfer some of these results to `order_iso`s; * rename `rel_iso.to_galois_insertion` to `order_iso.to_galois_insertion`.
Pull request successfully merged into master. Build succeeded: |
upper_bounds (l '' s)
upper_bounds (l '' s)
galois_connection.upper_bounds_l_image_subset
andgalois_connection.lower_bounds_u_image
to equalities;bdd_above (l '' s) ↔ bdd_above s
andbdd_below (u '' s) ↔ bdd_below s
;galois_connection.dual
to the top and use it in some proofs;order_iso.to_galois_connection
to transfer some of theseresults to
order_iso
s;rel_iso.to_galois_insertion
toorder_iso.to_galois_insertion
.