Theorem Convex.exists_forall_hasDerivWithinAt

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