2026-03-18 09:33
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (#34966) …
Added intervalIntegral.integral_Ioi_sub_Ioi'