Commit 2024-06-13 00:50 cc4d7641

View on Github →

feat: Add lemmas about finite products of measures (#13311) Add the following lemmas about finite product of measures and measurable equivalences:

piCongrLeft_apply_apply
pi_map_piCongrLeft
pi_map_piOptionEquivProd

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.Measure.pi_map_piCongrLeft

added theorem MeasureTheory.Measure.pi_map_piOptionEquivProd

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableEquiv.piCongrLeft_apply_apply