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