norm_toBCF_eq_norm

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.norm_toBCF_eq_norm

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

@[simp]
theorem norm_toBCF_eq_norm {f : C₀(α, β)} : ‖f.toBCF‖ = ‖f‖ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru