continuous_iteratedFDeriv' — Mathlib

English

If ∀ m, m ≤ n → Differentiable iteratedFDeriv 𝕜 m f, then ContDiff 𝕜 (WithTop.some n) f.

Русский

Если для каждого m выполняется условие, что iteratedFDeriv m f дифференцируем, тогда f ∈ C^n (с корректной обводкой)

LaTeX

$$$\forall m : \mathbb{N}, m \le n \Rightarrow \operatorname{Differentiable}_{\mathbb{K}} (\operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f) \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}\ (\mathrm{WithTop}.some\ n)\ f$$$

Lean4

@[fun_prop]
theorem continuous_iteratedFDeriv' {m : ℕ} (hf : ContDiff 𝕜 m f) : Continuous fun x => iteratedFDeriv 𝕜 m f x :=
  (contDiff_iff_continuous_differentiable.mp hf).1 m le_rfl

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