no goals
α : Type u_1
β : Type ?u.1619
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s = 0 ↔ ∀ (C : ℝ≥0∞), 0 < C → ∃ x x_1 y x_2 _hxy, edist x y < C
simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff]