English
If s is open, ContDiffOn ∞ f s is equivalent to differentiability on s and fderiv being ContDiffOn ∞ on s.
Русский
Если s открыто, ContDiffOn ∞ f s эквивалентно дифференцируемости на s и ContDiffOn ∞ (fderiv 𝕜 f) s.
LaTeX
$$$\\text{IsOpen } s \\Rightarrow \\ContDiffOn 𝕜 ∞ f s \\iff \\big( \\text{DifferentiableOn } 𝕜 f s \\land \\ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s \\big)$$$
Lean4
/-- A function is `C^(n + 1)` on an open domain if and only if it is
differentiable there, and its derivative (expressed with `fderiv`) is `C^n`. -/
theorem contDiffOn_succ_iff_fderiv_of_isOpen (hs : IsOpen s) :
ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) s := by
rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn, contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]
