isOrderedAddMonoid — Mathlib

English

If each coordinate α_i is an ordered additive group, then Lex(Π_i α_i) inherits an IsOrderedAddMonoid structure.

Русский

Если каждая координата α_i является упорядоченной аддитивной группой, то Lex(Π_i α_i) наследует структуру IsOrderedAddMonoid.

LaTeX

$$$$ \\text{IsOrderedAddMonoid}(\\\\mathrm{Lex}(\\\\Pi_i α_i)) $$$$

Lean4

instance isOrderedAddMonoid [∀ i, AddCommGroup (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsOrderedAddMonoid (α i)] :
    IsOrderedAddMonoid (Lex (Π₀ i, α i)) where add_le_add_left _ _ := add_le_add_left

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