Theorems · Theorem · measure theory

MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite

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

If a measurable space equipped with a finite measure is generated by an algebra of sets, then this algebra of sets is measure-dense.

Defined in

Mathlib.MeasureTheory.Measure.SeparableMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.IsFiniteMeasure