Description: Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | df-bj-cchat | |- CChat = ( CC u. { infty } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccchat | |- CChat |
|
1 | cc | |- CC |
|
2 | cinfty | |- infty |
|
3 | 2 | csn | |- { infty } |
4 | 1 3 | cun | |- ( CC u. { infty } ) |
5 | 0 4 | wceq | |- CChat = ( CC u. { infty } ) |