Description: A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | qustps.u | |
|
qustps.v | |
||
qustps.e | |
||
qustps.r | |
||
Assertion | qustps | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qustps.u | |
|
2 | qustps.v | |
|
3 | qustps.e | |
|
4 | qustps.r | |
|
5 | eqid | |
|
6 | 1 2 5 3 4 | qusval | |
7 | 1 2 5 3 4 | quslem | |
8 | 6 2 7 4 | imastps | |