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

Definition df-xrs 13398
Description: The extended real number structure. Unlike df-cnfld 16373, 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 16373. 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 13394 . 2  class  RR* s
2 cnx 13140 . . . . . 6  class  ndx
3 cbs 13143 . . . . . 6  class  Base
42, 3cfv 5222 . . . . 5  class  ( Base `  ndx )
5 cxr 8862 . . . . 5  class  RR*
64, 5cop 3645 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13203 . . . . . 6  class  +g
82, 7cfv 5222 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10446 . . . . 5  class  + e
108, 9cop 3645 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13204 . . . . . 6  class  .r
122, 11cfv 5222 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10447 . . . . 5  class  x e
1412, 13cop 3645 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3644 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13209 . . . . . 6  class TopSet
172, 16cfv 5222 . . . . 5  class  (TopSet `  ndx )
18 cle 8864 . . . . . 6  class  <_
19 cordt 13393 . . . . . 6  class ordTop
2018, 19cfv 5222 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3645 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13210 . . . . . 6  class  le
232, 22cfv 5222 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3645 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13212 . . . . . 6  class  dist
262, 25cfv 5222 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1623 . . . . . . . 8  class  x
3028cv 1623 . . . . . . . 8  class  y
3129, 30, 18wbr 4025 . . . . . . 7  wff  x  <_ 
y
3229cxne 10445 . . . . . . . 8  class  - e
x
3330, 32, 9co 5820 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10445 . . . . . . . 8  class  - e
y
3529, 34, 9co 5820 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3567 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 5822 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3645 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3644 . . 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 3152 . 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 1624 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  16376  xrsex  16377  xrsbas  16385  xrsadd  16386  xrsmul  16387  xrstset  16388  xrsle  16389  xrsds  16409
  Copyright terms: Public domain W3C validator