fderivWithin_sub_const — Mathlib

English

The derivative inside s of the function y ↦ f(y) − c equals the derivative inside s of f, i.e., fderivWithin 𝕜 (f(·) − c) s x = fderivWithin 𝕜 f s x.

Русский

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

LaTeX

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

Lean4

theorem fderivWithin_sub_const (c : F) : fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x := by
  simp only [sub_eq_add_neg, fderivWithin_add_const]

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