α : Type u_1
β : Type ?u.52764
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ 0 < einfsep s
α : Type u_1
β : Type ?u.52764
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
rw [← einfsep_pos]
no goals
α : Type u_1
β : Type ?u.52764
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ 0 < einfsep s
exact einfsep_pos_of_finite