English
Let α be a compact space with a distinguished base point and R a metric space. The space C(α, R)₀ of basepoint-preserving continuous maps α → R carries a metric inherited from the ambient metric on C(α, R) via the natural embedding. Equivalently, the distance between f and g in C(α, R)₀ is the sup over α of the distance in R: d(f,g) = sup_{x∈α} d_R(f(x), g(x)).
Русский
Пусть α – компактное пространство с базовой точкой и R – метрическое пространство. Пространство C(α, R)₀ базисно-фиксированных непрерывных отображений α → R наследует метрику из пространства C(α, R) через естественное вложение. Эквивалентно, расстояние между f и g в C(α, R)₀ равно d(f,g) = sup_{x∈α} d_R(f(x), g(x)).
LaTeX
$$$d_{C_0}(f,g)=\\sup_{x\\in\\alpha} d_R(f(x),g(x)).$$$
Lean4
noncomputable instance [MetricSpace R] [Zero R] : MetricSpace C(α, R)₀ :=
ContinuousMapZero.isUniformEmbedding_toContinuousMap.comapMetricSpace _
