Def MeasureTheory.MeasuredSets

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.MeasuredSetsView on Github →