English
The metric on FunSpace is the induced metric from its embedding into ContinuousMap, i.e., d(α,β) = sup_{t∈Icc(tmin,tmax)} ‖α(t)−β(t)‖.
Русский
Метрика на пространстве FunSpace является индуцированной через вложение в ContinuousMap: расстояние равно супремуму по t.
LaTeX
$$MetricSpace(FunSpace) is induced by toContinuousMap: d(α,β) = sup_{t∈Icc(tmin,tmax)} ‖α(t)−β(t)‖.$$
Lean4
/-- The metric between two curves `α` and `β` is the supremum of the metric between `α t` and `β t`
over all `t` in the domain. This is finite when the domain is compact, such as a closed
interval in our case. -/
noncomputable instance : MetricSpace (FunSpace t₀ x₀ r L) :=
MetricSpace.induced toContinuousMap toContinuousMap.injective inferInstance
