fderivWithin_comp_sub — Mathlib

English

For a, HasFDerivWithinAt for f( x − a) is equivalent to HasFDerivWithinAt for f at x − a with translated set.

Русский

Для функции f( x − a ) условие существования производной внутри задаётся эквивалентно условию для f в точке x − a с перенесённым множеством.

LaTeX

$$$\text{HasFDerivWithinAt}(f(\cdot - a), f', s, x) \iff \text{HasFDerivWithinAt}(f, f', ( -a) + s, x-a)$$$

Lean4

theorem fderivWithin_comp_sub (a : E) : fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a) :=
  by simpa [sub_eq_add_neg] using fderivWithin_comp_add_right (-a)

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