Theorem MeasureTheory.Measure.MeasureDense.nonempty'

Modification history

2024-09-19 20:54

Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

feat: separable measure and sufficient condition for Lp spaces to be second-countable (#12519) …

Added MeasureTheory.Measure.MeasureDense.nonempty'View on Github →