canonicallyOrderedAdd — Mathlib

English

If α is a Monoid with PartialOrder and CanonicallyOrderedMul, then Additive α is CanonicallyOrderedAdd, i.e., a ≤ a + b and a ≤ b + a hold for all a,b in α.

Русский

Если α — моноид с частичным порядком и CanonicallyOrderedMul, то Additive α — канонически упорядоченный аддитивный моноид; т.е. для любых a,b в α выполняются a ≤ a + b и a ≤ b + a.

LaTeX

$$$[\text{Monoid}(\alpha)]\,[\text{PartialOrder}(\alpha)]\,[\text{CanonicallyOrderedMul}(\alpha)] \Rightarrow \text{CanonicallyOrderedAdd}(\mathrm{Additive}(\alpha)).$$$

Lean4

instance canonicallyOrderedAdd [Monoid α] [PartialOrder α] [CanonicallyOrderedMul α] :
    CanonicallyOrderedAdd (Additive α)
    where
  le_add_self _ _ := le_mul_self (α := α)
  le_self_add _ _ := le_self_mul (α := α)

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