Commit 2024-07-24 08:31 5ef17893

View on Github →

feat(MeasureSpace): generalize pigeonhole to NullMeasurableSets (#15089)

Estimated changes

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.tsum_measure_le_measure_univ