Commit 2023-10-19 11:58 58a6689c

View on Github →

feat: some measure preserving equivalences on pi-types (#7751)

Also fix the statement of some lemmas of an earlier PR.
From the Sobolev project
There are more that depend on #7341

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.measurePreserving_piCongrLeft

modified theorem MeasureTheory.measurePreserving_piEquivPiSubtypeProd

added theorem MeasureTheory.measurePreserving_sumPiEquivProdPi

added theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm

added theorem MeasureTheory.volume_measurePreserving_piCongrLeft

added theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi

added theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm

modified theorem MeasureTheory.volume_preserving_piEquivPiSubtypeProd

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableEquiv.coe_piCongrLeft

deleted theorem MeasurableEquiv.piCongrLeft_eq