Commit 2024-08-25 13:48 b1ee9a95

View on Github →

chore(MeasureSpace): generalize to NullMeasurableSet (#16104)

Estimated changes

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.NullMeasurableSet.preimage