fderivWithin_const_sub — Mathlib

English

The derivative within s of the function y ↦ c − f(y) is equal to the negative of the derivative within s of f, i.e., fderivWithin 𝕜 (c − f(y)) s x = − fderivWithin 𝕜 f s x.

Русский

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

LaTeX

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

Lean4

theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
    fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x := by
  simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_fun_neg, hxs]

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