sigmaFinite_iff_measure_singleton_lt_top

English

A measure on a countable space is sigma-finite iff every singleton has finite measure.

Русский

Мера на счётном пространстве сигма-конечна тогда и только тогда, когда каждая единичная точка имеет конечную массу.

LaTeX

$$$[Countable α] :\; SigmaFinite μ \iff \forall a, μ({a}) < \infty$$$

Lean4

/-- A measure on a countable space is sigma-finite iff it gives finite mass to every singleton.

See `measure_singleton_lt_top` for the forward direction without the countability assumption. -/
theorem sigmaFinite_iff_measure_singleton_lt_top [Countable α] : SigmaFinite μ ↔ ∀ a, μ { a } < ∞
    where
  mp _ a := measure_singleton_lt_top
  mpr
    hμ := by
    cases isEmpty_or_nonempty α
    · rw [Subsingleton.elim μ 0]
      infer_instance
    · obtain ⟨f, hf⟩ := exists_surjective_nat α
      exact ⟨⟨⟨fun n ↦ {f n}, by simp, by simpa [hf.forall] using hμ, by simp [hf.range_eq]⟩⟩⟩

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