Theorem intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc

Modification history

2025-06-16 06:44
Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean
feat: easier to use FTC-2 versions for `C^1` functions (#25769)
Added intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_IccView on Github →