Metamath Proof Explorer
Description: Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019)
|
|
Ref |
Expression |
|
Assertion |
df-bj-cchat |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
ccchat |
|
1 |
|
cc |
|
2 |
|
cinfty |
|
3 |
2
|
csn |
|
4 |
1 3
|
cun |
|
5 |
0 4
|
wceq |
|