α : Type u_1
β : Type ?u.55856
inst✝ : EDist α
x y : α
s : Set α
hs : ¬Set.Nontrivial s
⊢ ¬0 < infsep s
α : Type u_1
β : Type ?u.55856
inst✝ : EDist α
x y : α
s : Set α
hs : 0 < infsep s
⊢ Set.Nontrivial s
contrapose hs
α : Type u_1
β : Type ?u.55856
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ ¬0 < infsep s
α : Type u_1
β : Type ?u.55856
inst✝ : EDist α
x y : α
s : Set α
hs : ¬Set.Nontrivial s
⊢ ¬0 < infsep s
rw [not_nontrivial_iff] at hs
no goals
α : Type u_1
β : Type ?u.55856
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ ¬0 < infsep s
exact hs.infsep_zero ▸ lt_irrefl _