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

Definition df-xrs 15116
Description: The extended real number structure. Unlike df-cnfld 18741, 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 18741. 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 15114 . 2  class  RR*s
2 cnx 14838 . . . . . 6  class  ndx
3 cbs 14841 . . . . . 6  class  Base
42, 3cfv 5569 . . . . 5  class  ( Base `  ndx )
5 cxr 9657 . . . . 5  class  RR*
64, 5cop 3978 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14909 . . . . . 6  class  +g
82, 7cfv 5569 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11369 . . . . 5  class  +e
108, 9cop 3978 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14910 . . . . . 6  class  .r
122, 11cfv 5569 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11370 . . . . 5  class  xe
1412, 13cop 3978 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3976 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14915 . . . . . 6  class TopSet
172, 16cfv 5569 . . . . 5  class  (TopSet `  ndx )
18 cle 9659 . . . . . 6  class  <_
19 cordt 15113 . . . . . 6  class ordTop
2018, 19cfv 5569 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3978 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14916 . . . . . 6  class  le
232, 22cfv 5569 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3978 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14918 . . . . . 6  class  dist
262, 25cfv 5569 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1404 . . . . . . . 8  class  x
3028cv 1404 . . . . . . . 8  class  y
3129, 30, 18wbr 4395 . . . . . . 7  wff  x  <_ 
y
3229cxne 11368 . . . . . . . 8  class  -e
x
3330, 32, 9co 6278 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11368 . . . . . . . 8  class  -e
y
3529, 34, 9co 6278 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3885 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6280 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3978 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3976 . . 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 3412 . 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 1405 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  18752  xrsex  18753  xrsbas  18754  xrsadd  18755  xrsmul  18756  xrstset  18757  xrsle  18758  xrsds  18781
  Copyright terms: Public domain W3C validator