instNormedSpace — Mathlib

English

The norm of a zero-at-infinity map equals the norm of its bounded-continuous representation: ||f|| = ||f.toBCF||.

Русский

Норма отображения vanishing at infinity равна норме его ограниченного непрерывного представления: ||f|| = ||f.toBCF||.

LaTeX

$$$\\|f\\| = \\|f^{\\mathrm{toBCF}}\\|$$$

Lean4

noncomputable instance : NormedSpace 𝕜 C₀(α, β) where norm_smul_le k f := norm_smul_le k f.toBCF

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