iteratedFDeriv_right — Mathlib

English

Alternative formulation: fderiv_right_succ expresses that fderiv is contDiff of order n.

Русский

Альтернативная формулировка: fderiv_right_succ выражает гладкость fderiv порядка n.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n f \Rightarrow \operatorname{ContDiff}_{\mathbb{K}} n (fderiv 𝕜 f)$$$

Lean4

theorem iteratedFDeriv_right {i : ℕ} (hf : ContDiff 𝕜 n f) (hmn : m + i ≤ n) : ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f) :=
  contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.iteratedFDeriv_right hmn

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