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

Definition df-xrs 15478
Description: The extended real number structure. Unlike df-cnfld 19048, 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 19048. 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 ) ,  xe >. }  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 15476 . 2  class  RR*s
2 cnx 15196 . . . . . 6  class  ndx
3 cbs 15199 . . . . . 6  class  Base
42, 3cfv 5589 . . . . 5  class  ( Base `  ndx )
5 cxr 9692 . . . . 5  class  RR*
64, 5cop 3965 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 15268 . . . . . 6  class  +g
82, 7cfv 5589 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11430 . . . . 5  class  +e
108, 9cop 3965 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 15269 . . . . . 6  class  .r
122, 11cfv 5589 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11431 . . . . 5  class  xe
1412, 13cop 3965 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3963 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 15274 . . . . . 6  class TopSet
172, 16cfv 5589 . . . . 5  class  (TopSet `  ndx )
18 cle 9694 . . . . . 6  class  <_
19 cordt 15475 . . . . . 6  class ordTop
2018, 19cfv 5589 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3965 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 15275 . . . . . 6  class  le
232, 22cfv 5589 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3965 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 15277 . . . . . 6  class  dist
262, 25cfv 5589 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1451 . . . . . . . 8  class  x
3028cv 1451 . . . . . . . 8  class  y
3129, 30, 18wbr 4395 . . . . . . 7  wff  x  <_ 
y
3229cxne 11429 . . . . . . . 8  class  -e
x
3330, 32, 9co 6308 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11429 . . . . . . . 8  class  -e
y
3529, 34, 9co 6308 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3872 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6310 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3965 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3963 . . 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 3388 . 2  class  ( {
<. ( Base `  ndx ) ,  RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }  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 1452 1  wff  RR*s 
=  ( { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }  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 setvar class
This definition is referenced by:  xrsstr  19059  xrsex  19060  xrsbas  19061  xrsadd  19062  xrsmul  19063  xrstset  19064  xrsle  19065  xrsds  19088
  Copyright terms: Public domain W3C validator