∀ {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (f : C(α, β)) (C : ℝ),
  (∀ (x y : α), dist (f x) (f y) ≤ C) → ∃ C, ∀ (x y : α), dist (f.toFun x) (f.toFun y) ≤ C