toBCF — Mathlib

English

From a continuous function vanishing at infinity, construct the corresponding bounded continuous function. This yields a map to bounded continuous functions, i.e., a canonical transition to a bounded-continuous-function representation.

Русский

Из непрерывного отображения, стремящегося к нулю на бесконечности, строится соответствующая ограниченная непрерывная функция. Это даёт переход к представлению в виде ограниченных непрерывных отображений.

LaTeX

$$$toBCF:\\ C_0(\\alpha,\\beta) \\to C_b(\\alpha,\\beta)$$$

Lean4

/-- Construct a bounded continuous function from a continuous function vanishing at infinity. -/
@[simps!]
def toBCF (f : C₀(α, β)) : α →ᵇ β :=
  ⟨f, map_bounded f⟩

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