analyticOnNhd

Mathlib.Analysis.Analytic.ChangeOrigin

URI: https://scilib.ai/kg/mathlib#HasFPowerSeriesOnBall.analyticOnNhd

English

The set of points where a function is analytic is an open subset of the domain.

Русский

Множество точек аналитичности функции открыто в области определения.

LaTeX

$$$\\{x\\;|\\; AnalyticAt 𝕜 f x\\}$ is open$$

Lean4

theorem analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) : AnalyticOnNhd 𝕜 f (EMetric.ball x r) := fun _y hy =>
  hf.analyticAt_of_mem hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru