Theorems · Theorem · general topology

UniformFun.edist_continuousMapMk

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α] [inst_2 : CompactSpace α]
  {f g : UniformFun α β} (hf : Continuous (UniformFun.toFun f)) (hg : Continuous (UniformFun.toFun g)),
  edist { toFun := UniformFun.toFun f, continuous_toFun := hf }
      { toFun := UniformFun.toFun g, continuous_toFun := hg } =
    edist f g

Defined in

Mathlib.Topology.MetricSpace.UniformConvergence

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceTopologicalSpaceCompactSpace