Description: The identity component, the connected component containing the identity element, is a closed ( conncompcld ) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tgpconncomp.x | |
|
tgpconncomp.z | |
||
tgpconncomp.j | |
||
tgpconncomp.s | |
||
Assertion | tgpconncomp | |