Commit 2024-02-22 11:57 1443e142

View on Github →

feat: add integral_eq_iff_of_ae_le (#10792)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.integral_eq_iff_of_ae_le

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.div_ae_eq_one

added theorem MeasureTheory.one_le_div_ae

deleted theorem MeasureTheory.sub_ae_eq_zero