Theorems · Theorem · measure theory

MeasureTheory.isSeparable_of_sigmaFinite

∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasurableSpace.CountablyGenerated X]
  [MeasureTheory.SigmaFinite μ], MeasureTheory.IsSeparable μ

If a measurable space is countably generated and equipped with a σ-finite measure, then the measure is separable. This is not an instance because it is used below to prove the more general case where μ is s-finite.

Defined in

Mathlib.MeasureTheory.Measure.SeparableMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace.CountablyGeneratedMeasureTheory.SigmaFinite