iteratedDerivWithin_eq_iteratedDeriv

English

If s has UniqueDiffOn and f is ContDiffAt of order n at x with x ∈ s, then iteratedDerivWithin n f s x equals iteratedDeriv n f x.

Русский

Если s удовлетворяет UniqueDiffOn, а f имеет ContDiffAt порядка n в точке x и x ∈ s, то iteratedDerivWithin n f s x равна iteratedDeriv n f x.

LaTeX

$$$ \text{UniqueDiffOn } 𝕜 s \to \; (\text{ContDiffAt } 𝕜 n f x) \to x \in s \Rightarrow iteratedDerivWithin n f s x = iteratedDeriv n f x $$$

Lean4

theorem iteratedDerivWithin_eq_iteratedDeriv (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 n f x) (hx : x ∈ s) :
    iteratedDerivWithin n f s x = iteratedDeriv n f x := by
  rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_eq_iteratedFDeriv hs h hx]

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