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 | |- CCinftyN = ran inftyexpitau |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cccinftyN | |- CCinftyN |
|
| 1 | cinftyexpitau | |- inftyexpitau |
|
| 2 | 1 | crn | |- ran inftyexpitau |
| 3 | 0 2 | wceq | |- CCinftyN = ran inftyexpitau |