instIsOrderedMonoid — Mathlib

English

If β is a commutative monoid with a compatible order, then Germ l β is an ordered monoid: multiplication respects the order.

Русский

Если β — коммутативная моноида с совместимой упорядоченностью, то Germ l β является упорядоченной моноидой: умножение сохраняет порядок.

LaTeX

$$$\\text{IsOrderedMonoid}(\\mathrm{Germ}_l \\beta)$$$

Lean4

@[to_additive]
instance instIsOrderedMonoid [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] : IsOrderedMonoid (Germ l β) where
  mul_le_mul_left f g := inductionOn₂ f g fun _ _ H h ↦ inductionOn h fun _ ↦ H.mono fun _ H ↦ mul_le_mul_left' H _

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