differentiable_iteratedDeriv — Mathlib

English

If f is ContDiff 𝕜 n f and m < n, then iteratedDeriv m f is differentiable 𝕜 on s.

Русский

Если f ∈ ContDiff 𝕜 n f и m < n, то iteratedDeriv m f дифференцируема по 𝕜 на s.

LaTeX

$$ContDiff 𝕜 n f → m < n → Differentiable 𝕜 (iteratedDeriv m f)$$

Lean4

theorem differentiable_iteratedDeriv {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : m < n) :
    Differentiable 𝕜 (iteratedDeriv m f) :=
  (contDiff_iff_iteratedDeriv.1 (h.of_le (ENat.add_one_natCast_le_withTop_of_lt hmn))).2 m (mod_cast (lt_add_one m))

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