class PiBase.PSpace (X : Type u) [TopologicalSpace X] : Prop

• isGδ_open ⦃s : Set X⦄ : IsGδ s → IsOpen s