Commit 2021-10-28 17:00 b9ff26b5

View on Github →

chore(measure_theory/measure/measure_space): reorder, golf (#10015) Move restrict_apply' up and use it to golf some proofs. Drop an unneeded measurable_set assumption in 1 proof.

Estimated changes

Modified src/measure_theory/function/ae_eq_of_integral.lean

Modified src/measure_theory/measure/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

modified theorem measure_theory.ae_of_ae_restrict_of_ae_restrict_compl

modified theorem measure_theory.measure.restrict_apply'

modified theorem measure_theory.measure.restrict_empty

added theorem measure_theory.measure.restrict_eq_self'

deleted theorem measure_theory.measure.restrict_eq_self_of_measurable_subset

deleted theorem measure_theory.measure.restrict_eq_self_of_subset_of_measurable