English
For hf,hg continuous, the edistance between the continuous maps coincides with the edistance of their UniformFun representations.
Русский
Если hf,hg непрерывны, евдистантное расстояние между непрерывными отображениями совпадает с евдистантным расстоянием между их представлениями в UniformFun.
LaTeX
$$$edist( (\langle - , hf \rangle) , (\langle - , hg \rangle) ) = edist f g$$$
Lean4
noncomputable instance [BoundedSpace β] : BoundedSpace (α →ᵤ β) where
bounded_univ := by
rw [Metric.isBounded_iff_ediam_ne_top, ← lt_top_iff_ne_top]
refine lt_of_le_of_lt ?_ <| BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
simp only [EMetric.diam_le_iff, Set.mem_univ, edist_le, forall_const]
exact fun f g x ↦ EMetric.edist_le_diam_of_mem (Set.mem_univ _) (Set.mem_univ _)
