α : Type u
β : Type v
X : Type ?u.4940
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
α : Type u
β : Type v
X : Type ?u.4940
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z
rw [edist_comm y]
no goals
α : Type u
β : Type v
X : Type ?u.4940
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
apply edist_triangle