Source: ProCGroups.Topologies.FullSubgroupTopology
1import ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
2import ProCGroups.Topologies.FullSubgroupTopology.QuotientVariety
4/-!
5# Full subgroup topologies
7This aggregate exports abstract quotient formations and varieties, the associated notions of
8open and closed subgroup, pro-\(C\) closure and residuality, and pullback stability.
9-/