Theorem HasDerivWithinAt.eventually_notMem

Modification history

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