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

Definition df-xrs 14562
Description: The extended real number structure. Unlike df-cnfld 17947, 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 17947. 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 14560 . 2  class  RR*s
2 cnx 14292 . . . . . 6  class  ndx
3 cbs 14295 . . . . . 6  class  Base
42, 3cfv 5529 . . . . 5  class  ( Base `  ndx )
5 cxr 9531 . . . . 5  class  RR*
64, 5cop 3994 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14360 . . . . . 6  class  +g
82, 7cfv 5529 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11201 . . . . 5  class  +e
108, 9cop 3994 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14361 . . . . . 6  class  .r
122, 11cfv 5529 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11202 . . . . 5  class  xe
1412, 13cop 3994 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3992 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14366 . . . . . 6  class TopSet
172, 16cfv 5529 . . . . 5  class  (TopSet `  ndx )
18 cle 9533 . . . . . 6  class  <_
19 cordt 14559 . . . . . 6  class ordTop
2018, 19cfv 5529 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3994 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14367 . . . . . 6  class  le
232, 22cfv 5529 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3994 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14369 . . . . . 6  class  dist
262, 25cfv 5529 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1369 . . . . . . . 8  class  x
3028cv 1369 . . . . . . . 8  class  y
3129, 30, 18wbr 4403 . . . . . . 7  wff  x  <_ 
y
3229cxne 11200 . . . . . . . 8  class  -e
x
3330, 32, 9co 6203 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11200 . . . . . . . 8  class  -e
y
3529, 34, 9co 6203 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3902 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6205 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3994 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3992 . . 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 3437 . 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 1370 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  17958  xrsex  17959  xrsbas  17960  xrsadd  17961  xrsmul  17962  xrstset  17963  xrsle  17964  xrsds  17984
  Copyright terms: Public domain W3C validator