Commit 2023-05-10 01:01 3ae40231

View on Github →

feat: port Dynamics.Ergodic.MeasurePreserving (#3821)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

added theorem MeasureTheory.MeasurableEquiv.measurePreserving_symm

added theorem MeasureTheory.MeasurePreserving.aemeasurable_comp_iff

added theorem MeasureTheory.MeasurePreserving.exists_mem_image_mem

added theorem MeasureTheory.MeasurePreserving.exists_mem_image_mem_of_volume_lt_mul_volume

added theorem MeasureTheory.MeasurePreserving.measure_preimage

added theorem MeasureTheory.MeasurePreserving.measure_preimage_emb

added theorem MeasureTheory.MeasurePreserving.restrict_image_emb

added theorem MeasureTheory.MeasurePreserving.restrict_preimage

added theorem MeasureTheory.MeasurePreserving.restrict_preimage_emb

added theorem MeasureTheory.MeasurePreserving.symm

added structure MeasureTheory.MeasurePreserving