English
A function is C^(n+1) on a domain with unique derivatives iff it is differentiable there and its derivative is C^n; more generally, with ω and ∞ variants.
Русский
Функция является C^(n+1) на области с уникальными производными тогда и только тогда, когда она дифференцируема на области и её производная является C^n; анализ распространяется на ω и ∞ варианты.
LaTeX
$$$\\text{contDiffOn_succ_iff_fderivWithin} (hs) : ContDiffOn 𝕜 (n+1) f s \\iff \\text{DifferentiableOn } 𝕜 f s \\land (n = ω \\rightarrow AnalyticOn 𝕜 f s) \\land ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s$$$
Lean4
theorem fderiv_of_isOpen (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (fderiv 𝕜 f) s :=
(hf.fderivWithin hs.uniqueDiffOn hmn).congr fun _ hx => (fderivWithin_of_isOpen hs hx).symm
