English
Under UniqueDiffOn, ContDiffOn (n+1) f s is equivalent to differentiability of f on s and the existence of a linear map-valued f' with ContDiffOn n f' and HasFDerivWithinAt f (f' x) on s.
Русский
При UniqueDiffOn ContDiffOn (n+1) f s эквивалентно дифференцируемости f на s и существованию линейного отображения f' с ContDiffOn n f' и 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 \\in s, HasFDerivWithinAt f (f' x) s x\\Big)$$$
Lean4
theorem contDiffOn_infty_iff_fderiv_of_isOpen (hs : IsOpen s) :
ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s :=
by
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]
simp
