toSigmaFinite — Mathlib

English

Every finite measure is sigma-finite.

Русский

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

LaTeX

$$instance (priority := 100) toSigmaFinite {_m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] : SigmaFinite μ$$

Lean4

/-- Every finite measure is σ-finite. -/
instance (priority := 100) toSigmaFinite {_m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] :
    SigmaFinite μ :=
  ⟨⟨⟨fun _ => univ, fun _ => trivial, fun _ => measure_lt_top μ _, iUnion_const _⟩⟩⟩

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