Yury G. Kudryashov (Jun 30 2020 at 07:09):
If I have
[decidable_linear_order α], then I have two non-defeq
@min α _ and
@max (order_dual α) _. Most of the time it doesn't matter but sometimes this stops me from using the
:= @some_lemma (order_dual α) _ _ trick for a proof.
Kevin Buzzard (Jun 30 2020 at 07:24):
How is max defined on order_dual?
Yury G. Kudryashov (Jun 30 2020 at 14:33):
If I unfold everything back to
α, then I get
if a ≤ b then a else b and
if b ≤ a then b else a.
Kevin Buzzard (Jun 30 2020 at 16:59):
Last updated: Aug 03 2023 at 10:10 UTC