Commit 2026-02-10 19:29 f4d59b3b

View on Github →

feat(Analysis/Calculus/Deriv/Inverse): add deriv_zero_of_frequently_mem (#34576) This PR proves that if a function frequently (in 𝓝[s ∖ {x}]) takes values in a set t that does not accumulate at f x, then its derivative at x equals zero. The application that I have in mind is where this set is closed and discrete (and thus has no accumulation points).

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Inverse.lean

added theorem HasDerivAt.eventually_notMem

added theorem HasDerivWithinAt.eventually_notMem

added theorem HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE

added theorem derivWithin_zero_of_frequently_mem

added theorem deriv_zero_of_frequently_mem

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

modified theorem HasFDerivAt.eventually_ne

added theorem HasFDerivAt.eventually_notMem

added theorem HasFDerivAt.tendsto_nhdsNE

added theorem HasFDerivWithinAt.eventually_notMem

added theorem HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE