isBoundedAtImInfty

Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty

English

If f is zero at ImInfty, then f is bounded at ImInfty.

Русский

Если f обращается в ноль на бесконечности, то она ограничена на бесконечности.

LaTeX

$$IsZeroAtImInfty(f) ⇒ IsBoundedAtImInfty(f)$$

Lean4

theorem isBoundedAtImInfty {α : Type*} [SeminormedAddGroup α] {f : ℍ → α} (hf : IsZeroAtImInfty f) :
    IsBoundedAtImInfty f :=
  hf.boundedAtFilter

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

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

Разделы

Аффилиация

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