fderiv_sub_const — Mathlib

English

The derivative of the function y ↦ f(y) − c at x equals the derivative of f at x: fderiv 𝕜 (f(·) − c) x = fderiv 𝕜 f x.

Русский

Производная функции y ↦ f(y) − c в точке x равна производной функции f в x.

LaTeX

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

Lean4

theorem fderiv_sub_const (c : F) : fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x := by
  simp only [sub_eq_add_neg, fderiv_add_const]

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