α : Type u_1
β : Type ?u.81734
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ Set.Nontrivial s → 0 < einfsep s
α : Type u_1
β : Type ?u.81734
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < infsep s ↔ Set.Nontrivial s
rw [infsep_pos, einfsep_lt_top_iff, and_iff_right_iff_imp]
no goals
α : Type u_1
β : Type ?u.81734
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ Set.Nontrivial s → 0 < einfsep s
exact fun _ => einfsep_pos_of_finite