analyticWithinAt_univ

Mathlib.Analysis.Analytic.Basic

URI: https://scilib.ai/kg/mathlib#analyticWithinAt_univ

English

AnalyticWithinAt on the whole space is equivalent to AnalyticAt at a point.

Русский

Аналитичность внутри всего пространства эквивалентна аналитичности в точке.

LaTeX

$$$AnalyticWithinAt 𝕜 f univ x \\iff AnalyticAt 𝕜 f x$$$

Lean4

@[simp]
theorem analyticWithinAt_univ : AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by simp [AnalyticWithinAt, AnalyticAt]

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

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

Разделы

Аффилиация

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