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

Definition df-xrs 13685
Description: The extended real number structure. Unlike df-cnfld 16663, 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 16663. 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 13681 . 2  class  RR* s
2 cnx 13425 . . . . . 6  class  ndx
3 cbs 13428 . . . . . 6  class  Base
42, 3cfv 5417 . . . . 5  class  ( Base `  ndx )
5 cxr 9079 . . . . 5  class  RR*
64, 5cop 3781 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13488 . . . . . 6  class  +g
82, 7cfv 5417 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10668 . . . . 5  class  + e
108, 9cop 3781 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13489 . . . . . 6  class  .r
122, 11cfv 5417 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10669 . . . . 5  class  x e
1412, 13cop 3781 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3780 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13494 . . . . . 6  class TopSet
172, 16cfv 5417 . . . . 5  class  (TopSet `  ndx )
18 cle 9081 . . . . . 6  class  <_
19 cordt 13680 . . . . . 6  class ordTop
2018, 19cfv 5417 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3781 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13495 . . . . . 6  class  le
232, 22cfv 5417 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3781 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13497 . . . . . 6  class  dist
262, 25cfv 5417 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  set  x
28 vy . . . . . 6  set  y
2927cv 1648 . . . . . . . 8  class  x
3028cv 1648 . . . . . . . 8  class  y
3129, 30, 18wbr 4176 . . . . . . 7  wff  x  <_ 
y
3229cxne 10667 . . . . . . . 8  class  - e
x
3330, 32, 9co 6044 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10667 . . . . . . . 8  class  - e
y
3529, 34, 9co 6044 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3703 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 6046 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3781 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3780 . . 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 3282 . 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 1649 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  16674  xrsex  16675  xrsbas  16676  xrsadd  16677  xrsmul  16678  xrstset  16679  xrsle  16680  xrsds  16700
  Copyright terms: Public domain W3C validator