analyticOn

Mathlib.Analysis.Calculus.ContDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContDiffWithinAt.analyticOn

← MathLib Explorer

English

Analyticity within at a point from contDiffWithinAt.

Русский

аналитичность внутри точки из contDiffWithinAt.

LaTeX

$$$\displaystyle \text{AnalyticWithinAt 𝕜 f s x}$$$

Lean4

theorem analyticOn (h : ContDiffWithinAt 𝕜 ω f s x) : ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u :=
  by
  obtain ⟨u, hu, p, hp, h'p⟩ := h
  exact ⟨u, hu, hp.analyticOn (h'p 0)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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