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

• isPreconnected_univ : IsPreconnected Set.univ
• 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