Skip to content

Commit

Permalink
Surreal Zero and One (#4585)
Browse files Browse the repository at this point in the history 
* move surreal zero, one to main

* document changes
  • Loading branch information
@sctfn
sctfn authored Jan 19, 2025
1 parent c3ba694 commit 4a0321b
Show file tree
Hide file tree
Showing 2 changed files with 116 additions and 114 deletions.
3 changes: 3 additions & 0 deletions changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,9 @@ make a github issue.)

DONE:
Date Old New Notes
19-Jan-25 --- --- Moved surreal zero and one theorems
from SF's mathbox to main set.mm
19-Jan-25 fnssintima [same] Moved from SF's mathbox to main set.mm
18-Jan-25 elintabg [same] Moved from RP's mathbox to main set.mm
17-Jan-25 --- --- Moved Conway cut theorems
from SF's mathbox to main set.mm
Expand Down
227 changes: 113 additions & 114 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70471,6 +70471,20 @@ complete lattice has a (least) fixpoint. Here we specialize this
cun csuc ) ADBDEACFBCFGCAHICBHICAJCBJGKKACCLQZFBSFACRZFBTFABCCMTSACNZOTSBUA
OP $.

${
$d A y $. $d B x y $. $d C x y $. $d F x y $.
$( Condition for subset of an intersection of an image. (Contributed by
Scott Fenton, 16-Aug-2024.) $)
fnssintima $p |- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <->
A. x e. B C C_ ( F ` x ) ) ) $=
( vy cima cint wss cv wcel wi wal wfn wa cfv wral bitri wceq albii df-ral
ssint wrex fvelimab imbi1d albidv ralcom4 eqcom imbi1i fvex sseq2 ceqsalv
ralbii r19.23v 3bitr3ri bitrdi bitrid ) DECGZHIZFJZURKZDUTIZLZFMZEBNCBIOZ
DAJZEPZIZACQZUSVBFURQVDFDURUBVBFURUARVEVDVGUTSZACUCZVBLZFMZVIVEVCVLFVEVAV
KVBABCUTEUDUEUFVJVBLZFMZACQVNACQZFMVIVMVNAFCUGVOVHACVOUTVGSZVBLZFMVHVNVRF
VJVQVBVGUTUHUITVBVHFVGVFEUJUTVGDUKULRUMVPVLFVJVBACUNTUOUPUQ $.
$}

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Cantor's Theorem
Expand Down Expand Up @@ -402505,6 +402519,105 @@ property of surreals and will be used (via surreal cuts) to prove many
DUE $.
$}

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Zero and One
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

$( Define new constants. $)
$c 0s 1s $.

$( Declare the class syntax for surreal zero. $)
c0s $a class 0s $.

$( Declare the class syntax for surreal one. $)
c1s $a class 1s $.

$( Define surreal zero. This is the simplest cut of surreal number sets.
Definition from [Conway] p. 17. (Contributed by Scott Fenton,
7-Aug-2024.) $)
df-0s $a |- 0s = ( (/) |s (/) ) $.

$( Define surreal one. This is the simplest number greater than surreal
zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton,
7-Aug-2024.) $)
df-1s $a |- 1s = ( { 0s } |s (/) ) $.

$( Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) $)
0sno $p |- 0s e. No $=
( c0s c0 cscut co csur df-0s csslt wbr wcel cpw 0elpw nulssgt ax-mp eqeltri
scutcl ) ABBCDZEFBBGHZPEIBEJIQEKBLMBBOMN $.

$( Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) $)
1sno $p |- 1s e. No $=
( c1s c0s csn c0 cscut csur df-1s csslt wbr wcel 0sno snelpwi ax-mp nulssgt
co cpw scutcl eqeltri ) ABCZDEOZFGSDHIZTFJSFPJZUABFJUBKBFLMSNMSDQMR $.

${
$d x y $.
$( Calculate the birthday of surreal zero. (Contributed by Scott Fenton,
7-Aug-2024.) $)
bday0s $p |- ( bday ` 0s ) = (/) $=
( vx c0s cbday cfv c0 cv csn csslt wa csur crab cima cint con0 cscut wcel
wbr co nulssgt 3eqtri df-0s fveq2i cpw wceq 0elpw scutbday mp2b eqtri cdm
crn snelpwi nulsslt jca rabeqc bdaydm eqtr4i imaeq2i imadmrn bdayrn inton
syl inteqi ) BCDZCEAFZGZHQZVEEHQZIZAJKZLZMZNMEVCEEORZCDZVKBVLCUAUBEJUCZPE
EHQVMVKUDJUEESAEEUFUGUHVJNVJCCUIZLCUJNVIVOCVIJVOVHAJVDJPVEVNPZVHVDJUKVPVF
VGVEULVESUMVAUNUOUPUQCURUSTVBUTT $.
$}

