α : Type u_1
β : Type ?u.49562
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
⊢ Set.Subsingleton s
α : Type u_1
β : Type ?u.49562
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ Set.Subsingleton s
rw [einfsep_top] at hs
no goals
α : Type u_1
β : Type ?u.49562
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
⊢ Set.Subsingleton s
exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)