AnalyticWithinAt — Mathlib

English

If a function has a power series on a ball, then it is analytic at the center.

Русский

Если функция имеет степенной ряд на шаре, то она аналитична в центре.

LaTeX

$$$ HasFPowerSeriesAt f p x \Rightarrow AnalyticAt 𝕜 f x $$$

Lean4

/-- `f` is analytic within `s` at `x` if it has a power series at `x` that converges on `𝓝[s] x` -/
def AnalyticWithinAt (f : E → F) (s : Set E) (x : E) : Prop :=
  ∃ p : FormalMultilinearSeries 𝕜 E F, HasFPowerSeriesWithinAt f p s x

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