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: add basic API lemmas for BddAbove (range f)
and BddBelow (range f)
#9472
Conversation
Mathlib/Order/Bounds/Basic.lean
Outdated
rw [bddBelow_def] at hf ⊢ | ||
obtain ⟨C, hC⟩ := hf | ||
refine ⟨g C, fun y hy => ?_⟩ | ||
rw [Set.mem_range] at hy | ||
obtain ⟨y', hy'⟩ := hy | ||
calc y = g (f y') := hy'.symm | ||
_ ≥ g C := hg <| hC (f y') <| Set.mem_range_self _ |
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.
Can't this also be golfed using OrderDual
?
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.
Not easily. We need to take the dual of both β
and γ
, and I think the Monotone g
hypothesis needs to be adapted. Maybe it's possible but it's easier to copy/paste.
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.
Could you also replace the uses of Set.range
by range
where the namespaces are already open?
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Thanks 🎉 bors merge |
…nge f)` (#9472) This PR adds some basic API lemmas for `BddAbove (range f)` (resp `BddBelow`). This is a ubiquitous side condition when working with `iInf`/`iSup` in conditionally complete lattices, so I think it's worth having. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
bors r- Sorry, I thought you were done... bors d+ |
✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
…nge f)` (#9472) This PR adds some basic API lemmas for `BddAbove (range f)` (resp `BddBelow`). This is a ubiquitous side condition when working with `iInf`/`iSup` in conditionally complete lattices, so I think it's worth having. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
BddAbove (range f)
and BddBelow (range f)
BddAbove (range f)
and BddBelow (range f)
…nge f)` (#9472) This PR adds some basic API lemmas for `BddAbove (range f)` (resp `BddBelow`). This is a ubiquitous side condition when working with `iInf`/`iSup` in conditionally complete lattices, so I think it's worth having. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
This PR adds some basic API lemmas for
BddAbove (range f)
(respBddBelow
). This is a ubiquitous side condition when working withiInf
/iSup
in conditionally complete lattices, so I think it's worth having.