iterate_deriv — Mathlib

English

Iterating the derivative preserves ContDiff under the right hypotheses.

Русский

Повторение дифференциирования сохраняет ContDiff при надлежащих условиях.

LaTeX

$$$\forall n\ ContDiff 𝕜 \infty f_2 \Rightarrow ContDiff 𝕜 \infty (Nat.iterate deriv\ n\ f_2)$$$

Lean4

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

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