Definition df-bj-cchat

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	⊢ ℂ̂ = ( ℂ ∪ { ∞ } )