Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 00:26 2d17f521

View on Github →

feat(measure_theory/integral/*): integral over map (e : α ≃ᵐ β) μ (#9316)

Estimated changes

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable_map_equiv

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.integral_map_equiv

Modified src/measure_theory/integral/integrable_on.lean

added theorem measure_theory.integrable_on_map_equiv

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.set_integral_map_equiv

Modified src/measure_theory/measure/measure_space.lean

added theorem ae_measurable_map_equiv_iff

added theorem measurable_equiv.restrict_map