English
If f(i) ≥ 1 for all i, and there exists some i with f(i) > 1, and the multiplicative support is finite, then the finprod is strictly greater than 1.
Русский
Если f(i) ≥ 1 для всех i и есть i с f(i) > 1, и поддержка конечна, то произведение больше 1.
LaTeX
$$$\\displaystyle \\Big( \\forall i, 1 \\le f(i) \\Big) \\rightarrow \\Big( \\exists i, 1 < f(i) \\Big) \\rightarrow (mulSupport f).Finite \\rightarrow 1 < \\prodᶠ i, f(i)$$$
Lean4
@[to_additive finsum_pos']
theorem one_lt_finprod' {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M}
(h : ∀ i, 1 ≤ f i) (h' : ∃ i, 1 < f i) (hf : (mulSupport f).Finite) : 1 < ∏ᶠ i, f i :=
by
rcases h' with ⟨i, hi⟩
rw [finprod_eq_prod _ hf]
refine Finset.one_lt_prod' (fun i _ ↦ h i) ⟨i, ?_, hi⟩
simpa only [Finite.mem_toFinset, mem_mulSupport] using ne_of_gt hi
