analyticOn_id

Mathlib.Analysis.Analytic.Linear

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

English

The identity map id: E → E is analytic on any set s; i.e., AnalyticOn 𝕜 id s.

Русский

Отображение id: E → E аналитично на любом множестве s; то есть AnalyticOn 𝕜 id s.

LaTeX

$$$AnalyticOn 𝕜 (id : E \\to E) s$$$

Lean4

theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s := fun _ _ ↦ analyticWithinAt_id

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

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

Разделы

Аффилиация

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