isOpen_analyticAt — Mathlib

English

The property of analyticity is stable under small perturbations; the set of analytic points is open in the ambient space.

Русский

Свойство аналитичности сохраняется при маленьких возмущениях; множество точек аналитических является открытым.

LaTeX

$$$\\text{IsOpen} \\{x \\;|\\; AnalyticAt 𝕜 f x\\}$$$

Lean4

/-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such
that `f` is analytic at `x` is open. -/
theorem isOpen_analyticAt : IsOpen {x | AnalyticAt 𝕜 f x} :=
  by
  rw [isOpen_iff_mem_nhds]
  rintro x ⟨p, r, hr⟩
  exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy

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