Commit 2023-09-28 17:09 3f15d771

View on Github →

chore: split Measure.Trim definition from MeasureSpace.lean (#7385) The file MeasureSpace has more than 4000 lines: let's move some results out of it.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted def MeasureTheory.Measure.trim

deleted theorem MeasureTheory.ae_eq_of_ae_eq_trim

deleted theorem MeasureTheory.ae_le_of_ae_le_trim

deleted theorem MeasureTheory.ae_of_ae_trim

deleted theorem MeasureTheory.le_trim

deleted theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero

deleted theorem MeasureTheory.measure_trim_toMeasurable_eq_zero

deleted theorem MeasureTheory.restrict_trim

deleted theorem MeasureTheory.sigmaFiniteTrim_mono

deleted theorem MeasureTheory.sigmaFinite_trim_bot_iff

deleted theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure

deleted theorem MeasureTheory.trim_eq_self

deleted theorem MeasureTheory.trim_measurableSet_eq

deleted theorem MeasureTheory.trim_trim

deleted theorem MeasureTheory.zero_trim

Created Mathlib/MeasureTheory/Measure/Trim.lean

added def MeasureTheory.Measure.trim

added theorem MeasureTheory.ae_eq_of_ae_eq_trim

added theorem MeasureTheory.ae_le_of_ae_le_trim

added theorem MeasureTheory.ae_of_ae_trim

added theorem MeasureTheory.le_trim

added theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero

added theorem MeasureTheory.measure_trim_toMeasurable_eq_zero

added theorem MeasureTheory.restrict_trim

added theorem MeasureTheory.sigmaFiniteTrim_mono

added theorem MeasureTheory.sigmaFinite_trim_bot_iff

added theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure

added theorem MeasureTheory.trim_eq_self

added theorem MeasureTheory.trim_measurableSet_eq

added theorem MeasureTheory.trim_trim

added theorem MeasureTheory.zero_trim