analyticOn_const

Mathlib.Analysis.Analytic.Constructions

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

English

The constant function is analytic on any set.

Русский

Константная функция аналитична на любом множестве.

LaTeX

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

Lean4

theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s :=
  analyticOnNhd_const.analyticOn

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

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

Разделы

Аффилиация

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