analyticOn — Mathlib

English

If a function has a power-series expansion on a ball around x, then it is analytic at y provided y ∈ x+s with an appropriate origin-change and radius offset.

Русский

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

LaTeX

$$$HasFPowerSeriesWithinOnBall f p s x r \\Rightarrow AnalyticWithinAt 𝕜 f s y$ under appropriate membership conditions$$

Lean4

theorem analyticOn (hf : HasFPowerSeriesWithinOnBall f p s x r) : AnalyticOn 𝕜 f (insert x s ∩ EMetric.ball x r) :=
  fun _ hy ↦ ((analyticWithinAt_insert (y := x)).2 (hf.analyticWithinAt_of_mem hy)).mono inter_subset_left

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