Commit 2025-05-11 06:44 989d4ee7

feat(MeasureTheory/Measure): Add fun_prop for QuasiMeasurePreserving + add lambda theorems for other classes (#24273) Add fun_prop declaration to quasiMeasurePreserving and various theorems which prove quasiMeasurePreserving as well as AEMeasurable.comp_quasiMeasurePreserving which proves AEMeasurable from composition with a quasiMeasurePreserving function. This significantly improves fun_props ability to prove functions are AEMeasurable. Add fst and snd (lambda theorems) for QuasiMeasurePreserving, AEMeasureable, StronglyMeasurable, EventuallyEq (to do this we also have to rename some incorrectly named theorems).