Theorems · Theorem · measure theory

MeasureTheory.dense_of_generateFrom_isSetSemiring

∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C → Dense (SetLike.coe ⁻¹' supClosure C)

Given a semiring of sets C covering the space modulo 0 and generating the measurable space structure, finite unions of elements of C are dense among measurable sets.

Defined in

Mathlib.MeasureTheory.Measure.MeasuredSets

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.IsFiniteMeasure