class PiBase.GδSpace (X : Type u) [TopologicalSpace X] : Prop

• closed_gdelta ⦃s : Set X⦄ : IsClosed s → IsGδ s