![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-xr | GIF version |
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 |
---|---|
df-xr | ⊢ ℝ* = (ℝ ∪ {+∞, -∞}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cxr 8053 | . 2 class ℝ* | |
2 | cr 7871 | . . 3 class ℝ | |
3 | cpnf 8051 | . . . 4 class +∞ | |
4 | cmnf 8052 | . . . 4 class -∞ | |
5 | 3, 4 | cpr 3619 | . . 3 class {+∞, -∞} |
6 | 2, 5 | cun 3151 | . 2 class (ℝ ∪ {+∞, -∞}) |
7 | 1, 6 | wceq 1364 | 1 wff ℝ* = (ℝ ∪ {+∞, -∞}) |
Colors of variables: wff set class |
This definition is referenced by: ressxr 8063 pnfxr 8072 mnfxr 8076 ltrelxr 8080 elxr 9842 xrex 9922 |
Copyright terms: Public domain | W3C validator |