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

Definition df-xrs 15400
Description: The extended real number structure. Unlike df-cnfld 18971, 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 18971. 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 15398 . 2  class  RR*s
2 cnx 15118 . . . . . 6  class  ndx
3 cbs 15121 . . . . . 6  class  Base
42, 3cfv 5582 . . . . 5  class  ( Base `  ndx )
5 cxr 9674 . . . . 5  class  RR*
64, 5cop 3974 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 15190 . . . . . 6  class  +g
82, 7cfv 5582 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11407 . . . . 5  class  +e
108, 9cop 3974 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 15191 . . . . . 6  class  .r
122, 11cfv 5582 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11408 . . . . 5  class  xe
1412, 13cop 3974 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3972 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 15196 . . . . . 6  class TopSet
172, 16cfv 5582 . . . . 5  class  (TopSet `  ndx )
18 cle 9676 . . . . . 6  class  <_
19 cordt 15397 . . . . . 6  class ordTop
2018, 19cfv 5582 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3974 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 15197 . . . . . 6  class  le
232, 22cfv 5582 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3974 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 15199 . . . . . 6  class  dist
262, 25cfv 5582 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1443 . . . . . . . 8  class  x
3028cv 1443 . . . . . . . 8  class  y
3129, 30, 18wbr 4402 . . . . . . 7  wff  x  <_ 
y
3229cxne 11406 . . . . . . . 8  class  -e
x
3330, 32, 9co 6290 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11406 . . . . . . . 8  class  -e
y
3529, 34, 9co 6290 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3881 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6292 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3974 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3972 . . 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 3402 . 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 1444 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  18982  xrsex  18983  xrsbas  18984  xrsadd  18985  xrsmul  18986  xrstset  18987  xrsle  18988  xrsds  19011
  Copyright terms: Public domain W3C validator