class PiBase.CorsonCompactSpace (X : Type u) [TopologicalSpace X] extends CompactSpace X : Prop

• isCompact_univ : IsCompact Set.univ
• isHomoeo_subset : ∃ (α : Type u) (f : X → ↑(SigmaProduct fun (x : α) => 0)), Topology.IsEmbedding f