Database SURREAL NUMBERS Conway cut representation
Table of Contents - 15.3. Conway cut representation
In [Conway ] surreal numbers are represented as equivalence classes of cuts
of previously defined surreal numbers. This is complicated to handle in
ZFC without classes so we do not make it our definition. However, we can
define a cut operator on surreals that behaves similarly. We introduce
such an operator in this section and use it to define all surreals hearafter.
Conway cuts
csslt df-sslt cscut df-scut noeta2 brsslt ssltex1 ssltex2 ssltss1 ssltss2 ssltsep ssltd ssltsn ssltsepc ssltsepcd sssslt1 sssslt2 nulsslt nulssgt conway scutval scutcut scutcl scutcld scutbday eqscut eqscut2 sslttr ssltun1 ssltun2 scutun12 dmscut scutf etasslt etasslt2 scutbdaybnd scutbdaybnd2 scutbdaybnd2lim scutbdaylt slerec sltrec ssltdisj
Zero and One
c0s c1s df-0s df-1s 0sno 1sno bday0s 0slt1s bday0b bday1s cuteq0 cutneg cuteq1 sgt0ne0 sgt0ne0d 1sne0s
Cuts and Options
cmade cold cnew cleft cright df-made df-old df-new df-left df-right madeval madeval2 oldval newval madef oldf newf old0 madessno oldssno newssno leftval rightval elleft elright leftlt rightgt leftf rightf elmade elmade2 elold ssltleft ssltright lltropt made0 new0 old1 madess oldssmade leftssold rightssold leftssno rightssno madecut madeun madeoldsuc oldsuc oldlim madebdayim oldbdayim oldirr leftirr rightirr left0s right0s left1s right1s lrold madebdaylemold madebdaylemlrcut madebday oldbday newbday newbdayim lrcut scutfo sltn0 lruneq sltlpss slelss 0elold 0elleft 0elright madefi oldfi
Cofinality and coinitiality
cofsslt coinitsslt cofcut1 cofcut1d cofcut2 cofcut2d cofcutr cofcutr1d cofcutr2d cofcutrtime cofcutrtime1d cofcutrtime2d cofss coiniss cutlt cutpos cutmax cutmin