zeroAtImInftySubmodule — Mathlib

English

The set of functions ℍ → α that vanish at infinity forms a submodule of all functions ℍ → α.

Русский

Набор функций ℍ → α, обращающихся в ноль на бесконечности, образует подмодуль над полем α.

LaTeX

$$$\text{zeroAtImInftySubmodule}(\alpha) = \{ f : \mathbb{H} \to \alpha \mid \text{IsZeroAtImInfty}(f) \}$$$

Lean4

/-- Module of functions that are zero at infinity. -/
def zeroAtImInftySubmodule (α : Type*) [NormedField α] : Submodule α (ℍ → α) :=
  zeroAtFilterSubmodule _ atImInfty

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