class PiBase.StoneanSpace (X : Type u_1) [TopologicalSpace X] extends CompactSpace X, ExtremallyDisconnected X, T2Space X : Prop

• isCompact_univ : IsCompact Set.univ
• open_closure (U : Set X) : IsOpen U → IsOpen (closure U)
• t2 : Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v