isometry_toBCF

Mathlib.Topology.ContinuousMap.ZeroAtInfty

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

English

The map toBCF is an isometry from C0(α,β) into α→ᵇβ, preserving distance.

Русский

Преобразование toBCF является изометрией между C0(α,β) и пространством ограниченных непрерывных отображений α→ᵇβ.

LaTeX

$$Isometry(toBCF: C0(α,β) → α →ᵇ β)$$

Lean4

theorem isometry_toBCF : Isometry (toBCF : C₀(α, β) → α →ᵇ β) := by tauto

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

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

Разделы

Аффилиация

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