Theorems · Theorem · general topology

UniformOnFun.edist_continuousRestrict_of_singleton

∀ {α : 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.domRestrict ((UniformOnFun.toFun {s}) f), continuous_toFun := ⋯ }
      { toFun := s.domRestrict ((UniformOnFun.toFun {s}) g), continuous_toFun := ⋯ } =
    edist f g

Defined in

Mathlib.Topology.MetricSpace.UniformConvergence

Cited by

2 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceTopologicalSpaceCompactSpace