instIsOrderedMonoid — Mathlib

English

If β is a partially ordered monoid with appropriate continuous multiplication, then the continuous maps C(α, β) form an ordered monoid under pointwise multiplication.

Русский

Если β — частично упорядоченная моноида с непрерывным умножением, то отображения C(α, β) образуют упорядоченную моноиду при покомпонентном умножении.

LaTeX

$$$\\text{IsOrderedMonoid } C(α, β)\\text{ given } [PartialOrder β], [CommMonoid β], [IsOrderedMonoid β], [ContinuousMul β]$ with operation $(f,g)\\mapsto (x\\mapsto f(x)g(x))$.$$

Lean4

@[to_additive]
instance [PartialOrder β] [CommMonoid β] [IsOrderedMonoid β] [ContinuousMul β] : IsOrderedMonoid C(α, β) where
  mul_le_mul_left _ _ hfg c x := mul_le_mul_left' (hfg x) (c x)

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