Commit 2023-10-16 14:39 b3740a51

View on Github →

feat: lemmas for MeasurableSpace.Basic (#7682)

From the Sobolev project

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem Measurable.eq_mp

added theorem MeasurableEquiv.coe_sumPiEquivProdPi

added theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm

added def MeasurableEquiv.piCongrLeft

added theorem MeasurableEquiv.piCongrLeft_eq

added def MeasurableEquiv.sumPiEquivProdPi

added theorem measurable_eq_mp

added theorem measurable_piCongrLeft

added theorem measurable_update'

modified theorem measurable_update

added theorem measurable_update_left