Commit 2023-10-05 10:24 49f71889

View on Github →

feat: add simple lemmas about MeasurableEquiv (#7509)

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableEquiv.eq_image_iff_symm_image_eq

added theorem MeasurableEquiv.image_preimage

added theorem MeasurableEquiv.image_symm

added theorem MeasurableEquiv.preimage_image

added theorem MeasurableEquiv.preimage_symm

added theorem MeasurableEquiv.symm_symm

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasurableEquiv.comap_symm

added theorem MeasurableEquiv.map_symm