Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.integral_Ico_eq_integral_Ioc
Modification history
2026-03-18 09:33
Mathlib/MeasureTheory/Integral/Bochner/Set.lean
feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (#34966) …
Added
MeasureTheory.integral_Ico_eq_integral_Ioc
View on Github →