IsZeroAtImInfty — Mathlib

English

A function f : ℍ → α is zero at infinity if it vanishes along atImInfty.

Русский

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

LaTeX

$$$\text{IsZeroAtImInfty}(f) \iff \text{ZeroAtFilter}(\text{atImInfty}, f)$$$

Lean4

/-- A function `f : ℍ → α` is zero at infinity it is zero along `atImInfty`. -/
def IsZeroAtImInfty {α : Type*} [Zero α] [TopologicalSpace α] (f : ℍ → α) : Prop :=
  ZeroAtFilter atImInfty f

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