Commit 2025-05-20 16:05 d86ef35c

View on Github →

feat(Deriv/Basic): add EventuallyEq.derivWithin_eq_of_* (#25048) Also rename Filter.EventuallyEq.fderivWithin_eq_nhds to Filter.EventuallyEq.fderivWithin_eq_of_nhds to sync with other similar lemmas.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

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

added theorem Filter.EventuallyEq.derivWithin_eq_of_mem

added theorem Filter.EventuallyEq.derivWithin_eq_of_nhds

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

deleted theorem Filter.EventuallyEq.fderivWithin_eq_nhds

added theorem Filter.EventuallyEq.fderivWithin_eq_of_nhds

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