mathlib

0977b203 - feat(measure_theory/interval_integral): weaken assumption in `integral_non_ae_measurable` (#6858)