sum_ne_top — Mathlib

English

The sum ∑_{x∈s} f(x) ≠ ∞ if and only if every summand f(x) ≠ ∞.

Русский

Сумма ∑_{x∈s} f(x) конечна тогда и только тогда, когда каждый член суммирования f(x) конечен.

LaTeX

$$$\sum_{x\in s} f(x) \neq \infty \;\Leftrightarrow\; \forall x \in s,\ f(x) \neq \infty$$$

Lean4

/-- A sum is finite iff all summands are finite. -/
theorem sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ∞ :=
  WithTop.sum_ne_top

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