Commit 2026-03-18 09:33 fe4b0121

View on Github →

feat(MeasureTheory): add continuousWithinAt_Ici/Iic_primitive_Ioi/Iio and continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic (#34966) This PR proves:

continuousWithinAt_Ici/Iic_primitive_Ioi/Iio
continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic
integral_Ioi_sub_Ioi, integral_Ioi_sub_Ioi', integral_Iio_sub_Iio, integral_Iio_sub_Iio'
Ioi_diff_Ioc

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

added theorem MeasureTheory.integral_Ico_eq_integral_Ioc

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

added theorem MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ici

added theorem MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi

added theorem MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iic

added theorem MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio

added theorem MeasureTheory.IntegrableOn.continuousWithinAt_Ici_primitive_Ioi

added theorem MeasureTheory.IntegrableOn.continuousWithinAt_Iic_primitive_Iio

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

added theorem intervalIntegral.integral_Iio_sub_Iio'

added theorem intervalIntegral.integral_Iio_sub_Iio

added theorem intervalIntegral.integral_Ioi_sub_Ioi'

added theorem intervalIntegral.integral_Ioi_sub_Ioi

Modified Mathlib/Order/Interval/Set/LinearOrder.lean

added theorem Set.Ioi_diff_Ioc