Commit 2024-08-12 19:34 3697f513

View on Github →

chore(MeasurePreserving): rename a lemma (#15742) There is no volume in the statement.

Estimated changes

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

added theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure

deleted theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume