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

Definition df-xrs 14432
Description: The extended real number structure. Unlike df-cnfld 17794, 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 17794. 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 14430 . 2  class  RR*s
2 cnx 14163 . . . . . 6  class  ndx
3 cbs 14166 . . . . . 6  class  Base
42, 3cfv 5413 . . . . 5  class  ( Base `  ndx )
5 cxr 9409 . . . . 5  class  RR*
64, 5cop 3878 . . . 4  class  <. ( Base `  ndx ) , 
RR* >.
7 cplusg 14230 . . . . . 6  class  +g
82, 7cfv 5413 . . . . 5  class  ( +g  ` 
ndx )
9 cxad 11079 . . . . 5  class  +e
108, 9cop 3878 . . . 4  class  <. ( +g  `  ndx ) ,  +e >.
11 cmulr 14231 . . . . . 6  class  .r
122, 11cfv 5413 . . . . 5  class  ( .r
`  ndx )
13 cxmu 11080 . . . . 5  class  xe
1412, 13cop 3878 . . . 4  class  <. ( .r `  ndx ) ,  xe >.
156, 10, 14ctp 3876 . . 3  class  { <. (
Base `  ndx ) , 
RR* >. ,  <. ( +g  `  ndx ) ,  +e >. ,  <. ( .r `  ndx ) ,  xe >. }
16 cts 14236 . . . . . 6  class TopSet
172, 16cfv 5413 . . . . 5  class  (TopSet `  ndx )
18 cle 9411 . . . . . 6  class  <_
19 cordt 14429 . . . . . 6  class ordTop
2018, 19cfv 5413 . . . . 5  class  (ordTop `  <_  )
2117, 20cop 3878 . . . 4  class  <. (TopSet ` 
ndx ) ,  (ordTop `  <_  ) >.
22 cple 14237 . . . . . 6  class  le
232, 22cfv 5413 . . . . 5  class  ( le
`  ndx )
2423, 18cop 3878 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
25 cds 14239 . . . . . 6  class  dist
262, 25cfv 5413 . . . . 5  class  ( dist `  ndx )
27 vx . . . . . 6  setvar  x
28 vy . . . . . 6  setvar  y
2927cv 1368 . . . . . . . 8  class  x
3028cv 1368 . . . . . . . 8  class  y
3129, 30, 18wbr 4287 . . . . . . 7  wff  x  <_ 
y
3229cxne 11078 . . . . . . . 8  class  -e
x
3330, 32, 9co 6086 . . . . . . 7  class  ( y +e  -e
x )
3430cxne 11078 . . . . . . . 8  class  -e
y
3529, 34, 9co 6086 . . . . . . 7  class  ( x +e  -e
y )
3631, 33, 35cif 3786 . . . . . 6  class  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) )
3727, 28, 5, 5, 36cmpt2 6088 . . . . 5  class  ( x  e.  RR* ,  y  e. 
RR*  |->  if ( x  <_  y ,  ( y +e  -e x ) ,  ( x +e  -e y ) ) )
3826, 37cop 3878 . . . 4  class  <. ( dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y +e  -e x ) ,  ( x +e  -e y ) ) ) >.
3921, 24, 38ctp 3876 . . 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 3321 . 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 1369 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  17805  xrsex  17806  xrsbas  17807  xrsadd  17808  xrsmul  17809  xrstset  17810  xrsle  17811  xrsds  17831
  Copyright terms: Public domain W3C validator