countable_support_nnreal — Mathlib

English

If f: α → ℝ≥0 is summable, then its support is countable.

Русский

Если f: α → ℝ≥0 суммируема, то множество опоры f (где f(a) ≠ 0) является счетным.

LaTeX

$$$\\{a \\in \\alpha \\mid f(a) \\neq 0\\} \\text{ is countable}$$$

Lean4

/-- Summable non-negative functions have countable support -/
theorem _root_.Summable.countable_support_nnreal (f : α → ℝ≥0) (h : Summable f) : f.support.Countable :=
  by
  rw [← NNReal.summable_coe] at h
  simpa [support] using h.countable_support

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