Commit 2024-05-18 23:49 68f23711

View on Github →

chore(MeasureTheory): golf (#13016) Minor golf and formatting fixes cherry-picked from an otherwise no longer relevant branch.

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/Measure/Doubling.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.Measure.le_iff

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.Measure.outerMeasure_le_iff

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean