Theorems · Theorem · measure theory

MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring

∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C →
        ∀ {s : Set α}, MeasurableSet s → ∀ {ε : ENNReal}, 0 < ε → ∃ t ∈ supClosure C, μ (symmDiff t s) < ε

Given a semiring of sets C covering the space modulo 0 and generating the measurable space structure, any measurable set can be approximated by finite unions of elements of C.

Defined in

Mathlib.MeasureTheory.Measure.MeasuredSets

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.IsFiniteMeasure