Theorem HasFDerivWithinAt.eventually_notMem

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.eventually_notMemView on Github →