Mathlib Changelog
v4
Changelog
About
Github
Theorem
intervalIntegral.integral_Ici_sub_Ici
Modification history
2026-04-24 08:11
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
feat(MeasureTheory): Integral over Ioi tends to zero (#34298) …
Added
intervalIntegral.integral_Ici_sub_Ici
View on Github →