English
If f is analytic on s and s has UniqueDiffOn, then f is ContDiffOn 𝕜 n f s for any n.
Русский
Если f аналитична на s и для s верна уникальность дифференцируемости, то f ∈ ContDiffOn 𝕜 n f s для любого n.
LaTeX
$$$AnalyticOn\\ 𝕜\\ f\\ s \\rightarrow UniqueDiffOn\\ 𝕜\\ s \\rightarrow ContDiffOn\\ 𝕜\\ n\\ f\\ s$$$
Lean4
/-- On a set with unique differentiability, an analytic function is automatically `C^ω`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOn.contDiffOn_of_completeSpace`. -/
theorem contDiffOn (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 n f s :=
by
suffices ContDiffOn 𝕜 ω f s from this.of_le le_top
rcases h.exists_hasFTaylorSeriesUpToOn hs with ⟨p, hp⟩
intro x hx
refine ⟨s, ?_, p, hp⟩
rw [insert_eq_of_mem hx]
exact self_mem_nhdsWithin
