no goals
F : Type ?u.308003
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ (⨆ (x : α), dist (↑f x) (↑g x)) = ↑(⨆ (x : α), nndist (↑f x) (↑g x))
simp_rw [val_eq_coe, coe_iSup, coe_nndist]