Zulip Chat Archive

Stream: general

Topic: diamond: min/max and order_dual


view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 07:09):

If I have [decidable_linear_order α], then I have two non-defeq has_sup on order_dual α: @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.

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:24):

How is max defined on order_dual?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 16:59):

D'oh


Last updated: May 08 2021 at 18:17 UTC