English
Same as 44019 but stated explicitly for nat-indexed ContDiff.
Русский
То же самое, изложенное явно для натурального индекса ContDiff.
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}\ n\ f \iff \Big(\forall m : \mathbb{N}, m \le n \Rightarrow \operatorname{Continuous}\ (x \mapsto \operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f\ x)\Big) \land \Big(\forall m : \mathbb{N}, m < n \Rightarrow \operatorname{Differentiable}_{\mathbb{K}} (\operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f)\Big)$$
Lean4
theorem contDiff_of_differentiable_iteratedFDeriv {n : ℕ∞}
(h : ∀ m : ℕ, m ≤ n → Differentiable 𝕜 (iteratedFDeriv 𝕜 m f)) : ContDiff 𝕜 n f :=
contDiff_iff_continuous_differentiable.2 ⟨fun m hm => (h m hm).continuous, fun m hm => h m (le_of_lt hm)⟩