instMinOfLinearOrder — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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