class HasGδSingletons (X : Type u_1) [TopologicalSpace X] : Prop

A space where all singletons are Gδ sets.

• isGδ_singleton ⦃x : X⦄ : IsGδ {x}

instance HasGδSingletons.of_t1Space_firstCountableTopology (X : Type u_1) [TopologicalSpace X] [FirstCountableTopology X] [T1Space X] : HasGδSingletons X

Singletons are Gδ in first-countable T₁ spaces.