∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α] {s : Set α}
  {f g : UniformOnFun α β {s}} [inst_2 : CompactSpace ↑s] (hf : ContinuousOn ((UniformOnFun.toFun {s}) f) s)
  (hg : ContinuousOn ((UniformOnFun.toFun {s}) g) s),
  edist { toFun := s.restrict ((UniformOnFun.toFun {s}) f), continuous_toFun := ⋯ }
      { toFun := s.restrict ((UniformOnFun.toFun {s}) g), continuous_toFun := ⋯ } =
    edist f g