Further separation lemmas

theorem CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum {X : Type u_1} [TopologicalSpace X] [T35Space X] (h : Cardinal.mk X < Cardinal.continuum) : TotallySeparatedSpace X

instance CompletelyRegularSpace.instTotallySeparatedSpaceOfCountable {X : Type u_1} [TopologicalSpace X] [T35Space X] [Countable X] : TotallySeparatedSpace X

theorem Set.Countable.totallySeparatedSpace {X : Type u_1} [TopologicalSpace X] [T35Space X] {s : Set X} (h : s.Countable) : TotallySeparatedSpace ↑s

theorem Set.Countable.isTotallyDisconnected {X : Type u_1} [MetricSpace X] {s : Set X} (hs : s.Countable) : IsTotallyDisconnected s

Countable subsets of metric spaces are totally disconnected.