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