analyticOnNhd_const

Mathlib.Analysis.Analytic.Constructions

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

English

The constant map is analytic on every neighborhood, i.e., analytic in nhds of every point.

Русский

Константная функция аналитична на любой окрестности, то есть в любой nhds точки.

LaTeX

$$$AnalyticOnNhd\\ 𝕜(\\lambda x. c) S$$$

Lean4

theorem analyticOnNhd_const {v : F} {s : Set E} : AnalyticOnNhd 𝕜 (fun _ => v) s := fun _ _ => analyticAt_const

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

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

Разделы

Аффилиация

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