analyticWithinAt — Mathlib

English

If a function f has a formal power series p within a set s at x, then f is analytic within s at x.

Русский

Если функция f имеет формальную степенную серию p внутри множества s около точки x, то она аналитична внутри s в точке x.

LaTeX

$$$HasFPowerSeriesWithinAt\ f\ p\ s\ x \Rightarrow AnalyticWithinAt\ 𝕜\ f\ s\ x$$$

Lean4

theorem analyticWithinAt (hf : HasFPowerSeriesWithinAt f p s x) : AnalyticWithinAt 𝕜 f s x :=
  ⟨p, hf⟩

Похожие утверждения