Description: Definition of the circle at infinity CCinfty . (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-ccinfty | ⊢ ℂ∞ = ran +∞ei |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cccinfty | ⊢ ℂ∞ | |
1 | cinftyexpi | ⊢ +∞ei | |
2 | 1 | crn | ⊢ ran +∞ei |
3 | 0 2 | wceq | ⊢ ℂ∞ = ran +∞ei |