English
Let f: E → F be a differentiable map between normed spaces, and let a ∈ E. Then the Frechet derivative of the translated function x ↦ f(a + x) at x with respect to any set s is the Frechet derivative of f at the translated point a + x with respect to the translated set a + s.
Русский
Пусть f: E → F—отображение между нормированными пространствами, и возьмём a ∈ E. Тогда производная Фреше функции x ↦ f(a + x) внутри множества s в точке x равна производной функции f в точке a + x внутри множества a + s.
LaTeX
$$$Df(a+x) = D\bigl(y \mapsto f(a+y)\bigr)(x)$$$
Lean4
theorem fderivWithin_comp_add_left (a : E) :
fderivWithin 𝕜 (fun x ↦ f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x) := by
classical simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]
