Commit 2025-04-08 07:05 8249256e

View on Github →

feat: the completion of a separable measure is separable (#23796)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

added theorem MeasureTheory.Measure.MeasureDense.completion

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

added theorem MeasureTheory.ae_eq_set_diff

added theorem MeasureTheory.ae_eq_set_symmDiff