iterate_deriv'

Mathlib.Analysis.Calculus.ContDiff.Basic

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

← MathLib Explorer

English

If f is ContDiff, then its deriv is ContDiff.

Русский

Если f — ContDiff, то deriv f — ContDiff.

LaTeX

$$$ContDiff 𝕜 n f_2 \Rightarrow ContDiff 𝕜 n (deriv f_2)$$$

Lean4

@[fun_prop]
theorem iterate_deriv' (n : ℕ) : ∀ (k : ℕ) {f₂ : 𝕜 → F}, ContDiff 𝕜 (n + k : ℕ) f₂ → ContDiff 𝕜 n (deriv^[k] f₂)
  | 0, _, hf => hf
  | k + 1, _, hf => ContDiff.iterate_deriv' _ k (contDiff_succ_iff_deriv.mp hf).2.2

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

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

Разделы

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

Аффилиация

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