Description: The usual topology on ( RR X. RR ) is the product topology of the usual topology on RR . (Contributed by Thierry Arnoux, 21-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tpr2tp.0 | ||
Assertion | tpr2tp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpr2tp.0 | ||
2 | retopon | ||
3 | 1 2 | eqeltri | |
4 | txtopon | ||
5 | 3 3 4 | mp2an |