English
A function is C^∞ (ContDiff 𝕜 ∞) if and only if it is differentiable and its derivative fderiv 𝕜 f is C^∞.
Русский
Функция бесконечно дифференцируема тогда и только тогда, когда она дифференцируема и её производная тоже бесконечно дифференцируема.
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}\ infinity\ f \iff \operatorname{Differentiable}_{\mathbb{K}} f \land \operatorname{ContDiff}_{\mathbb{K}}\ infinity\ (fderiv_{\mathbb{K}} f)$$$
Lean4
/-- A function is `C^(n + 1)` if and only if it is differentiable,
and its derivative (formulated in terms of `fderiv`) is `C^n`. -/
theorem contDiff_succ_iff_fderiv :
ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 n (fderiv 𝕜 f) := by
simp only [← contDiffOn_univ, ← differentiableOn_univ, ← fderivWithin_univ,
contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ, analyticOn_univ]
