Description: The connected component containing A is the left coset of the identity component containing A . (Contributed by Mario Carneiro, 17-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tgpconncomp.x | |
|
tgpconncomp.z | |
||
tgpconncomp.j | |
||
tgpconncomp.s | |
||
tgpconncompeqg.r | |
||
Assertion | tgpconncompeqg | |