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

Definition df-xrs 14756
Description: The extended real number structure. Unlike df-cnfld 18208, 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 18208. 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 14754 . 2  class  RR*s
2 cnx 14486 . . . . . 6  class  ndx
3 cbs 14489 . . . . . 6  class  Base
42, 3cfv 5587 . . . . 5  class  ( Base `  ndx )
5 cxr 9626 . . . . 5  class  RR*
64, 5cop 4033 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14554 . . . . . 6  class  +g
82, 7cfv 5587 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11315 . . . . 5  class  +e
108, 9cop 4033 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14555 . . . . . 6  class  .r
122, 11cfv 5587 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11316 . . . . 5  class  xe
1412, 13cop 4033 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 4031 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14560 . . . . . 6  class TopSet
172, 16cfv 5587 . . . . 5  class  (TopSet `  ndx )
18 cle 9628 . . . . . 6  class  <_
19 cordt 14753 . . . . . 6  class ordTop
2018, 19cfv 5587 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 4033 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14561 . . . . . 6  class  le
232, 22cfv 5587 . . . . 5  class  ( le
`  ndx )
2423, 18cop 4033 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14563 . . . . . 6  class  dist
262, 25cfv 5587 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1378 . . . . . . . 8  class  x
3028cv 1378 . . . . . . . 8  class  y
3129, 30, 18wbr 4447 . . . . . . 7  wff  x  <_ 
y
3229cxne 11314 . . . . . . . 8  class  -e
x
3330, 32, 9co 6283 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11314 . . . . . . . 8  class  -e
y
3529, 34, 9co 6283 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3939 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6285 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 4033 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 4031 . . 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 3474 . 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 1379 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  18219  xrsex  18220  xrsbas  18221  xrsadd  18222  xrsmul  18223  xrstset  18224  xrsle  18225  xrsds  18245
  Copyright terms: Public domain W3C validator