atImInfty — Mathlib

English

The filter atImInfty is the filter on the upper half-plane that captures approaching infinity along the imaginary axis.

Русский

Фильтр atImInfty задаёт поведение функций при стремлении к бесконечности вдоль мнимой оси на множестве верхней полуплоскости.

LaTeX

$$$\text{atImInfty} = \text{Filter.atTop} \circ \text{comap}(\operatorname{im})$$$

Lean4

/-- Filter for approaching `i∞`. -/
def atImInfty :=
  Filter.atTop.comap UpperHalfPlane.im

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