deriv_sub_const — Mathlib

English

For any c, the derivative of the function y ↦ c − f(y) at x equals the negative of the derivative of f at x.

Русский

Для любой константы c производная функции y ↦ c − f(y) в точке x равна минусу производной f в точке x.

LaTeX

$$$$ \operatorname{deriv}(\lambda y, c - f(y)) x = -\operatorname{deriv} f x. $$$$

Lean4

theorem deriv_sub_const (c : F) : deriv (fun y ↦ f y - c) x = deriv f x := by simp only [deriv, fderiv_sub_const]

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