Theorem hasFDerivWithinAt_of_isOpen

Modification history

2023-11-07 14:27

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

feat: lemmas analogous to fderiv_within_of_isOpen (#8057) …

Added hasFDerivWithinAt_of_isOpen View on Github →