## Stream: general

### Topic: diamond: min/max and order_dual

#### 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.

#### 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):

D'oh

Last updated: May 08 2021 at 18:17 UTC