sigmaFinite_of_countable — Mathlib

English

If S is countable family of sets with μ(s) < ∞ for all s ∈ S and ⋃ S = univ, then μ is sigma-finite.

Русский

Если S — счётная семейство множеств и μ(s) < ∞ для всех s ∈ S, а ⋃S = univ, тогда μ — сигма-конечная.

LaTeX

$$$[Countable S] \; (hc : S.Countable) (hμ : \forall s ∈ S, μ s < ∞) (hU : ⋃₀ S = univ) : SigmaFinite μ$$$

Lean4

theorem sigmaFinite_of_countable {S : Set (Set α)} (hc : S.Countable) (hμ : ∀ s ∈ S, μ s < ∞) (hU : ⋃₀ S = univ) :
    SigmaFinite μ :=
  by
  obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ ⋃ n, s n = univ :=
    (@exists_seq_cover_iff_countable _ (fun x => μ x < ∞) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩
  exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩

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