${
$d x y $.
$( Surreal zero is less than surreal one. Theorem from [Conway] p. 7.
(Contributed by Scott Fenton, 7-Aug-2024.) $)
0slt1s $p |- 0s <s 1s $=
( vx vy c0s c1s cslt wbr cv csle wrex c0 csur wcel 0sno ax-mp mpbir csslt
cscut co wceq nulssgt csn wo slerflex elexi breq2 rexsn orci wb cpw 0elpw
wss snssi snex elpw df-0s df-1s sltrec mp4an ) CDEFZCAGZHFZACUAZIZBGDHFBJ
IZUBZVCVDVCCCHFZCKLZVFMCUCNVAVFACCKMUDUTCCHUEUFOUGJJPFZVBJPFZCJJQRSDVBJQR
SUSVEUHJKUIZLVHKUJJTNVBVJLZVIVKVBKUKZVGVLMCKULNVBKCUMUNOVBTNUOUPJJVBJCDBA
UQURO $.
$}

${
$d X x $.
$( The only surreal with birthday ` (/) ` is ` 0s ` . (Contributed by
Scott Fenton, 8-Aug-2024.) $)
bday0b $p |- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) $=
( vx csur wcel cbday cfv c0 c0s wa cscut co df-0s csn csslt wbr cv adantr
wceq syl nulssgt wss wi cpw snelpwi nulsslt id 0ss eqsstrdi a1d ralrimivw
wral adantl wb 0elpw ax-mp eqscut2 mpan mpbir3and eqtr2id ex fveq2 bday0s
w3a eqtrdi impbid1 ) ACDZAEFZGRZAHRZVFVHVIVFVHIZHGGJKZALVJVKARZGAMZNOZVMG
NOZGBPZMZNOVQGNOIZVGVPEFZUAZUBZBCUKZVFVNVHVFVMCUCZDZVNACUDZVMUESQVFVOVHVF
WDVOWEVMTSQVJWABCVHWAVFVHVTVRVHVGGVSVHUFVSUGUHUIULUJVFVLVNVOWBVCUMZVHGGNO
ZVFWFGWCDWGCUNGTUOBGGAUPUQQURUSUTVIVGHEFGAHEVAVBVDVE $.
$}

${
$d x y z $.
$( The birthday of surreal one is ordinal one. (Contributed by Scott
Fenton, 8-Aug-2024.) $)
bday1s $p |- ( bday ` 1s ) = 1o $=
( vx vy vz cbday cfv c0s csn c1o cima csslt wbr csur wcel 0sno ax-mp wceq
c0 wss wral cslt c1s cscut df-1s fveq2i cun cuni csuc cpw snelpwi nulssgt
co scutbdaybnd2 un0 imaeq2i wfn bdayfn fnsnfv mp2an bday0s 3eqtr2i unieqi
sneqi 0ex unisn eqtri suceq df-1o eqtr4i sseqtri cv wa crab wb fnssintima
cint ssrab2 weq sneq breq2d breq1d anbi12d elrab wn sltirr breq2 necon2ai
wne mtbiri bday0b necon3bid syl5ibr word bdayelon onordi ordge1n0 syl6ibr
ssltsep ralsn ralbii elexi breq1 bitri sylib impel adantrr sylbi scutbday
vex mprgbir sseqtrri eqssi ) UADEFGZQUBUKZDEZHUAXMDUCUDXNHXNDXLQUEZIZUFZU
GZHXLQJKZXNXRRXLLUHMZXSFLMZXTNFLUIOXLUJOZXLQULOXRQUGZHXQQPXRYCPXQQGZUFQXP
YDXPDXLIZFDEZGZYDXOXLDXLUMUNDLUOZYAYGYEPUPNLFDUQURYFQUSVBUTVAQVCVDVEXQQVF
OVGVHVIHDXLAVJZGZJKZYJQJKZVKZALVLZIVOZXNHYORZHBVJZDEZRZBYNYHYNLRYPYSBYNSV
MUPYMALVPBLYNHDVNURYQYNMYQLMZXLYQGZJKZUUAQJKZVKZVKYSYMUUDAYQLABVQZYKUUBYL
UUCUUEYJUUAXLJYIYQVRZVSUUEYJUUAQJUUFVTWAWBYTUUBYSUUCYTFYQTKZYSUUBYTUUGYRQ
WGZYSUUGUUHYTYQFWGUUGYQFYQFPUUGFFTKZYAUUIWCNFWDOYQFFTWEWHWFYTYRQYQFYQWIWJ
WKYRWLYSUUHVMYRYQWMWNYRWOOWPUUBYICVJZTKZCUUASZAXLSZUUGACXLUUAWQUUMYIYQTKZ
AXLSUUGUULUUNAXLUUKUUNCYQBXHUUJYQYITWEWRWSUUNUUGAFFLNWTYIFYQTXAWRXBXCXDXE
XFXIXSXNYOPYBAXLQXGOXJXKVE $.
$}


$( End $[ set-surreals.mm $] $)

Expand Down Expand Up @@ -536087,20 +536200,6 @@ Real and complex numbers (cont.)
UAEZVKBTQEZEZVLBTNDZEZEZVNBCFVPVMEZVQVNEVOQEVRNPGVOQTHIVPVMBHIIVMUAEZVNVLEU
MVSUNQRTHIVMUABHIIUGVLVKEUOUARBHIIBRKIURRAHIIARKII $.

${
$d A y $. $d B x y $. $d C x y $. $d F x y $.
$( Condition for subset of an intersection of an image. (Contributed by
Scott Fenton, 16-Aug-2024.) $)
fnssintima $p |- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <->
A. x e. B C C_ ( F ` x ) ) ) $=
( vy cima cint wss cv wcel wi wal wfn wa cfv wral bitri wceq albii df-ral
ssint wrex fvelimab imbi1d albidv ralcom4 eqcom imbi1i fvex sseq2 ceqsalv
ralbii r19.23v 3bitr3ri bitrdi bitrid ) DECGZHIZFJZURKZDUTIZLZFMZEBNCBIOZ
DAJZEPZIZACQZUSVBFURQVDFDURUBVBFURUARVEVDVGUTSZACUCZVBLZFMZVIVEVCVLFVEVAV
KVBABCUTEUDUEUFVJVBLZFMZACQVNACQZFMVIVMVNAFCUGVOVHACVOUTVGSZVBLZFMVHVNVRF
VJVQVBVGUTUHUITVBVHFVGVFEUJUTVGDUKULRUMVPVLFVJVBACUNTUOUPUQ $.
$}

