α : Type u_1
β : Type ?u.5645
inst✝ : EDist α
x y : α
s t : Set α
⊢ (¬∀ (C : ℝ≥0∞), 0 < C → ∃ x x_1 y x_2 _hxy, edist x y < C) ↔
    ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
α : Type u_1
β : Type ?u.5645
inst✝ : EDist α
x y : α
s t : Set α
⊢ 0 < einfsep s ↔ ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
rw [pos_iff_ne_zero, Ne.def, einfsep_zero]
no goals
α : Type u_1
β : Type ?u.5645
inst✝ : EDist α
x y : α
s t : Set α
⊢ (¬∀ (C : ℝ≥0∞), 0 < C → ∃ x x_1 y x_2 _hxy, edist x y < C) ↔
    ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
simp only [not_forall, not_exists, not_lt]