Commit 2024-11-18 13:41 a0408b3f

View on Github →

chore(MeasureTheory): move Measure.comap to a new file (#19178)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Comap.lean

added theorem MeasurableEmbedding.comap_add

added theorem MeasurableEquiv.comap_symm

added theorem MeasurableEquiv.map_symm

added theorem MeasureTheory.Measure.NullMeasurableSet.image

added theorem MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap

added def MeasureTheory.Measure.comap

added theorem MeasureTheory.Measure.comap_apply

added theorem MeasureTheory.Measure.comap_apply₀

added theorem MeasureTheory.Measure.comap_preimage

added theorem MeasureTheory.Measure.comap_zero

added def MeasureTheory.Measure.comapₗ

added theorem MeasureTheory.Measure.comapₗ_apply

added theorem MeasureTheory.Measure.comapₗ_eq_comap

added theorem MeasureTheory.Measure.le_comap_apply

added theorem MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero

added theorem comap_swap

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem MeasurableEmbedding.comap_add

deleted theorem MeasurableEquiv.comap_symm

deleted theorem MeasurableEquiv.map_symm

deleted theorem MeasureTheory.Measure.NullMeasurableSet.image

deleted theorem MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap

deleted def MeasureTheory.Measure.comap

deleted theorem MeasureTheory.Measure.comap_apply

deleted theorem MeasureTheory.Measure.comap_apply₀

deleted theorem MeasureTheory.Measure.comap_preimage

deleted theorem MeasureTheory.Measure.comap_swap

deleted theorem MeasureTheory.Measure.comap_zero

deleted def MeasureTheory.Measure.comapₗ

deleted theorem MeasureTheory.Measure.comapₗ_apply

deleted theorem MeasureTheory.Measure.comapₗ_eq_comap

deleted theorem MeasureTheory.Measure.le_comap_apply

deleted theorem MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero

Modified Mathlib/MeasureTheory/Measure/Restrict.lean