instMaxOfLinearOrder — Mathlib

English

If α is a Monoid with LinearOrder, then Max on Units α is defined so that max a b has value max(a.val, b.val).

Русский

Если α — моноид с линейным порядком, то максимум на единицах α определяется так, что max a b имеет значение max(a.val, b.val).

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ \\mathrm{max}_{\\mathrm{Units}}(a,b).\\mathrm{val} = \\max(a.\\mathrm{val}, b.\\mathrm{val})$$$

Lean4

@[to_additive]
instance [Monoid α] [LinearOrder α] : Max αˣ where max a b := if a ≤ b then b else a

Похожие утверждения