Theorem Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric

Modification history

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