Theorem MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring

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