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

Definition df-xrs 15393
Description: The extended real number structure. Unlike df-cnfld 18964, 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 18964. 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 15391 . 2  class  RR*s
2 cnx 15111 . . . . . 6  class  ndx
3 cbs 15114 . . . . . 6  class  Base
42, 3cfv 5599 . . . . 5  class  ( Base `  ndx )
5 cxr 9676 . . . . 5  class  RR*
64, 5cop 4003 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 15183 . . . . . 6  class  +g
82, 7cfv 5599 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11409 . . . . 5  class  +e
108, 9cop 4003 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 15184 . . . . . 6  class  .r
122, 11cfv 5599 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11410 . . . . 5  class  xe
1412, 13cop 4003 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 4001 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 15189 . . . . . 6  class TopSet
172, 16cfv 5599 . . . . 5  class  (TopSet `  ndx )
18 cle 9678 . . . . . 6  class  <_
19 cordt 15390 . . . . . 6  class ordTop
2018, 19cfv 5599 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 4003 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 15190 . . . . . 6  class  le
232, 22cfv 5599 . . . . 5  class  ( le
`  ndx )
2423, 18cop 4003 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 15192 . . . . . 6  class  dist
262, 25cfv 5599 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1437 . . . . . . . 8  class  x
3028cv 1437 . . . . . . . 8  class  y
3129, 30, 18wbr 4421 . . . . . . 7  wff  x  <_ 
y
3229cxne 11408 . . . . . . . 8  class  -e
x
3330, 32, 9co 6303 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11408 . . . . . . . 8  class  -e
y
3529, 34, 9co 6303 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3910 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6305 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 4003 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 4001 . . 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 3435 . 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 1438 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  18975  xrsex  18976  xrsbas  18977  xrsadd  18978  xrsmul  18979  xrstset  18980  xrsle  18981  xrsds  19004
  Copyright terms: Public domain W3C validator