iteratedFDerivWithin_comp_add_left

English

A direct corollary of the previous result: the equality with the shifted input holds for all n, a, x.

Русский

Прямой следствия из предыдущего результата: равенство со сдвинутым аргументом выполняется для всех n, a, x.

LaTeX

$$$\forall n\ a\ x:\ iteratedFDerivWithin 𝕜 n (\lambda z, f(a+z)) s x = iteratedFDerivWithin 𝕜 n f (a+ᵥ s) (a+x)$$$

Lean4

/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
theorem iteratedFDerivWithin_comp_add_left (n : ℕ) (a : E) (x : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x) := by
  simp [iteratedFDerivWithin_comp_add_left']

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