English
AnalyticWithinAt 𝕜 f s x is equivalent to the existence of a local analytic extension g with f and g agreeing on insert x s and g analytic at x.
Русский
AnalyticWithinAt 𝕜 f s x эквивалентно существованию локального аналитического продолжения g, которое согласуется с f на insert x s и аналитично в точке x.
LaTeX
$$$AnalyticWithinAt 𝕜 f s x \iff \exists g, f =^\mathrm{ᶠ}[𝓝[insert x s] x] g \land AnalyticAt 𝕜 g x$$$
Lean4
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x` -/
theorem analyticWithinAt_iff_exists_analyticAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
AnalyticWithinAt 𝕜 f s x ↔ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x :=
by
simp only [AnalyticWithinAt, AnalyticAt, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt]
tauto
