Theorem hasFDerivWithinAt_of_mem_nhds

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_mem_nhds View on Github →