Commit 2024-05-25 20:06 fb5cb8b7

View on Github →

feat(AEEqFun): add 3 trivial lemmas (#13043)

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

added theorem MeasureTheory.AEEqFun.compMeasurePreserving_toGerm

added theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm

added theorem MeasureTheory.AEEqFun.comp_compQuasiMeasurePreserving