Commit 2021-02-13 00:49 152ad1fc

View on Github →

feat(measure_theory/measure_space): add theorems about restrict and subtraction (#5000) This is the next tranche of theorems toward Lebesgue-Radon-Nikodym.

Estimated changes

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.restrict_apply_self

added theorem measure_theory.measure.restrict_eq_self

added theorem measure_theory.measure.restrict_sub_eq_restrict_sub_restrict

added theorem measure_theory.measure.sub_apply_eq_zero_of_restrict_le_restrict