countable_support_ennreal — Mathlib

English

If a function f: α → ℝ≥0∞ has finite sum, its support is countable.

Русский

Если функция f: α → ℝ≥0∞ имеет конечную сумму, то её поддержка счётна.

LaTeX

$$$\sum_i' f(i) \neq \infty \;\Rightarrow\; \operatorname{support}(f)\text{ is countable}.$$$

Lean4

/-- Finitely summable non-negative functions have countable support -/
theorem _root_.Summable.countable_support_ennreal {f : α → ℝ≥0∞} (h : ∑' (i : α), f i ≠ ∞) : f.support.Countable :=
  by
  lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top h
  simpa [support] using (ENNReal.tsum_coe_ne_top_iff_summable.1 h).countable_support_nnreal

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