Commit 2024-01-02 05:36 4f83eae3

View on Github →

chore(MeasureTheory): golf (#9374) Reorder/golf lemmas, add ae_restrict_iff₀. Also remove 3 lemmas that are no longer needed and can be proved in 1 line each.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

deleted theorem MeasureTheory.ae_restrict_eq_const_iff_ae_eq_const_of_mem'

deleted theorem MeasureTheory.ae_restrict_eq_const_iff_ae_eq_const_of_mem

deleted theorem MeasureTheory.set_integral_eq_integral_of_ae_restrict_eq_zero

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.ae_restrict_iff₀

modified theorem MeasureTheory.ae_restrict_mem₀