Description: A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | qustgp.h | |
|
qustgpopn.x | |
||
qustgpopn.j | |
||
qustgpopn.k | |
||
qustgpopn.f | |
||
Assertion | qustgpopn | |