Description: Definition of the circle at infinity CCinftyN . (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-ccinftyN | ⊢ ℂ∞N = ran +∞eiτ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cccinftyN | ⊢ ℂ∞N | |
| 1 | cinftyexpitau | ⊢ +∞eiτ | |
| 2 | 1 | crn | ⊢ ran +∞eiτ |
| 3 | 0 2 | wceq | ⊢ ℂ∞N = ran +∞eiτ |