theorem PiBase.r0Space_iff_inseparableComponent_closed {X : Type u} [TopologicalSpace X] : R0Space X ↔ ∀ (x : X), IsClosed (InseparableComponent x)

A space is R₀, iff all "inseparable" components are closed.

theorem PiBase.instSubsingletonOfPreconnectedSpaceOfR0SpaceOfHasAnIsolatedPoint (X : Type u) [TopologicalSpace X] [h : R0Space X] [h' : HasAnIsolatedPoint X] [h'' : PreconnectedSpace X] : Subsingleton X