Theorem intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc

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_uIcc_of_contDiffOn_uIccView on Github →