${
$d a b $. $d a ph $. $d a ps $. $d a x $. $d a y $. $d b ph $.
$d b ps $. $d b x $. $d b y $. $d ph y $. $d ps x $. $d x y $.
Expand Down Expand Up @@ -539541,106 +539640,6 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
wss ) ADEZBDEZCDEZFZABPACGHZBCGHZPCAGHZCBGHZPABCITUAUCUBUDQSUAUCJRACKLRSUBU
DJQBCKMNO $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Surreal numbers - zero and one
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

$( Define new constants. $)
$c 0s 1s $.

$( Declare the class syntax for surreal zero. $)
c0s $a class 0s $.

$( Declare the class syntax for surreal one. $)
c1s $a class 1s $.

$( Define surreal zero. This is the simplest cut of surreal number sets.
Definition from [Conway] p. 17. (Contributed by Scott Fenton,
7-Aug-2024.) $)
df-0s $a |- 0s = ( (/) |s (/) ) $.

$( Define surreal one. This is the simplest number greater than surreal
zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton,
7-Aug-2024.) $)
df-1s $a |- 1s = ( { 0s } |s (/) ) $.

$( Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) $)
0sno $p |- 0s e. No $=
( c0s c0 cscut co csur df-0s csslt wbr wcel cpw 0elpw nulssgt ax-mp eqeltri
scutcl ) ABBCDZEFBBGHZPEIBEJIQEKBLMBBOMN $.

$( Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) $)
1sno $p |- 1s e. No $=
( c1s c0s csn c0 cscut csur df-1s csslt wbr wcel 0sno snelpwi ax-mp nulssgt
co cpw scutcl eqeltri ) ABCZDEOZFGSDHIZTFJSFPJZUABFJUBKBFLMSNMSDQMR $.

