Interaction of separation properties with connectedness properties

@[instance 100]

instance TotallyDisconnectedSpace.t1Space {X : Type u_1} [TopologicalSpace X] [h : TotallyDisconnectedSpace X] : T1Space X

theorem PreconnectedSpace.trivial_of_discrete {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [DiscreteTopology X] : Subsingleton X

theorem IsPreconnected.infinite_of_nontrivial {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (h : IsPreconnected s) (hs : s.Nontrivial) : s.Infinite

theorem PreconnectedSpace.infinite {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [Nontrivial X] [T1Space X] : Infinite X

@[deprecated PreconnectedSpace.infinite (since := "2025-03-21")]

theorem ConnectedSpace.infinite {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [Nontrivial X] [T1Space X] : Infinite X

Alias of PreconnectedSpace.infinite.

@[instance 100]

instance ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] (x : X) : (nhdsWithin x {x}ᶜ).NeBot

A non-trivial connected T1 space has no isolated points.