instSFiniteOfSigmaFinite — Mathlib

English

Every sigma-finite measure is s-finite.

Русский

Каждая сигма-конечная мера является s-конечной.

LaTeX

$$$\text{SFinite}(\mu)$ given $[\Sigma\text{-finite }\mu]$$$

Lean4

instance (priority := 100) [SigmaFinite μ] : SFinite μ :=
  by
  have : ∀ n, Fact (μ (disjointed (spanningSets μ) n) < ∞) := fun n ↦
    ⟨(measure_mono (disjointed_subset _ _)).trans_lt (measure_spanningSets_lt_top μ n)⟩
  exact
    ⟨⟨fun n ↦ μ.restrict (disjointed (spanningSets μ) n), fun n ↦ by infer_instance,
        (sum_restrict_disjointed_spanningSets μ μ).symm⟩⟩

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