Theorem MeasureTheory.MeasuredSets.dist_def

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