α : Type u_1
β : Type ?u.39983
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} = min (edist x y) (edist x y)
α : Type u_1
β : Type ?u.39983
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} = edist x y
nth_rw 1 [← min_self (edist x y)]
case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.39983
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ edist x y = edist y x
α : Type u_1
β : Type ?u.39983
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} = min (edist x y) (edist x y)
convert einfsep_pair_eq_inf hxy using 2
no goals
case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.39983
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ edist x y = edist y x
rw [edist_comm]