Theorem Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric

Modification history

2025-11-24 23:37
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
feat(Analysis): Poincaré lemma for 1-forms (#24019)
Added Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetricView on Github →