α : Type u_1
β : Type ?u.50351
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s ≠ ⊤
α : Type u_1
β : Type ?u.50351
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s < ⊤
rw [lt_top_iff_ne_top]
no goals
α : Type u_1
β : Type ?u.50351
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s ≠ ⊤
exact hs.einfsep_ne_top