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

Definition df-xrs 13681
Description: The extended real number structure. Unlike df-cnfld 16659, 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 16659. 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 13677 . 2  class  RR* s
2 cnx 13421 . . . . . 6  class  ndx
3 cbs 13424 . . . . . 6  class  Base
42, 3cfv 5413 . . . . 5  class  ( Base `  ndx )
5 cxr 9075 . . . . 5  class  RR*
64, 5cop 3777 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 13484 . . . . . 6  class  +g
82, 7cfv 5413 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 10664 . . . . 5  class  + e
108, 9cop 3777 . . . 4  class  <. ( +g  `  ndx ) ,  + e >.
11 cmulr 13485 . . . . . 6  class  .r
122, 11cfv 5413 . . . . 5  class  ( .r
`  ndx )
13 cxmu 10665 . . . . 5  class  x e
1412, 13cop 3777 . . . 4  class  <. ( .r `  ndx ) ,  x e >.
156, 10, 14ctp 3776 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }
16 cts 13490 . . . . . 6  class TopSet
172, 16cfv 5413 . . . . 5  class  (TopSet `  ndx )
18 cle 9077 . . . . . 6  class  <_
19 cordt 13676 . . . . . 6  class ordTop
2018, 19cfv 5413 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3777 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 13491 . . . . . 6  class  le
232, 22cfv 5413 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3777 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 13493 . . . . . 6  class  dist
262, 25cfv 5413 . . . . 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 4172 . . . . . . 7  wff  x  <_ 
y
3229cxne 10663 . . . . . . . 8  class  - e
x
3330, 32, 9co 6040 . . . . . . 7  class  ( y + e  - e
x )
3430cxne 10663 . . . . . . . 8  class  - e
y
3529, 34, 9co 6040 . . . . . . 7  class  ( x + e  - e
y )
3631, 33, 35cif 3699 . . . . . 6  class  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) )
3727, 28, 5, 5, 36cmpt2 6042 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y + e  - e x ) ,  ( x + e  - e y ) ) )
3826, 37cop 3777 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >.
3921, 24, 38ctp 3776 . . 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 3278 . 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  16670  xrsex  16671  xrsbas  16672  xrsadd  16673  xrsmul  16674  xrstset  16675  xrsle  16676  xrsds  16696
  Copyright terms: Public domain W3C validator