no goals
F : Type ?u.306222
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : IsEmpty α
⊢ dist f g = 0
rw [(ext isEmptyElim : f = g), dist_self]