isOrderedMonoid — Mathlib

English

If α is a commutative monoid with a PartialOrder and IsOrderedMonoid, then the order dual αᵒᵈ is an IsOrderedMonoid as well.

Русский

Если α — коммутативное моноиды с частичным порядком и свойством IsOrderedMonoid, то противоположный по порядку моноид αᵒᵈ тоже является IsOrderedMonoid.

LaTeX

$$IsOrderedMonoid(\alpha^{\mathrm{op}})$$

Lean4

@[to_additive]
instance isOrderedMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid αᵒᵈ :=
  { mul_le_mul_left := fun _ _ h c => mul_le_mul_left' h c }

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