sum_eq_top — Mathlib

English

For a finite set s and function f: α → ℝ≥0∞, the sum ∑_{x∈s} f(x) equals ∞ if and only if there exists some a ∈ s with f(a) = ∞.

Русский

Для конечного множества s и функции f: α → ℝ≥0∞ сумма ∑_{x∈s} f(x) бесконечна тогда и только тогда, когда существует элемент a ∈ s с f(a) = ∞.

LaTeX

$$$\sum_{x\in s} f(x) = \infty \;\Leftrightarrow\; \exists a \in s,\ f(a) = \infty$$$

Lean4

/-- A sum is infinite iff one of the summands is infinite. -/
@[simp]
theorem sum_eq_top : ∑ x ∈ s, f x = ∞ ↔ ∃ a ∈ s, f a = ∞ :=
  WithTop.sum_eq_top

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