no goals
α : Type u_2
β : Type u_1
E : Type ?u.70790
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
x : α
⊢ dist (↑f x) (↑g x) ≤ dist f g
simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]