Description: Definition of the auxiliary function inftyexpi parameterizing the circle at infinity CCinfty in CCbar . We use coupling with CC to simplify the proof of bj-ccinftydisj . It could seem more natural to define inftyexpi on all of RR , but we want to use only basic functions in the definition of CCbar . TODO: transition to df-bj-inftyexpitau instead. (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-inftyexpi | |- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cinftyexpi | |- inftyexpi |
|
| 1 | vx | |- x |
|
| 2 | cpi | |- _pi |
|
| 3 | 2 | cneg | |- -u _pi |
| 4 | cioc | |- (,] |
|
| 5 | 3 2 4 | co | |- ( -u _pi (,] _pi ) |
| 6 | 1 | cv | |- x |
| 7 | cc | |- CC |
|
| 8 | 6 7 | cop | |- <. x , CC >. |
| 9 | 1 5 8 | cmpt | |- ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. ) |
| 10 | 0 9 | wceq | |- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. ) |