ProCGroups.NormalSubgroups.SimpleQuotients

If \(G/K\) is simple, every normal subgroup of \(G\) containing \(K\) is either \(K\) or all of \(G\). This is the correspondence theorem form of the simple-quotient dichotomy.

Compactness step: if the closed normal subgroups satisfying \(M \sqcup K = \top\) are already stable under finite intersections, then they are stable under arbitrary intersections.

An arbitrary infimum of normal subgroups is normal, when normality is known for every subgroup in the indexing set.