fderiv_right — Mathlib

English

One can iterate derivatives within a set and retain contDiff at the base point.

Русский

Можно продолжать дифференцирование внутри множества, сохранив ContDiff на базовой точке.

LaTeX

$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}} n (\text{iteratedFDerivWithin } 𝕜 i f s) \ s x_0$$$

Lean4

/-- `fderiv 𝕜 f` is smooth at `x₀`. -/
theorem fderiv_right (hf : ContDiffAt 𝕜 n f x₀) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (fderiv 𝕜 f) x₀ :=
  ContDiffAt.fderiv (ContDiffAt.comp (x₀, x₀) hf contDiffAt_snd) contDiffAt_id hmn

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