class PiBase.SemiregularSpace (X : Type u_1) [TopologicalSpace X] : Prop

• semiregular : ∃ (B : Set (Set X)), TopologicalSpace.IsTopologicalBasis B ∧ ∀ s ∈ B, IsRegularOpen s