contDiff_iff_continuous_differentiable

English

ContDiff 𝕜 ω f holds iff AnalyticOnNhd 𝕜 f univ.

Русский

ContDiff 𝕜 ω f имеет место тогда и только тогда, когда AnalyticOnNhd 𝕜 f univ.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}\omega\ f \iff \operatorname{AnalyticOnNhd}_{\mathbb{K}}\ f\ univ$$$

Lean4

theorem contDiff_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
  simp [contDiffOn_univ.symm, continuousOn_univ, differentiableOn_univ.symm, iteratedFDerivWithin_univ,
    contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ]

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