Theorem MeasureTheory.MeasuredSets.continuous_measure

Modification history

2026-01-31 14:23
Mathlib/MeasureTheory/Measure/MeasuredSets.lean
feat: distance on the set of measurable sets given by the measure of the symmetric difference (#34517) …
Added MeasureTheory.MeasuredSets.continuous_measureView on Github →