Commit 2023-11-09 12:07 7901bf47

View on Github →

feat(MeasureSpace): add Measure.map_apply₀ (#8283) Add a version of map_apply for NullMeasurableSets. Also remove some empty lines and golf the proof of ae_le_of_ae_lt.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.liftLinear_apply₀

added theorem MeasureTheory.Measure.map_apply₀

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

modified theorem MeasureTheory.ae_le_of_ae_lt