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

Definition df-xrs 14880
Description: The extended real number structure. Unlike df-cnfld 18399, 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 18399. 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 14878 . 2  class  RR*s
2 cnx 14610 . . . . . 6  class  ndx
3 cbs 14613 . . . . . 6  class  Base
42, 3cfv 5578 . . . . 5  class  ( Base `  ndx )
5 cxr 9630 . . . . 5  class  RR*
64, 5cop 4020 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14678 . . . . . 6  class  +g
82, 7cfv 5578 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11326 . . . . 5  class  +e
108, 9cop 4020 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14679 . . . . . 6  class  .r
122, 11cfv 5578 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11327 . . . . 5  class  xe
1412, 13cop 4020 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 4018 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14684 . . . . . 6  class TopSet
172, 16cfv 5578 . . . . 5  class  (TopSet `  ndx )
18 cle 9632 . . . . . 6  class  <_
19 cordt 14877 . . . . . 6  class ordTop
2018, 19cfv 5578 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 4020 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14685 . . . . . 6  class  le
232, 22cfv 5578 . . . . 5  class  ( le
`  ndx )
2423, 18cop 4020 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14687 . . . . . 6  class  dist
262, 25cfv 5578 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1382 . . . . . . . 8  class  x
3028cv 1382 . . . . . . . 8  class  y
3129, 30, 18wbr 4437 . . . . . . 7  wff  x  <_ 
y
3229cxne 11325 . . . . . . . 8  class  -e
x
3330, 32, 9co 6281 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11325 . . . . . . . 8  class  -e
y
3529, 34, 9co 6281 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3926 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6283 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 4020 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 4018 . . 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 3459 . 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 1383 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  18410  xrsex  18411  xrsbas  18412  xrsadd  18413  xrsmul  18414  xrstset  18415  xrsle  18416  xrsds  18439
  Copyright terms: Public domain W3C validator