fderivWithin_neg — Mathlib

English

For a function f and a set s, the derivative within s of −f at x equals the negation of the derivative within s of f at x, under the same differentiability conditions as above.

Русский

Для функции f и множества s производная внутри s от −f в точке x равна минусу производной внутри s от f в точке x при тех же условиях дифференцируемости.

LaTeX

$$$fderivWithin_{\mathbb{K}}(-f)\, s\, x = -\, fderivWithin_{\mathbb{K}} f\, s\, x$$$

Lean4

theorem fderivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (-f) s x = -fderivWithin 𝕜 f s x :=
  fderivWithin_fun_neg hxs

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