English
Let f,g: ι → M and s a finite set. If f(i) ≤ g(i) for all i in s, then (∏_{i∈s} f(i) = ∏_{i∈s} g(i)) if and only if f(i) = g(i) for all i in s.
Русский
Пусть f,g: ι → M и s конечное. Если ∀ i ∈ s, f(i) ≤ g(i), то равенство произведений ∏_{i∈s} f(i) = ∏_{i∈s} g(i) эквивалентно тому, что ∀ i ∈ s, f(i) = g(i).
LaTeX
$$$\left( \forall i \in s,\ f(i) \le g(i) \right) \implies \left( \left( \prod_{i \in s} f(i) \;=\; \prod_{i \in s} g(i) \right) \iff \left( \forall i \in s,\ f(i) = g(i) \right) \right)$$$
Lean4
@[to_additive]
theorem prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
((∏ i ∈ s, f i) = ∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i := by
classical
revert h
refine
Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
exact
mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a)) (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)
