continuous_iteratedDeriv — Mathlib

English

Equivalent reformulation of contDiff_nat_iff_iteratedDeriv with simplifications.

Русский

Эквивалентная формулировка contDiff_nat_iff_iteratedDeriv с упрощениями.

LaTeX

$$Iff simplification of contDiff_nat_iff_iteratedDeriv using simp$$

Lean4

theorem continuous_iteratedDeriv {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : m ≤ n) :
    Continuous (iteratedDeriv m f) :=
  (contDiff_iff_iteratedDeriv.1 (h.of_le hmn)).1 m le_rfl

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