Compact groups with a descending chain condition are Lie groups (source code)

= Compact groups with a descending chain condition are Lie groups

The <Peter-Weyl theorem> makes finite-dimensional <unitary representations> separate elements of a <compact group>. Intersecting their closed kernels gives the identity <subgroup>. If the <descending chain condition> holds for closed <subgroups>, choose finitely many representations whose kernel intersection is already trivial: otherwise repeatedly exclude a surviving nonidentity element to obtain an infinite strict chain. Their direct sum is a <faithful representation> into a finite-dimensional <unitary group>. Compactness makes its image closed, and the <closed-subgroup theorem> gives the original <group> a compatible <Lie group> structure.