Theorem MeasureTheory.Measure.MeasureDense.completion

Modification history

2025-04-08 07:05

Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

feat: the completion of a separable measure is separable (#23796)

Added MeasureTheory.Measure.MeasureDense.completion View on Github →