English
Let {Z_i} be a family of commutative monoids each endowed with a partial order such that every Z_i is an ordered monoid. Then the product ∏_{i} Z_i, with multiplication and order defined coordinatewise, is an ordered commutative monoid. Equivalently, for f,g in ∏_{i} Z_i, (f g)(i) = f(i) g(i) and f ≤ g iff ∀ i, f(i) ≤ g(i).
Русский
Пусть {Z_i} — семейство коммутативных моноидов, каждая из которых имеет частичный порядок и является упорядоченным моноидом. Тогда их произведение ∏_{i} Z_i, со степенным умножением и порядком, задаваемыми по координатам, является упорядоченным коммутативным моноидом. То есть для любого f,g ∈ ∏_{i} Z_i выполняется (f g)(i) = f(i) g(i) и f ≤ g тогда и только тогда, когда для всех i выполняется f(i) ≤ g(i).
LaTeX
$$$\\displaystyle \\mathcal{Z} = (Z_i)_{i \\in I} \\text{ with each } Z_i \\text{ an ordered commutative monoid, then } \\prod_{i\\in I} Z_i \\text{ is an ordered commutative monoid with } (f \\le g) \\iff (\\forall i, f(i) \\le g(i)) \text{ and } (f g)(i)=f(i) g(i).$$$
Lean4
/-- The product of a family of ordered commutative monoids is an ordered commutative monoid. -/
@[to_additive /-- The product of a family of ordered additive commutative monoids is
an ordered additive commutative monoid. -/
]
instance isOrderedMonoid {ι : Type*} {Z : ι → Type*} [∀ i, CommMonoid (Z i)] [∀ i, PartialOrder (Z i)]
[∀ i, IsOrderedMonoid (Z i)] : IsOrderedMonoid (∀ i, Z i) where
mul_le_mul_left _ _ w _ := fun i => mul_le_mul_left' (w i) _