${
$d x y $.
$( Calculate the birthday of surreal zero. (Contributed by Scott Fenton,
7-Aug-2024.) $)
bday0s $p |- ( bday ` 0s ) = (/) $=
( vx c0s cbday cfv c0 cv csn csslt wa csur crab cima cint con0 cscut wcel
wbr co nulssgt 3eqtri df-0s fveq2i cpw wceq 0elpw scutbday mp2b eqtri cdm
crn snelpwi nulsslt jca rabeqc bdaydm eqtr4i imaeq2i imadmrn bdayrn inton
syl inteqi ) BCDZCEAFZGZHQZVEEHQZIZAJKZLZMZNMEVCEEORZCDZVKBVLCUAUBEJUCZPE
EHQVMVKUDJUEESAEEUFUGUHVJNVJCCUIZLCUJNVIVOCVIJVOVHAJVDJPVEVNPZVHVDJUKVPVF
VGVEULVESUMVAUNUOUPUQCURUSTVBUTT $.
$}

${
$d x y $.
$( Surreal zero is less than surreal one. Theorem from [Conway] p. 7.
(Contributed by Scott Fenton, 7-Aug-2024.) $)
0slt1s $p |- 0s <s 1s $=
( vx vy c0s c1s cslt wbr cv csle wrex c0 csur wcel 0sno ax-mp mpbir csslt
cscut co wceq nulssgt csn wo slerflex elexi breq2 rexsn orci wb cpw 0elpw
wss snssi snex elpw df-0s df-1s sltrec mp4an ) CDEFZCAGZHFZACUAZIZBGDHFBJ
IZUBZVCVDVCCCHFZCKLZVFMCUCNVAVFACCKMUDUTCCHUEUFOUGJJPFZVBJPFZCJJQRSDVBJQR
SUSVEUHJKUIZLVHKUJJTNVBVJLZVIVKVBKUKZVGVLMCKULNVBKCUMUNOVBTNUOUPJJVBJCDBA
UQURO $.
$}

${
$d X x $.
$( The only surreal with birthday ` (/) ` is ` 0s ` . (Contributed by
Scott Fenton, 8-Aug-2024.) $)
bday0b $p |- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) $=
( vx csur wcel cbday cfv c0 c0s wa cscut co df-0s csn csslt wbr cv adantr
wceq syl nulssgt wss wi cpw snelpwi nulsslt id 0ss eqsstrdi a1d ralrimivw
wral adantl wb 0elpw ax-mp eqscut2 mpan mpbir3and eqtr2id ex fveq2 bday0s
w3a eqtrdi impbid1 ) ACDZAEFZGRZAHRZVFVHVIVFVHIZHGGJKZALVJVKARZGAMZNOZVMG
NOZGBPZMZNOVQGNOIZVGVPEFZUAZUBZBCUKZVFVNVHVFVMCUCZDZVNACUDZVMUESQVFVOVHVF
WDVOWEVMTSQVJWABCVHWAVFVHVTVRVHVGGVSVHUFVSUGUHUIULUJVFVLVNVOWBVCUMZVHGGNO
ZVFWFGWCDWGCUNGTUOBGGAUPUQQURUSUTVIVGHEFGAHEVAVBVDVE $.
$}

${
$d x y z $.
$( The birthday of surreal one is ordinal one. (Contributed by Scott
Fenton, 8-Aug-2024.) $)
bday1s $p |- ( bday ` 1s ) = 1o $=
( vx vy vz cbday cfv c0s csn c1o cima csslt wbr csur wcel 0sno ax-mp wceq
c0 wss wral cslt c1s cscut df-1s fveq2i cun cuni csuc cpw snelpwi nulssgt
co scutbdaybnd2 un0 imaeq2i wfn bdayfn fnsnfv mp2an bday0s 3eqtr2i unieqi
sneqi 0ex unisn eqtri suceq df-1o eqtr4i sseqtri cv wa crab wb fnssintima
cint ssrab2 weq sneq breq2d breq1d anbi12d elrab wn sltirr breq2 necon2ai
wne mtbiri bday0b necon3bid syl5ibr word bdayelon onordi ordge1n0 syl6ibr
ssltsep ralsn ralbii elexi breq1 bitri sylib impel adantrr sylbi scutbday
vex mprgbir sseqtrri eqssi ) UADEFGZQUBUKZDEZHUAXMDUCUDXNHXNDXLQUEZIZUFZU
GZHXLQJKZXNXRRXLLUHMZXSFLMZXTNFLUIOXLUJOZXLQULOXRQUGZHXQQPXRYCPXQQGZUFQXP
YDXPDXLIZFDEZGZYDXOXLDXLUMUNDLUOZYAYGYEPUPNLFDUQURYFQUSVBUTVAQVCVDVEXQQVF
OVGVHVIHDXLAVJZGZJKZYJQJKZVKZALVLZIVOZXNHYORZHBVJZDEZRZBYNYHYNLRYPYSBYNSV
MUPYMALVPBLYNHDVNURYQYNMYQLMZXLYQGZJKZUUAQJKZVKZVKYSYMUUDAYQLABVQZYKUUBYL
UUCUUEYJUUAXLJYIYQVRZVSUUEYJUUAQJUUFVTWAWBYTUUBYSUUCYTFYQTKZYSUUBYTUUGYRQ
WGZYSUUGUUHYTYQFWGUUGYQFYQFPUUGFFTKZYAUUIWCNFWDOYQFFTWEWHWFYTYRQYQFYQWIWJ
WKYRWLYSUUHVMYRYQWMWNYRWOOWPUUBYICVJZTKZCUUASZAXLSZUUGACXLUUAWQUUMYIYQTKZ
AXLSUUGUULUUNAXLUUKUUNCYQBXHUUJYQYITWEWRWSUUNUUGAFFLNWTYIFYQTXAWRXBXCXDXE
XFXIXSXNYOPYBAXLQXGOXJXKVE $.
$}


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Surreal numbers - cuts and options
Expand Down

0 comments on commit 4a0321b

Please sign in to comment.