class PiBase.StoneSpace (X : Type u) [TopologicalSpace X] extends CompactSpace X, T2Space X, TotallyDisconnectedSpace X : Prop

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