α : Type u_1
β : Type ?u.81138
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ einfsep s = 0 → Set.Subsingleton s
α : Type u_1
β : Type ?u.81138
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ infsep s = 0 ↔ Set.Subsingleton s
rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]
no goals
α : Type u_1
β : Type ?u.81138
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ einfsep s = 0 → Set.Subsingleton s
exact fun H => (einfsep_pos_of_finite.ne' H).elim