no goals
α : Type u
β : Type v
X : Type ?u.226694
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ Inseparable x y ↔ edist x y = 0
simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_lt_iff_le']