α : Type u_1
β : Type ?u.50084
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ ¬Set.Nontrivial s
α : Type u_1
β : Type ?u.50084
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s ≠ ⊤
contrapose! hs
α : Type u_1
β : Type ?u.50084
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ Set.Subsingleton s
α : Type u_1
β : Type ?u.50084
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ ¬Set.Nontrivial s
rw [not_nontrivial_iff]
no goals
α : Type u_1
β : Type ?u.50084
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ Set.Subsingleton s
exact subsingleton_of_einfsep_eq_top hs