-
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] - fix(order/basic): fix subtype.linear_order
#15056
Conversation
src/order/basic.lean
Outdated
max := λ x y, ⟨max x y, max_rec' _ x.2 y.2⟩, | ||
min := λ x y, ⟨min x y, min_rec' _ x.2 y.2⟩, | ||
max_def := by { ext ⟨x, hx⟩ ⟨y, hy⟩, by_cases y ≤ x; simp [*, max_def, max_default] }, | ||
min_def := by { ext ⟨x, hx⟩ ⟨y, hy⟩, by_cases x ≤ y; simp [*, min_def, min_default] }, |
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.
Does min_rec'
work for this field?
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'm rewriting linear_order.lift
.
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.
What exactly is the idea here? I don't quite parse what's going on with has_sup
and has_inf
.
@@ -68,14 +65,6 @@ end | |||
|
|||
/- TODO: automatic construction of dual definitions / theorems -/ |
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 comment doesn't seem relevant here anymore.
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
…nity/mathlib into YK-linear-subtype
Currently, there is a diamond : |
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!
bors r+
This makes `subtype.lattice` definitionally equal to `linear_order.to_lattice`, after unfolding some (which?) semireducible definitions. * Rewrite `linear_order.lift` to allow custom `max` and `min` fields. Move the old definition to `linear_order.lift'`. * Use the new `linear_order.lift` to fix a non-defeq diamond on `subtype _`. * Use the new `linear_order.lift` in various `function.injective.linear_*` definitions.
Build failed (retrying...): |
This makes `subtype.lattice` definitionally equal to `linear_order.to_lattice`, after unfolding some (which?) semireducible definitions. * Rewrite `linear_order.lift` to allow custom `max` and `min` fields. Move the old definition to `linear_order.lift'`. * Use the new `linear_order.lift` to fix a non-defeq diamond on `subtype _`. * Use the new `linear_order.lift` in various `function.injective.linear_*` definitions.
Pull request successfully merged into master. Build succeeded: |
subtype.linear_order
subtype.linear_order
This makes
subtype.lattice
definitionally equal tolinear_order.to_lattice
, after unfolding some (which?) semireducible definitions.linear_order.lift
to allow custommax
andmin
fields. Move the old definition tolinear_order.lift'
.linear_order.lift
to fix a non-defeq diamond onsubtype _
.linear_order.lift
in variousfunction.injective.linear_*
definitions.