English
On a domain with UniqueDiffOn, ContDiffOn (n+1) f s is equivalent to differentiability of f on s and the existence of an f' with ContDiffOn n and HasFDerivWithinAt f (f' x) on s.
Русский
На области с уникальными дифференциаторами ContDiffOn (n+1) f s эквивалентно дифференцируемости f на s и существованию f' с ContDiffOn n и HasFDerivWithinAt f (f' x) на s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 (n+1) f s \\iff \\Big( \\text{DifferentiableOn } 𝕜 f s \\land \\exists f' : E \\to E \\toL[𝕜] F, \\ContDiffOn 𝕜 n f' s \\land \\forall x, x \\in s \\to HasFDerivWithinAt f (f' x) s x\\Big)$$$
Lean4
theorem continuousOn_fderivWithin (h : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hn : 1 ≤ n) :
ContinuousOn (fderivWithin 𝕜 f s) s :=
((contDiffOn_succ_iff_fderivWithin hs).1 (h.of_le (show 0 + (1 : WithTop ℕ∞) ≤ n from hn))).2.2.continuousOn
