zero_form_isBoundedAtImInfty

Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.zero_form_isBoundedAtImInfty

English

The zero function f ≡ 0 is bounded at ImInfty for any NormedField α.

Русский

Нулевая функция ограничена при ImInfty для любого нормированного поля α.

LaTeX

$$$\text{IsBoundedAtImInfty}(0 : \mathbb{H} \to \alpha)$$$

Lean4

theorem zero_form_isBoundedAtImInfty {α : Type*} [NormedField α] : IsBoundedAtImInfty (0 : ℍ → α) :=
  const_boundedAtFilter atImInfty (0 : α)

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

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

Разделы

Аффилиация

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