Description: Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of Gleason p. 173. (Contributed by NM, 13-Oct-2005)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-xr | |- RR* = ( RR u. { +oo , -oo } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cxr | |- RR* |
|
| 1 | cr | |- RR |
|
| 2 | cpnf | |- +oo |
|
| 3 | cmnf | |- -oo |
|
| 4 | 2 3 | cpr | |- { +oo , -oo } |
| 5 | 1 4 | cun | |- ( RR u. { +oo , -oo } ) |
| 6 | 0 5 | wceq | |- RR* = ( RR u. { +oo , -oo } ) |