instIsOrderedAddMonoid — Mathlib

English

If α_i are additive commutative monoids with a compatible order and DFinsupp is formed, then Π₀ i, α_i is an IsOrderedAddMonoid, i.e., addition preserves order on the left.

Русский

Если α_i — коммутативные моноиды по сумме с допустимым порядком, то Π₀ i, α_i образуют IsOrderedAddMonoid: сложение сохраняет порядок слева.

LaTeX

$$$$ \text{IsOrderedAddMonoid}(\Pi_0 i, \alpha_i) \quad\text{with additive structure defined pointwise}. $$$$

Lean4

instance (α : ι → Type*) [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsOrderedAddMonoid (α i)] :
    IsOrderedAddMonoid (Π₀ i, α i) :=
  { add_le_add_left := fun _ _ h c i ↦ add_le_add_left (h i) (c i) }

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