English
Let N be a partially ordered commutative monoid with MulLeftMono. If f: ι → N satisfies f(i) ≥ 1 for all i in a finite s ⊆ ι, then 1 ≤ ∏_{i∈s} f(i).
Русский
Пусть N — упорядоченный коммутативный моноид с условием MulLeftMono. Если f: ι → N такова, что f(i) ≥ 1 для всех i ∈ конечного множества s ⊆ ι, то 1 ≤ ∏_{i∈s} f(i).
LaTeX
$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s : \\mathrm{Finset} \\iota}, [\\text{MulLeftMono } N], ( \\forall i \\in s, 1 \\le f(i) ) \\Rightarrow 1 \\le \\prod_{i \\in s} f(i). $$$
Lean4
@[to_additive sum_nonneg]
theorem one_le_prod' [MulLeftMono N] (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
le_trans (by rw [prod_const_one]) (prod_le_prod' h)
