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]