isometry_toContinuousMap — Mathlib

English

The natural map that sends a basepoint-preserving continuous map to its underlying continuous map is distance-preserving between the metric spaces C(α, R)₀ and C(α, R). In particular, for f,g ∈ C(α, R)₀, d_{C₀}(f,g) = d_{C}(toContinuousMap f, toContinuousMap g).

Русский

Естественное отображение, отправляющее базисно-фиксированное непрерывное отображение в его базовое непрерывное отображение, сохраняет расстояния между точками; т.е. между пространствами C(α, R)₀ и C(α, R) сохраняется метрическое расстояние: d_{C₀}(f,g)=d_{C}(toContinuousMap f, toContinuousMap g).

LaTeX

$$$d_{C_0}(f,g)=d_{C}(toContinuousMap\,f,\;toContinuousMap\,g).$$$

Lean4

theorem isometry_toContinuousMap [MetricSpace R] [Zero R] : Isometry (toContinuousMap : C(α, R)₀ → C(α, R)) := fun _ _ ↦
  rfl

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