class PiBase.GoSpace (X : Type u) [TopologicalSpace X] : Prop

• subset_lots : ∃ (Z : Type u) (f : X → Z) (x : TopologicalSpace Z), Lots Z ∧ Topology.IsEmbedding f