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
cslts df-slts ccuts df-cuts noeta2 brslts sltsex1 sltsex2 sltsss1 sltsss2 sltssep sltsd sltssnb sltssn sltssepc sltssepcd ssslts1 ssslts2 nulslts nulsgts nulsltsd nulsgtsd conway cutsval cutcuts cutscl cutscld cutbday eqcuts eqcuts2 sltstr sltsun1 sltsun2 cutsun12 dmcuts cutsf etaslts etaslts2 cutbdaybnd cutbdaybnd2 cutbdaybnd2lim cutbdaylt lesrec lesrecd ltsrec ltsrecd sltsdisj eqcuts3
Zero and One
c0s c1s df-0s df-1s 0no 1no bday0 0lt1s bday0b bday1 cuteq0 cutneg cuteq1 gt0ne0s gt0ne0sd 1ne0s rightge0
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 madeno oldno newno madenod oldnod newnod leftval rightval elleft elright leftlt rightgt leftf rightf elmade elmade2 elold sltsleft sltsright lltr made0 new0 old1 madess oldssmade oldmade oldmaded oldss leftssold rightssold leftssno rightssno leftold rightold leftno rightno leftoldd leftnod rightoldd rightnod madecut madeun madeoldsuc oldsuc oldlim madebdayim oldbdayim oldirr leftirr rightirr left0s right0s left1s right1s lrold madebdaylemold madebdaylemlrcut madebday oldbday newbday newbdayim lrcut cutsfo ltsn0 lruneq ltslpss leslss 0elold 0elleft 0elright madefi oldfi bdayiun bdayle sltsbday
Cofinality and coinitiality
cofslts coinitslts cofcut1 cofcut1d cofcut2 cofcut2d cofcutr cofcutr1d cofcutr2d cofcutrtime cofcutrtime1d cofcutrtime2d cofss coiniss cutlt cutpos cutmax cutmin cutminmax