isOrderedAddMonoid — Mathlib

English

If α is an ordered additive monoid, then the finsupp space ι →₀ α is an ordered additive monoid under pointwise addition and order.

Русский

Если α — упорядоченный аддитивный моноид, то пространство δ i →₀ α также является упорядоченным аддитивным моноидом по покомпонентному сложению и порядку.

LaTeX

$$IsOrderedAddMonoid(ι →₀ α)$$

Lean4

instance isOrderedAddMonoid : IsOrderedAddMonoid (ι →₀ α) :=
  { add_le_add_left := fun _a _b h c s => add_le_add_left (h s) (c s) }

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