Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 16:19 59bf4540

View on Github →

refactor(measure_theory): enable dot notation for measure.map (#12350) Refactor to allow for using dot notation with measure.map (was previously not possible because it was bundled as a linear map). Mirrors measure.restrict wrapper implementation for measure.restrictₗ.

Estimated changes

Modified src/measure_theory/constructions/prod.lean

Modified src/measure_theory/group/measure.lean

Modified src/measure_theory/measure/haar.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

Modified src/measure_theory/measure/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

modified theorem measurable_embedding.ae_map_iff

modified theorem measurable_embedding.map_apply

modified theorem measurable_embedding.map_comap

modified theorem measurable_equiv.map_apply_eq_iff_map_symm_apply_eq

modified theorem measurable_equiv.map_map_symm

modified theorem measurable_equiv.map_symm_map

modified theorem measurable_equiv.restrict_map

modified theorem measure_theory.ae_of_ae_map

modified theorem measure_theory.measure.le_map_apply

modified def measure_theory.measure.map

added theorem measure_theory.measure.map_add

modified theorem measure_theory.measure.map_mono

added theorem measure_theory.measure.map_smul

added theorem measure_theory.measure.map_zero

added def measure_theory.measure.mapₗ

added theorem measure_theory.measure.mapₗ_apply

modified theorem measure_theory.measure.quasi_measure_preserving.ae_map_le

modified theorem measure_theory.measure.tendsto_ae_map

modified theorem measure_theory.mem_ae_of_mem_ae_map