2026-03-18 09:33
Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (#34966) …
Added MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iic