instIsOrderedMonoid — Mathlib

English

If β is a CommMonoid with a partial order and IsOrderedMonoid, then the space α →ₛ β inherits an IsOrderedMonoid structure; multiplication is defined pointwise and preserves the order.

Русский

Если β — коммутативный моноид с частичным порядком и IsOrderedMonoid, то пространство α →ₛ β наследует структуру IsOrderedMonoid; операция умножения определяется по точкам и сохраняет порядок.

LaTeX

$$$\\text{IsOrderedMonoid}(\\alpha \\to_{\\mathcal{S}} \\beta)$ with $(f \\cdot g)(x) = f(x) \\cdot g(x)$ and $f \\le g \\implies h \\cdot f \\le h \\cdot g$.$$

Lean4

@[to_additive]
instance [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] : IsOrderedMonoid (α →ₛ β) where
  mul_le_mul_left _ _ h _ _ := mul_le_mul_left' (h _) _

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