English
For ENat-n, ContDiffWithinAt 𝕜 n f s x can be characterized by HasFTaylorSeriesUpToOn and an ω-analytic constraint when n equals ω.
Русский
Для ENat-числа ContDiffWithinAt 𝕜 n f s x описывается через HasFTaylorSeriesUpToOn и аналитическое условие при n = ω.
LaTeX
$$$ ContDiffWithinAt 𝕜 n f s x \\iff \\exists u \\in 𝓝[insert x s] x, \\exists p : E \\to \\text{FormalMultilinearSeries } 𝕜 E F, HasFTaylorSeriesUpToOn n f p u ∧ (n = ω \\to \\forall i, AnalyticOn 𝕜 (fun z => p z i) u)$$
Lean4
/-- In a complete space, a function which is analytic within a set at a point is also `C^ω` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`. -/
theorem contDiffWithinAt [CompleteSpace F] (h : AnalyticWithinAt 𝕜 f s x) : ContDiffWithinAt 𝕜 n f s x :=
(contDiffWithinAt_omega_iff_analyticWithinAt.2 h).of_le le_top
