derivWithin_sub_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem derivWithin_sub_const (c : F) : derivWithin (fun y ↦ f y - c) s x = derivWithin f s x := by
  simp only [derivWithin, fderivWithin_sub_const]

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