tsum_eq_zero — Mathlib

English

For f : α → ENNReal, ∑' a, f(a) = 0 if and only if f(a) = 0 for all a.

Русский

Для любой функции f : α → ENNReal сумма равна нулю тогда и только тогда, когда каждый член равен нулю: ∑' a, f(a) = 0 ⇔ ∀ a, f(a) = 0.

LaTeX

$$$\sum'_{a \in \alpha} f(a) = 0 \;\Longleftrightarrow\; \forall a \in \alpha, f(a) = 0$$$

Lean4

@[simp]
protected theorem tsum_eq_zero : ∑' i, f i = 0 ↔ ∀ i, f i = 0 :=
  ENNReal.summable.tsum_eq_zero_iff

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