fderiv_right — Mathlib

English

If f is C^{n}, then fderiv_right holds for successor indices.

Русский

Если f ∈ C^n, то выполняется fderiv_right для следующего индекса.

LaTeX

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

Lean4

/-- `fderiv 𝕜 f` is smooth. -/
theorem fderiv_right (hf : ContDiff 𝕜 n f) (hmn : m + 1 ≤ n) : ContDiff 𝕜 m (fderiv 𝕜 f) :=
  contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.fderiv_right hmn

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