no goals
α : Type u_1
β : Type ?u.46357
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ einfsep {x, y, z} = edist x y ⊓ edist x z ⊓ edist y z
simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
  ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]