analyticAt_of_mem — Mathlib

English

If a ball has an origin-change power series, then the analytic property holds on a neighborhood of every point in that ball.

Русский

Если существует степенной ряд через изменение начала, то аналитичность сохраняется в окрестности каждой точки внутри шара.

LaTeX

$$HasFPowerSeriesOnBall f p x r \\Rightarrow AnalyticOnNhd 𝕜 f (EMetric.ball x r)$$

Lean4

/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball. -/
theorem analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r) (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y :=
  by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  rw [← analyticWithinAt_univ]
  exact hf.analyticWithinAt_of_mem (by simpa using h)

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