class PiBase.HasGroupTopology (X : Type u_1) [TopologicalSpace X] : Prop

• has_group_topology : ∃ (x : Group X), IsTopologicalGroup X