English
Let N be a partially ordered commutative monoid in which left-multiplication is order-preserving. If f,g : ι → N satisfy f(i) ≤ g(i) for every i in a finite set s ⊆ ι, then the product over i ∈ s of f(i) is ≤ the product over i ∈ s of g(i).
Русский
Пусть N — упорядоченный коммутативный моноид, для которого умножение слева сохраняет порядок. Если f,g : ι → N таковы, что f(i) ≤ g(i) для каждого i ∈ конечного подмножества s ⊆ ι, то ∏_{i∈s} f(i) ≤ ∏_{i∈s} g(i).
LaTeX
$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], \\forall f,g:\\\\iota \\to N, \\forall s:\\\\mathrm{Finset}\\\\iota, [\\text{MulLeftMono } N], ( \\forall i \\in s, f(i) \\le g(i) ) \\Rightarrow \\prod_{i\\in s} f(i) \\le \\prod_{i\\in s} g(i). $$$
Lean4
/-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
equal to the corresponding factor `g i` of another finite product, then
`∏ i ∈ s, f i ≤ ∏ i ∈ s, g i`. -/
@[to_additive (attr := gcongr) sum_le_sum]
theorem prod_le_prod' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i :=
Multiset.prod_map_le_prod_map f g h
