exists_ball_analyticOnNhd — Mathlib

English

If f is analytic at x, then there exists a radius r > 0 such that f is analytic on the ball B(x,r) in a neighborhood of x.

Русский

Если f аналитична в x, то существует радиус r > 0, такой что f аналитична на шаре B(x,r).

LaTeX

$$$\\exists r>0: \\ AnalyticOnNhd_{\\mathbb{K}}(f, \\mathrm{Ball}(x,r)).$$$

Lean4

/-- If we're analytic at a point, we're analytic in a nonempty ball -/
theorem exists_ball_analyticOnNhd (h : AnalyticAt 𝕜 f x) : ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r) :=
  Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h

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