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

Definition df-xrs 13646
Description: The extended real number structure. Unlike df-cnfld 16620, 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 16620. 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 13642 . 2  class  RR* s
2 cnx 13386 . . . . . 6  class  ndx
3 cbs 13389 . . . . . 6  class  Base
42, 3cfv 5387 . . . . 5  class  ( Base `  ndx )
5 cxr 9045 . . . . 5  class  RR*
64, 5cop 3753 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13449 . . . . . 6  class  +g
82, 7cfv 5387 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10633 . . . . 5  class  + e
108, 9cop 3753 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13450 . . . . . 6  class  .r
122, 11cfv 5387 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10634 . . . . 5  class  x e
1412, 13cop 3753 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3752 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13455 . . . . . 6  class TopSet
172, 16cfv 5387 . . . . 5  class  (TopSet `  ndx )
18 cle 9047 . . . . . 6  class  <_
19 cordt 13641 . . . . . 6  class ordTop
2018, 19cfv 5387 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3753 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13456 . . . . . 6  class  le
232, 22cfv 5387 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3753 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13458 . . . . . 6  class  dist
262, 25cfv 5387 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1648 . . . . . . . 8  class  x
3028cv 1648 . . . . . . . 8  class  y
3129, 30, 18wbr 4146 . . . . . . 7  wff  x  <_ 
y
3229cxne 10632 . . . . . . . 8  class  - e
x
3330, 32, 9co 6013 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10632 . . . . . . . 8  class  - e
y
3529, 34, 9co 6013 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3675 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 6015 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3753 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3752 . . 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 3254 . 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 1649 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  16631  xrsex  16632  xrsbas  16633  xrsadd  16634  xrsmul  16635  xrstset  16636  xrsle  16637  xrsds  16657
  Copyright terms: Public domain W3C validator