Source: ProCGroups.ProC.Quotients
1import ProCGroups.ProC.Quotients.ClosedNormal
2import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
3import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
4import ProCGroups.ProC.Quotients.LeftQuotientMaps
5import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
6import ProCGroups.ProC.Quotients.OpenSubgroupSections
8/-!
9# Quotients and sections of pro-\(C\) groups
11This aggregate exports quotient topology results, left-quotient projections, continuous sections
12for open and closed subgroups, neighborhood approximation, and inverse systems formed from
13descending closed subgroups.
14-/