English
Let f: s → N with f(i) ≥ 1 for i ∈ s. Then ∏_{i∈s} f(i) = 1 if and only if f(i) = 1 for all i ∈ s.
Русский
Пусть f(i) ≥ 1 для всех i ∈ s. Тогда ∏_{i∈s} f(i) = 1 тогда и только тогда, когда для всех i ∈ s имеет место f(i) = 1.
LaTeX
$$$ \\forall \\iota\\, N\\, [\\text{MulLeftMono } N], ( \\forall i \\in s, 1 \\le f(i) ) \\Rightarrow \\left( \\left( \\prod_{i \\in s} f(i) \\right) = 1 \\Leftrightarrow \\forall i \\in s, f(i) = 1 \\right). $$$
Lean4
@[to_additive sum_eq_zero_iff_of_nonneg]
theorem prod_eq_one_iff_of_one_le' [MulLeftMono N] : (∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
classical
refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
intro a s ha ih H
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this), forall_mem_insert,
ih this]
