Open normal subgroup basis of a profinite group (source code)

= Open normal subgroup basis of a profinite group

Every identity neighbourhood of a compact Hausdorff totally disconnected <topological group> contains an open <normal subgroup>. Choose a <clopen set> $U$ containing the identity inside that neighbourhood. Compactness and continuity give a symmetric identity neighbourhood $V$ with $VU\subseteq U$, hence $VU=U$. The setwise stabilizer $H=\{g:gU=U\}$ is an open <subgroup> contained in $U$. Its index is finite, so its <normal core> is an open <normal subgroup> contained in $U$. These subgroups recover the <profinite group> as the <inverse limit> of its finite quotients.