differentiable_iteratedDeriv' — Mathlib

English

If f is C^(m+1) on its domain, then the m-th iterated derivative of f is differentiable.

Русский

Пусть f имеет гладкость C^(m+1). Тогда m-я повторная производная f дифференцируема.

LaTeX

$$$\\forall m \\in \\mathbb{N},\\; \\ContDiff 𝕜 (m+1) f \\Rightarrow \\Differentiable 𝕜 (iteratedDeriv m f)$$$

Lean4

@[fun_prop]
theorem differentiable_iteratedDeriv' (m : ℕ) (h : ContDiff 𝕜 (m + 1) f) : Differentiable 𝕜 (iteratedDeriv m f) :=
  h.differentiable_iteratedDeriv m (Nat.cast_lt.mpr m.lt_succ_self)

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