mfderiv_neg — Mathlib

English

The derivative of the negated function equals the negation of the derivative of the function.

Русский

Производная отрицательной функции равна отрицательной производной функции.

LaTeX

$$$mfderiv I 𝓘(𝕜,E')( -f) x = - mfderiv I 𝓘(𝕜,E') f x$ for all x.$$

Lean4

theorem mfderiv_neg (f : M → E') (x : M) :
    (mfderiv I 𝓘(𝕜, E') (-f) x : TangentSpace I x →L[𝕜] E') = (-mfderiv I 𝓘(𝕜, E') f x : TangentSpace I x →L[𝕜] E') :=
  by
  simp_rw [mfderiv]
  by_cases hf : MDifferentiableAt I 𝓘(𝕜, E') f x
  · exact hf.hasMFDerivAt.neg.mfderiv
  · rw [if_neg hf]; rw [← mdifferentiableAt_neg] at hf; rw [if_neg hf, neg_zero]

Похожие утверждения