English
On a domain with UniqueDiffOn, ContDiffOn (n+1) f s holds if and only if f is differentiable on s, and if n is finite or ω, the derivative is cont/diff accordingly and fderivWithin is ContDiffOn n.
Русский
На области с уникальными производными ContDiffOn (n+1) f s эквивалентно тому, что f дифференцируема на s, а производная удовлетворяет соответствующим условиям и fderivWithin ∈ ContDiffOn n.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 (n+1) f s \\iff \\Big( \\DifferentiableOn 𝕜 f s \\land (n = ω \\rightarrow AnalyticOn 𝕜 f s) \\land \\ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s \\Big)$$$
Lean4
protected theorem fderivWithin (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) :
ContDiffOn 𝕜 m (fderivWithin 𝕜 f s) s :=
((contDiffOn_succ_iff_fderivWithin hs).1 (hf.of_le hmn)).2.2
