no goals
α : Type u_1
β : Type u_2
E : Type ?u.76000
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, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]