contDiff_nat_iff_continuous_differentiable

English

If m ≤ n and f is ContDiff 𝕜 n f, then the map x ↦ iteratedFDeriv 𝕜 m f x is continuous.

Русский

Если m ≤ n и f ∈ C^n, то x ↦ iteratedFDeriv m f x непрерывна.

LaTeX

$$$\forall m\in\mathbb{N},\ m\le n\Rightarrow \operatorname{ContDiff}_{\mathbb{K}}\ n\ f \Rightarrow \operatorname{Continuous}\ (x \mapsto \operatorname{iteratedFDeriv}_{\mathbb{K}}\ m\ f\ x)$$$

Lean4

theorem contDiff_nat_iff_continuous_differentiable {n : ℕ} :
    ContDiff 𝕜 n f ↔
      (∀ m : ℕ, m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
        ∀ m : ℕ, m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x :=
  by
  rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]
  simp

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