continuous_iteratedDeriv'

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

URI: https://scilib.ai/kg/mathlib#ContDiff.continuous_iteratedDeriv'

← MathLib Explorer

English

If ContDiff 𝕜 m f, then the function iteratedDeriv m f is continuous.

Русский

Если f ∈ ContDiff 𝕜 m, то iteratedDeriv m f непрерывна.

LaTeX

$$ContDiff 𝕜 m.cast f → Continuous (iteratedDeriv m f)$$

Lean4

@[fun_prop]
theorem continuous_iteratedDeriv' (m : ℕ) (h : ContDiff 𝕜 m f) : Continuous (iteratedDeriv m f) :=
  ContDiff.continuous_iteratedDeriv m h (le_refl _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru