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