-
Notifications
You must be signed in to change notification settings - Fork 298
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(algebra/order/nonneg): properties about the nonnegative cone #9598
Conversation
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
/-- If `Sup ∅ ≤ a` then `{x : α // a ≤ x}` is a `conditionally_complete_linear_order_bot`. -/ | ||
@[reducible] | ||
protected noncomputable def conditionally_complete_linear_order_bot | ||
[conditionally_complete_linear_order α] {a : α} (h : Sup ∅ ≤ a) : | ||
conditionally_complete_linear_order_bot {x : α // a ≤ x} := | ||
{ cSup_empty := (function.funext_iff.1 | ||
(@subset_Sup_def α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩) ∅).trans $ subtype.eq $ | ||
by { cases h.lt_or_eq with h2 h2, { simp [h2.not_le] }, simp [h2] }, | ||
..nonneg.order_bot, | ||
.. @ord_connected_subset_conditionally_complete_linear_order α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ } |
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 this be defined on set.IcI
like the semilattice_inf_bot
isntance above is?
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 could, but order.lattice_intervals
currently doesn't import order.conditionally_complete_lattice
...
bors merge |
) * Provide various classes on the type `{x : α // 0 ≤ x}` where `α` has some order (and algebraic) structure. * Use this to automatically derive the classes on `nnreal`. * We currently do not yet define `conditionally_complete_linear_order_bot nnreal` using nonneg, since that causes some errors (I think Lean then thinks that there are two orders that are not definitionally equal (unfolding only instances)). * We leave a bunch of `example` lines in `nnreal` to show that `nnreal` has all the old classes. These could also be removed, if desired. * We currently only give some instances and simp/norm_cast lemmas. This could be expanded in the future. Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu> Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
{x : α // 0 ≤ x}
whereα
has some order (and algebraic) structure.nnreal
.conditionally_complete_linear_order_bot nnreal
using nonneg, since that causes some errors (I think Lean then thinks that there are two orders that are not definitionally equal (unfolding only instances)).example
lines innnreal
to show thatnnreal
has all the old classes. These could also be removed, if desired.