Theorems · Definition · measure theory

MeasureTheory.Measure.toFiniteSpanningSetsIn

{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    (μ : MeasureTheory.Measure α) → [h : MeasureTheory.SigmaFinite μ] → μ.FiniteSpanningSetsIn {s | MeasurableSet s}

If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Cited by

13 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.SigmaFinite