Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-19 11:33 245b614e

View on Github →

chore(measure_theory/measure): move subtraction to a new file (#12809)

Estimated changes

Modified src/measure_theory/decomposition/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

deleted theorem measure_theory.measure.restrict_sub_eq_restrict_sub_restrict

deleted theorem measure_theory.measure.sub_add_cancel_of_le

deleted theorem measure_theory.measure.sub_apply

deleted theorem measure_theory.measure.sub_apply_eq_zero_of_restrict_le_restrict

deleted theorem measure_theory.measure.sub_def

deleted theorem measure_theory.measure.sub_eq_zero_of_le

deleted theorem measure_theory.measure.sub_le

Created src/measure_theory/measure/sub.lean

added theorem measure_theory.measure.restrict_sub_eq_restrict_sub_restrict

added theorem measure_theory.measure.sub_add_cancel_of_le

added theorem measure_theory.measure.sub_apply

added theorem measure_theory.measure.sub_apply_eq_zero_of_restrict_le_restrict

added theorem measure_theory.measure.sub_def

added theorem measure_theory.measure.sub_eq_zero_of_le

added theorem measure_theory.measure.sub_le