Theorems · Theorem · measure theory

MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite

∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  MeasureTheory.IsSetAlgebra 𝒜 → ∀ (S : μ.FiniteSpanningSetsIn 𝒜), m = MeasurableSpace.generateFrom 𝒜 → μ.MeasureDense 𝒜

If a measure space X is generated by an algebra of sets which contains a monotone countable family of sets with finite measure spanning X (thus the measure is σ-finite), then this algebra of sets is measure-dense.

Defined in

Mathlib.MeasureTheory.Measure.SeparableMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace