Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ae_measurable_map_equiv_iff

Modification history

2022-04-09 06:37

src/measure_theory/measure/ae_measurable.lean

chore(measure_theory): move lemmas about `ae_measurable` to a new file (#13246)

Modified ae_measurable_map_equiv_iff View on Github →

2021-09-24 00:26

src/measure_theory/measure/measure_space.lean

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

Added ae_measurable_map_equiv_iff View on Github →