Description: The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | ioorp | |- ( 0 (,) +oo ) = RR+ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioopos | |- ( 0 (,) +oo ) = { x e. RR | 0 < x } |
|
2 | df-rp | |- RR+ = { x e. RR | 0 < x } |
|
3 | 1 2 | eqtr4i | |- ( 0 (,) +oo ) = RR+ |