no goals
α : Type u
β : Type v
X : Type ?u.22805
ι : Type ?u.22808
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]