comp_sub_const — Mathlib

English

Let f: 𝕜 → F. If f has derivative f' at x − a, then the function x ↦ f(x − a) has derivative f' at x.

Русский

Пусть f: 𝕜 → F. Если у f в точке x − a существует производная f', то функция x ↦ f(x − a) имеет ту же производную f' в точке x.

LaTeX

$$$\\text{If } \\mathrm{HasDerivAt}(f,f',x-a) \\text{ then } \\mathrm{HasDerivAt}\\left(\\lambda x, f(x-a)\\right) f' x$$$

Lean4

/-- Translation in the domain does not change the derivative. -/
theorem comp_sub_const (x a : 𝕜) (hf : HasDerivAt f f' (x - a)) : HasDerivAt (fun x ↦ f (x - a)) f' x := by
  simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.sub_const a

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