Structure MeasureTheory.Measure.MeasureDense

Modification history

2024-10-09 08:43
Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
chore: adaptations for lean4#5542 (#17564) …
Modified MeasureTheory.Measure.MeasureDenseView on Github →
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.MeasureDenseView on Github →