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 34511

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 34510	. 2 class ℂ_∞N
2		cinftyexpitau 34508	. . 3 class +∞e^iτ
3	2	crn 5549	. 2 class ran +∞e^iτ
4	1, 3	wceq 1536	1 wff ℂ_∞N = ran +∞e^iτ

Colors of variables: wff setvar class

This definition is referenced by: bj-inftyexpitaufo 34512

W3C validator