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

Definition df-xrs 13403
Description: The extended real number structure. Unlike df-cnfld 16378, 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 16378. 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 13399 . 2  class  RR* s
2 cnx 13145 . . . . . 6  class  ndx
3 cbs 13148 . . . . . 6  class  Base
42, 3cfv 5255 . . . . 5  class  ( Base `  ndx )
5 cxr 8866 . . . . 5  class  RR*
64, 5cop 3643 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13208 . . . . . 6  class  +g
82, 7cfv 5255 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10450 . . . . 5  class  + e
108, 9cop 3643 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13209 . . . . . 6  class  .r
122, 11cfv 5255 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10451 . . . . 5  class  x e
1412, 13cop 3643 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3642 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13214 . . . . . 6  class TopSet
172, 16cfv 5255 . . . . 5  class  (TopSet `  ndx )
18 cle 8868 . . . . . 6  class  <_
19 cordt 13398 . . . . . 6  class ordTop
2018, 19cfv 5255 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3643 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13215 . . . . . 6  class  le
232, 22cfv 5255 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3643 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13217 . . . . . 6  class  dist
262, 25cfv 5255 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1622 . . . . . . . 8  class  x
3028cv 1622 . . . . . . . 8  class  y
3129, 30, 18wbr 4023 . . . . . . 7  wff  x  <_ 
y
3229cxne 10449 . . . . . . . 8  class  - e
x
3330, 32, 9co 5858 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10449 . . . . . . . 8  class  - e
y
3529, 34, 9co 5858 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3565 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 5860 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3643 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3642 . . 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 3150 . 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 1623 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  16381  xrsex  16382  xrsbas  16390  xrsadd  16391  xrsmul  16392  xrstset  16393  xrsle  16394  xrsds  16414
  Copyright terms: Public domain W3C validator