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	$$⊢\widehat{ℂ}=ℂ\cup \left\{\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccchat	$$class\widehat{ℂ}$$
1		cc	$$classℂ$$
2		cinfty	$$class\infty$$
3	2	csn	$$class\left\{\infty \right\}$$
4	1 3	cun	$$class\left(ℂ\cup \left\{\infty \right\}\right)$$
5	0 4	wceq	$$wff\widehat{ℂ}=ℂ\cup \left\{\infty \right\}$$