lt_top_of_sum_ne_top — Mathlib

English

If the sum ∑_{x∈s} f(x) is finite, then every summand f(a) with a ∈ s is finite.

Русский

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

LaTeX

$$$\left(\sum_{x\in s} f(x) \neq \infty\right) \Rightarrow \forall a\in s,\ f(a) < \infty$$$

Lean4

theorem lt_top_of_sum_ne_top {s : Finset α} {f : α → ℝ≥0∞} (h : ∑ x ∈ s, f x ≠ ∞) {a : α} (ha : a ∈ s) : f a < ∞ :=
  sum_lt_top.1 h.lt_top a ha

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