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

Definition df-xrs 13403
 Description: The extended real number structure. Unlike df-cnfld 16378, 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 16378. 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 is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make an isolated point since there is nothing else in the -ball around it). All components of this structure agree with ℂfld when restricted to . (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xrs TopSet ordTop
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-xrs
StepHypRef Expression
1 cxrs 13399 . 2
2 cnx 13145 . . . . . 6
3 cbs 13148 . . . . . 6
42, 3cfv 5255 . . . . 5
5 cxr 8866 . . . . 5
64, 5cop 3643 . . . 4
7 cplusg 13208 . . . . . 6
82, 7cfv 5255 . . . . 5
9 cxad 10450 . . . . 5
108, 9cop 3643 . . . 4
11 cmulr 13209 . . . . . 6
122, 11cfv 5255 . . . . 5
13 cxmu 10451 . . . . 5
1412, 13cop 3643 . . . 4
156, 10, 14ctp 3642 . . 3
16 cts 13214 . . . . . 6 TopSet
172, 16cfv 5255 . . . . 5 TopSet
18 cle 8868 . . . . . 6
19 cordt 13398 . . . . . 6 ordTop
2018, 19cfv 5255 . . . . 5 ordTop
2117, 20cop 3643 . . . 4 TopSet ordTop
22 cple 13215 . . . . . 6
232, 22cfv 5255 . . . . 5
2423, 18cop 3643 . . . 4
25 cds 13217 . . . . . 6
262, 25cfv 5255 . . . . 5
27 vx . . . . . 6
28 vy . . . . . 6
2927cv 1622 . . . . . . . 8
3028cv 1622 . . . . . . . 8
3129, 30, 18wbr 4023 . . . . . . 7
3229cxne 10449 . . . . . . . 8
3330, 32, 9co 5858 . . . . . . 7
3430cxne 10449 . . . . . . . 8
3529, 34, 9co 5858 . . . . . . 7
3631, 33, 35cif 3565 . . . . . 6
3727, 28, 5, 5, 36cmpt2 5860 . . . . 5
3826, 37cop 3643 . . . 4
3921, 24, 38ctp 3642 . . 3 TopSet ordTop
4015, 39cun 3150 . 2 TopSet ordTop
411, 40wceq 1623 1 TopSet ordTop
 Colors of variables: wff set class This definition is referenced by:  xrsstr  16381  xrsex  16382  xrsbas  16390  xrsadd  16391  xrsmul  16392  xrstset  16393  xrsle  16394  xrsds  16414
 Copyright terms: Public domain W3C validator