MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xrs Unicode version

Definition df-xrs 13419
Description: The extended real number structure. Unlike df-cnfld 16394, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 16394. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because  +oo is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make  +oo an isolated point since there is nothing else in the  1 -ball around it). All components of this structure agree with ℂfld when restricted to  RR. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xrs  |-  RR* s  =  ( { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  u.  {
<. (TopSet `  ndx ) ,  (ordTop `  <_  ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >. } )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-xrs
StepHypRef Expression
1 cxrs 13415 . 2  class  RR* s
2 cnx 13161 . . . . . 6  class  ndx
3 cbs 13164 . . . . . 6  class  Base
42, 3cfv 5271 . . . . 5  class  ( Base `  ndx )
5 cxr 8882 . . . . 5  class  RR*
64, 5cop 3656 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13224 . . . . . 6  class  +g
82, 7cfv 5271 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10466 . . . . 5  class  + e
108, 9cop 3656 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13225 . . . . . 6  class  .r
122, 11cfv 5271 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10467 . . . . 5  class  x e
1412, 13cop 3656 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3655 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13230 . . . . . 6  class TopSet
172, 16cfv 5271 . . . . 5  class  (TopSet `  ndx )
18 cle 8884 . . . . . 6  class  <_
19 cordt 13414 . . . . . 6  class ordTop
2018, 19cfv 5271 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3656 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13231 . . . . . 6  class  le
232, 22cfv 5271 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3656 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13233 . . . . . 6  class  dist
262, 25cfv 5271 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1631 . . . . . . . 8  class  x
3028cv 1631 . . . . . . . 8  class  y
3129, 30, 18wbr 4039 . . . . . . 7  wff  x  <_ 
y
3229cxne 10465 . . . . . . . 8  class  - e
x
3330, 32, 9co 5874 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10465 . . . . . . . 8  class  - e
y
3529, 34, 9co 5874 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3578 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 5876 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3656 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3655 . . 3  class  { <. (TopSet `  ndx ) ,  (ordTop `  <_  ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >. }
4015, 39cun 3163 . 2  class  ( {
<. ( Base `  ndx ) ,  RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  u.  {
<. (TopSet `  ndx ) ,  (ordTop `  <_  ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >. } )
411, 40wceq 1632 1  wff  RR* s  =  ( { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  u.  {
<. (TopSet `  ndx ) ,  (ordTop `  <_  ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >. } )
Colors of variables: wff set class
This definition is referenced by:  xrsstr  16397  xrsex  16398  xrsbas  16406  xrsadd  16407  xrsmul  16408  xrstset  16409  xrsle  16410  xrsds  16430
  Copyright terms: Public domain W3C validator