fderiv_const_sub — Mathlib

English

The derivative of the function y ↦ c − f(y) is − f'(y), i.e., fderiv 𝕜 (c − f(y)) x = − fderiv 𝕜 f x.

Русский

Производная функции y ↦ c − f(y) равна − производной f: fderiv 𝕜 (c − f(y)) x = − fderiv 𝕜 f x.

LaTeX

$$$ fderiv 𝕜 (\\lambda y, c - f(y)) x = -\, fderiv 𝕜 f x $$$

Lean4

theorem fderiv_const_sub (c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x := by
  simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]

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