Theorem HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE

Modification history

2026-02-10 19:29
Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
feat(Analysis/Calculus/Deriv/Inverse): add `deriv_zero_of_frequently_mem` (#34576) …
Added HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNEView on Github →