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

Definition df-xrs 14423
Description: The extended real number structure. Unlike df-cnfld 17663, 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 17663. 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 14421 . 2  class  RR*s
2 cnx 14154 . . . . . 6  class  ndx
3 cbs 14157 . . . . . 6  class  Base
42, 3cfv 5406 . . . . 5  class  ( Base `  ndx )
5 cxr 9405 . . . . 5  class  RR*
64, 5cop 3871 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14221 . . . . . 6  class  +g
82, 7cfv 5406 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11075 . . . . 5  class  +e
108, 9cop 3871 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14222 . . . . . 6  class  .r
122, 11cfv 5406 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11076 . . . . 5  class  xe
1412, 13cop 3871 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3869 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14227 . . . . . 6  class TopSet
172, 16cfv 5406 . . . . 5  class  (TopSet `  ndx )
18 cle 9407 . . . . . 6  class  <_
19 cordt 14420 . . . . . 6  class ordTop
2018, 19cfv 5406 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3871 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14228 . . . . . 6  class  le
232, 22cfv 5406 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3871 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14230 . . . . . 6  class  dist
262, 25cfv 5406 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1361 . . . . . . . 8  class  x
3028cv 1361 . . . . . . . 8  class  y
3129, 30, 18wbr 4280 . . . . . . 7  wff  x  <_ 
y
3229cxne 11074 . . . . . . . 8  class  -e
x
3330, 32, 9co 6080 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11074 . . . . . . . 8  class  -e
y
3529, 34, 9co 6080 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3779 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6082 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3871 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3869 . . 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 3314 . 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 1362 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  17674  xrsex  17675  xrsbas  17676  xrsadd  17677  xrsmul  17678  xrstset  17679  xrsle  17680  xrsds  17700
  Copyright terms: Public domain W3C validator