Commit 2023-12-09 12:32 5ef74df5

View on Github →

chore(Deriv): golf (#8899) Assorted golf I did while working on a refactor. Submitting as a separate PR.

Move not_differentiableAt_abs_zero to Calculus.Deriv.Add, golf.
Rename HasFDerivWithinAt_of_nhdsWithin_eq_bot to HasFDerivWithinAt.of_nhdsWithin_eq_bot, golf.
Protect Filter.EventuallyEq.rfl.
Golf here and there.

Estimated changes

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

added theorem not_differentiableAt_abs_zero

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

added theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot

deleted theorem HasFDerivWithinAt_of_nhdsWithin_eq_bot

modified theorem hasFDerivWithinAt_of_nmem_closure

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

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

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

deleted theorem not_differentiableAt_abs_zero

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.EventuallyEq.rfl

Modified Mathlib/Topology/ContinuousOn.lean

modified theorem continuousWithinAt_of_not_mem_closure