IsBoundedAtImInfty — Mathlib

English

A function f : ℍ → α is bounded at infinity if it is bounded along the filter atImInfty.

Русский

Функция f : ℍ → α ограничена вдоль фильтра atImInfty, то есть при стремлении к бесконечности вдоль мнимой оси.

LaTeX

$$$\text{IsBoundedAtImInfty}(f) \;\equiv\; BoundedAtFilter(\text{atImInfty}, f)$$$

Lean4

/-- A function `f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`. -/
def IsBoundedAtImInfty {α : Type*} [Norm α] (f : ℍ → α) : Prop :=
  BoundedAtFilter atImInfty f

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