boundedAtImInftySubalgebra — Mathlib

English

The subalgebra of functions ℍ → α which are bounded at ImInfty is formed by restricting the boundedness along atImInfty to the algebra operations.

Русский

Подалгебра функций ℍ → α ограниченных на ImInfty образована из функций, ограниченных вдоль atImInfty под операциями алгебры.

LaTeX

$$$\text{boundedAtImInftySubalgebra}(\alpha) = \text{boundedFilterSubalgebra}(\text{atImInfty})$$$

Lean4

/-- Subalgebra of functions that are bounded at infinity. -/
def boundedAtImInftySubalgebra (α : Type*) [NormedField α] : Subalgebra α (ℍ → α) :=
  boundedFilterSubalgebra _ atImInfty

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