class PiBase.CechCompleteSpace (X : Type u) [TopologicalSpace X] extends T35Space X : Prop

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• completely_regular (x : X) (K : Set X) : IsClosed K → x ∉ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K
• is_gδ : IsGδ (Set.range stoneCechUnit)