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

Definition df-xrs 13726
Description: The extended real number structure. Unlike df-cnfld 16704, 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 16704. 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 ) ,  x e >. }  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 13722 . 2  class  RR* s
2 cnx 13466 . . . . . 6  class  ndx
3 cbs 13469 . . . . . 6  class  Base
42, 3cfv 5454 . . . . 5  class  ( Base `  ndx )
5 cxr 9119 . . . . 5  class  RR*
64, 5cop 3817 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13529 . . . . . 6  class  +g
82, 7cfv 5454 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10708 . . . . 5  class  + e
108, 9cop 3817 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13530 . . . . . 6  class  .r
122, 11cfv 5454 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10709 . . . . 5  class  x e
1412, 13cop 3817 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3816 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13535 . . . . . 6  class TopSet
172, 16cfv 5454 . . . . 5  class  (TopSet `  ndx )
18 cle 9121 . . . . . 6  class  <_
19 cordt 13721 . . . . . 6  class ordTop
2018, 19cfv 5454 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3817 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13536 . . . . . 6  class  le
232, 22cfv 5454 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3817 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13538 . . . . . 6  class  dist
262, 25cfv 5454 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1651 . . . . . . . 8  class  x
3028cv 1651 . . . . . . . 8  class  y
3129, 30, 18wbr 4212 . . . . . . 7  wff  x  <_ 
y
3229cxne 10707 . . . . . . . 8  class  - e
x
3330, 32, 9co 6081 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10707 . . . . . . . 8  class  - e
y
3529, 34, 9co 6081 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3739 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 6083 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3817 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3816 . . 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 3318 . 2  class  ( {
<. ( Base `  ndx ) ,  RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  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 1652 1  wff  RR* s  =  ( { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  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 set class
This definition is referenced by:  xrsstr  16715  xrsex  16716  xrsbas  16717  xrsadd  16718  xrsmul  16719  xrstset  16720  xrsle  16721  xrsds  16741
  Copyright terms: Public domain W3C validator