Source: ProCGroups.Topologies
1import ProCGroups.Topologies.Conjugation
2import ProCGroups.Topologies.ContinuousMonoidHom
3import ProCGroups.Topologies.ContinuousMulEquiv
4import ProCGroups.Topologies.FullSubgroupTopology
5import ProCGroups.Topologies.OpenSubgroup
6import ProCGroups.Topologies.QuotientMaps
7import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
9/-!
10# Topological-group infrastructure
12This aggregate module exposes continuous homomorphisms and equivalences, conjugation, open and
13characteristic subgroups, quotient maps, and full subgroup topologies.
14-/