contDiff_of_differentiable_iteratedFDeriv

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)⟩

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