English
For any n ∈ ℕ, a ∈ E, and x ∈ E, the n-th iterated derivative within s of the translated function z ↦ f(z + a) evaluated at x equals the n-th iterated derivative of f on a translated set a + s evaluated at x + a: iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a).
Русский
Для любых n, a и x верно то же равенство перехода на сдвиг без явного указания s: iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a).
LaTeX
$$$\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n}(\lambda z\,. f(z+a))\,s\,x = \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n} f\ (a+ᵥ s)\ (x+a)$$$
Lean4
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
theorem iteratedFDerivWithin_comp_add_right (n : ℕ) (a : E) (x : E) :
iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a) := by
simp [iteratedFDerivWithin_comp_add_right']
