α : Type u_1
β : Type ?u.61000
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
⊢ ENNReal.toReal (ENNReal.ofReal (dist x y)) = dist x y
α : Type u_1
β : Type ?u.61000
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
⊢ infsep {x, y} = dist x y
rw [infsep_pair_eq_toReal, edist_dist]
no goals
α : Type u_1
β : Type ?u.61000
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
⊢ ENNReal.toReal (ENNReal.ofReal (dist x y)) = dist x y
exact ENNReal.toReal_ofReal dist_nonneg