Theorems · Theorem · general topology

ContinuousMap.isometryEquivBoundedOfCompact_apply

∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ⇑(ContinuousMap.isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpacePseudoMetricSpace