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

• embeds_in_topological_w_group : ∃ (Y : Type u) (x : TopologicalSpace Y) (f : X → Y), WSpace Y ∧ HasGroupTopology Y ∧ Topology.IsEmbedding f