df-bj-ccinftyN - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-ccinftyN		Structured version Visualization version GIF version

Definition df-bj-ccinftyN 35299

Description: Definition of the circle at infinity ℂ_∞N. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

**Assertion**
Ref	Expression
df-bj-ccinftyN	⊢ ℂ_∞N = ran +∞e^iτ

**Detailed syntax breakdown of Definition df-bj-ccinftyN**
Step	Hyp	Ref	Expression
1		cccinftyN 35298	. 2 class ℂ_∞N
2		cinftyexpitau 35296	. . 3 class +∞e^iτ
3	2	crn 5581	. 2 class ran +∞e^iτ
4	1, 3	wceq 1539	1 wff ℂ_∞N = ran +∞e^iτ

Colors of variables: wff setvar class

This definition is referenced by: bj-inftyexpitaufo 35300

W3C validator