Definition df-bj-inftyexpi

Description: Definition of the auxiliary function inftyexpi parameterizing the circle at infinity CCinfty in CCbar . We use coupling with CC to simplify the proof of bj-ccinftydisj . It could seem more natural to define inftyexpi on all of RR , but we want to use only basic functions in the definition of CCbar . TODO: transition to df-bj-inftyexpitau instead. (Contributed by BJ, 22-Jun-2019) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-inftyexpi	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinftyexpi	⊢ +∞ei
1		vx	⊢ 𝑥
2		cpi	⊢ π
3	2	cneg	⊢ - π
4		cioc	⊢ (,]
5	3 2 4	co	⊢ ( - π (,] π )
6	1	cv	⊢ 𝑥
7		cc	⊢ ℂ
8	6 7	cop	⊢ ⟨ 𝑥 , ℂ ⟩
9	1 5 8	cmpt	⊢ ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
10	0 9	wceq	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )