English
If x lies in the domain interior to s with a unique differentiability point, then the derivative within s of −f at x equals the negation of the derivative within s of f at x.
Русский
Пусть x является точкой внутри s с уникальной точкой дифференцирования; производная внутри s от −f в x равна минусу производной внутри s от f в x.
LaTeX
$$$fderivWithin_{\mathbb{K}}(-f)\, s\, x = -\, fderivWithin_{\mathbb{K}} f\, s\, x$$$
Lean4
theorem fderivWithin_fun_neg (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x := by
classical
by_cases h : DifferentiableWithinAt 𝕜 f s x
· exact h.hasFDerivWithinAt.neg.fderivWithin hxs
· rw [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]
simpa
