tprod_ne_one_iff — Mathlib

English

For a multipliable f, the infinite product ∏' i, f(i) is not equal to 1 if and only if there exists some i with f(i) ≠ 1.

Русский

Для многократно суммируемого f бесконечное произведение ∏' i, f(i) не равно 1 тогда и только тогда, когда существует i с f(i) ≠ 1.

LaTeX

$$$\\\\prod' i \\, f(i) \\\\neq 1 \\\\iff \\\\exists i \\, f(i) \\\neq 1$$$

Lean4

@[to_additive]
protected theorem tprod_ne_one_iff (hf : Multipliable f) : ∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1 := by
  rw [Ne, hf.tprod_eq_one_iff, not_forall]

Похожие утверждения