From a30fe316459d6aeecf1ca48bf760c4c02426d187 Mon Sep 17 00:00:00 2001 From: Scott Fenton Date: Sun, 12 Jan 2025 13:55:24 -0500 Subject: [PATCH 1/2] move surreal birthday and density to main --- set.mm | 606 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 302 insertions(+), 304 deletions(-) diff --git a/set.mm b/set.mm index 1e662247a..f2718059d 100644 --- a/set.mm +++ b/set.mm @@ -53415,6 +53415,12 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few OQUPUQUR $. $} + $( Trichotomy law for strict orderings. (Contributed by Scott Fenton, + 8-Dec-2021.) $) + sotrine $p |- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> + ( B =/= C <-> ( B R C \/ C R B ) ) ) $= + ( wor wcel wa wbr wo wceq wn sotrieq bicomd necon1abid ) ADEBAFCAFGGZBCDHCB + DHIZBCOBCJPKABCDLMN $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -70273,6 +70279,16 @@ complete lattice has a (least) fixpoint. Here we specialize this ( wcel wn wo cres cfv wceq c0 exmid fvres nfvres orim12i ax-mp ) ABDZPEZFAC BGHZACHIZRJIZFPKPSQTABCLABCMNO $. + $( If ` (/) ` is not part of the range of a function ` F ` , then ` A ` is in + the domain of ` F ` iff ` ( F `` A ) =/= (/) ` . (Contributed by Scott + Fenton, 7-Dec-2021.) $) + funeldmb $p |- ( ( Fun F /\ -. (/) e. ran F ) -> + ( A e. dom F <-> ( F ` A ) =/= (/) ) ) $= + ( wfun c0 crn wcel wn wa cdm cfv wi fvelrn ex adantr wb eleq1 adantl sylibd + wceq con3d impancom ndmfv impbid1 necon2abid ) BCZDBEZFZGZHZABIFZABJZDUIUKD + SZUJGZUEULUHUMUEULHZUJUGUNUJUKUFFZUGUEUJUOKULUEUJUOABLMNULUOUGOUEUKDUFPQRTU + AABUBUCUD $. + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -399026,6 +399042,292 @@ a multiplicative function (but not completely multiplicative). ctp soseq ) ABEFGEHIEFIHFIPJCDKLCAMABCDNOQ $. $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Birthday Function +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d x y $. + $( The birthday function maps the surreals onto the ordinals. Axiom B of + [Alling] p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed + by Scott Fenton, 11-Jun-2011.) $) + bdayfo $p |- bday : No -onto-> On $= + ( vx vy csur con0 cbday wfo wfn crn wceq cdm wcel wral dmexg rgen df-bday + cv cvv mptfng mpbi c1o wrex cab rnmpt csn cxp noxp1o 1oex snnz dmxp ax-mp + wne eqcomi dmeq rspceeqv sylancl nodmon eleq1a syl rexlimiv impbii abbi2i + c0 wi eqtr4i df-fo mpbir2an ) CDEFECGZEHZDIAPZJZQKZACLVGVKACVICMNACVJEAOZ + RSVHBPZVJIZACUAZBUBDABCVJEVLUCVOBDVMDKZVOVPVMTUDZUEZCKVMVRJZIVOVMUFVSVMVQ + VBUKVSVMITUGUHVMVQUIUJULAVRCVJVSVMVIVRUMUNUOVNVPACVICKVJDKVNVPVCVIUPVJDVM + UQURUSUTVAVDCDEVEVF $. + $} + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Density +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + $( The value of a surreal at its birthday is ` (/) ` . (Contributed by Scott + Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) $) + fvnobday $p |- ( A e. No -> ( A ` ( bday ` A ) ) = (/) ) $= + ( csur wcel cbday cfv wn c0 wceq bdayval word nodmord ordirr eqneltrd ndmfv + cdm syl ) ABCZADEZAOZCFRAEGHQRSSAIQSJSSCFAKSLPMRANP $. + + ${ + $d A x $. $d B x $. + $( Lemma for ~ nosepne . (Contributed by Scott Fenton, 24-Nov-2021.) $) + nosepnelem $p |- ( ( A e. No /\ B e. No /\ A + ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= + ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) $= + ( csur wcel wbr cfv wne con0 wa c1o cop c2o wceq fvex simpl simpr neeq12d + c0 mpbiri cslt cv crab cint ctp sltval2 w3o brtp csuc df-2o df-1o eqeq12i + 1n0 wb 1on 0elon suc11 mp2an bitri necon3bii mpbir necomi 2on elexi prid2 + nosgnn0i 3jaoi sylbi syl6bi 3impia ) BDEZCDEZBCUAFZAUBZBGVNCGHAIUCUDZBGZV + OCGZHZVKVLJVMVPVQKSLKMLSMLUEFZVRBCAUFVSVPKNZVQSNZJZVTVQMNZJZVPSNZWCJZUGVR + KSKMSMVPVQVOBOVOCOUHWBVRWDWFWBVRKSHZUMWBVPKVQSVTWAPVTWAQRTWDVRKMHMKMKHWGU + MMKKSMKNKUIZSUIZNZKSNZMWHKWIUJUKULKIESIEWJWKUNUOUPKSUQURUSUTVAVBWDVPKVQMV + TWCPVTWCQRTWFVRSMHMKMMIVCVDVEVFWFVPSVQMWEWCPWEWCQRTVGVHVIVJ $. + + $( The value of two non-equal surreals at the first place they differ is + different. (Contributed by Scott Fenton, 24-Nov-2021.) $) + nosepne $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> + ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= + ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) $= + ( csur wcel wne cv cfv con0 crab cint wa cslt wbr wo wor nosepnelem necom + 3expia fveq2i wb sltso sotrine mpan wi rabbii inteqi neeq12i bitri sylibr + w3a ancoms jaod sylbid 3impia ) BDEZCDEZBCFZAGZBHZUSCHZFZAIJZKZBHZVDCHZFZ + UPUQLZURBCMNZCBMNZOZVGDMPVHURVKUAUBDBCMUCUDVHVIVGVJUPUQVIVGABCQSUQUPVJVGU + EUQUPVJVGUQUPVJUKVAUTFZAIJZKZCHZVNBHZFZVGACBQVGVPVOFVQVEVPVFVOVDVNBVCVMVB + VLAIUTVARUFUGZTVDVNCVRTUHVPVORUIUJSULUMUNUO $. + $} + + ${ + $d A x $. $d B x $. + $( If the value of a surreal at a separator is ` 1o ` then the surreal is + lesser. (Contributed by Scott Fenton, 7-Dec-2021.) $) + nosep1o $p |- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ + ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> + A + B + |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) $= + ( csur wcel wbr cfv wne con0 cdm wo wn wi wa c1o c0 cop c2o wceq syl cslt + w3a cv crab cint cun ctp sltval2 w3o fvex brtp df-3or ndmfv 1oex nosgnn0i + prid1 neeq1 mpbiri intnanrd ioran sylanbrc orel1 biimtrid 2on elexi prid2 + neneqd adantl con4i syl6 ex com23 sylbid 3impia orrd elun sylibr ) BDEZCD + EZBCUAFZUBZAUCZBGWBCGHAIUDUEZBJZEZWCCJZEZKWCWDWFUFEWAWEWGVRVSVTWELZWGMZVR + VSNZVTWCBGZWCCGZOPQORQPRQUGFZWIBCAUHWMWKOSZWLPSZNZWNWLRSZNZWKPSZWQNZUIZWJ + WIOPORPRWKWLWCBUJWCCUJUKWJWHXAWGWJWHXAWGMWJWHNZXAWTWGXAWPWRKZWTKZXBWTWPWR + WTULXBXCLZXDWTMWHXEWJWHWSXEWCBUMWSWPLWRLXEWSWNWOWSWKOWSWKOHPOHOORUNUPUOWK + POUQURVGZUSWSWNWQXFUSWPWRUTVATVHXCWTVBTVCWQWGWSWGWQWGLZWLRXGWOWLRHZWCCUMW + OXHPRHRORRIVDVEVFUOWLPRUQURTVGVIVHVJVKVLVCVMVNVOWCWDWFVPVQ $. + + $( The first place two surreals differ is an element of the larger of their + domains. (Contributed by Scott Fenton, 24-Nov-2021.) $) + nosepdm $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> + |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) $= + ( csur wcel wne cv cfv con0 crab cint cdm cun wa wbr wo wor wb nosepdmlem + cslt sltso sotrine 3expa simplr simpll simpr syl3anc necom rabbii 3eltr4g + mpan inteqi uncom jaodan ex sylbid 3impia ) BDEZCDEZBCFZAGZBHZVACHZFZAIJZ + KZBLZCLZMZEZURUSNZUTBCTOZCBTOZPZVJDTQVKUTVNRUADBCTUBUKVKVNVJVKVLVJVMURUSV + LVJABCSUCVKVMNZVCVBFZAIJZKZVHVGMZVFVIVOUSURVMVRVSEURUSVMUDURUSVMUEVKVMUFA + CBSUGVEVQVDVPAIVBVCUHUIULVGVHUMUJUNUOUPUQ $. + $} + + ${ + $d A x $. $d B x $. $d X x $. + $( The values of two surreals at a point less than their separators are + equal. (Contributed by Scott Fenton, 6-Dec-2021.) $) + nosepeq $p |- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ + X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> + ( A ` X ) = ( B ` X ) ) $= + ( csur wcel wne w3a cv cfv con0 crab cint wa wn wceq nosepon onelon sylan + fveq2 simpr neeq12d onnminsb sylc df-ne con2bii sylibr ) BEFCEFBCGHZDAIZB + JZUICJZGZAKLMZFZNZDBJZDCJZGZOZUPUQPZUODKFZUNUSUHUMKFUNVAABCQUMDRSUHUNUAUL + URADUIDPUJUPUKUQUIDBTUIDCTUBUCUDURUTUPUQUEUFUG $. + $} + + ${ + $d A x $. $d B x $. + $( Given two non-equal surreals, their separator is less than or equal to + the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. + (Contributed by Scott Fenton, 6-Dec-2021.) $) + nosepssdm $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> + |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A ) $= + ( csur wcel wne cfv con0 cdm wn wceq wa c0 wi word nodmord 3ad2ant1 ndmfv + wss syl w3a cv crab cint nosepne neneqd ordn2lp sylibr imp nosepeq simpl1 + imnan ordirr 3syl eqeq1d eqcom bitrdi crn wb simpl2 nofun c1o c2o nosgnn0 + wfun cpr norn sseld mtoi funeldmb syl2anc necon2bbid ordtr1 expdimp con3d + 3ad2ant2 sylbid mpd eqtr4d mtand nosepon nodmon ontri1 mpbird ) BDEZCDEZB + CFZUAZAUBZBGWICGFAHUCUDZBIZSZWKWJEZJZWHWMWJBGZWJCGZKWHWOWPABCUEUFWHWMLZWO + MWPWQWJWKEZJZWOMKWHWMWSWHWMWRLJZWMWSNWHWKOZWTWEWFXAWGBPZQWKWJUGTWMWRULUHU + IWJBRTWQWJCIZEZJZWPMKWQWKBGZWKCGZKZXEABCWKUJWQXHXGMKZXEWQXHMXGKXIWQXFMXGW + QXAWKWKEJXFMKWQWEXAWEWFWGWMUKXBTWKUMWKBRUNUOMXGUPUQWQXIWKXCEZJXEWQXJXGMWQ + CVEZMCURZEZJXJXGMFUSWQWFXKWEWFWGWMUTZCVATWQXMMVBVCVFZEVDWQXLXOMWQWFXLXOSX + NCVGTVHVIWKCVJVKVLWQXDXJWHWMXDXJWHXCOZWMXDLXJNWFWEXPWGCPVPWKWJXCVMTVNVOVQ + VQVRWJCRTVSVTWHWJHEWKHEZWLWNUSABCWAWEWFXQWGBWBQWJWKWCVKWD $. + $} + + ${ + $d A a $. $d B a $. + $( Lemma for ~ nodense . Show that a particular abstraction is an ordinal. + (Contributed by Scott Fenton, 16-Jun-2011.) $) + nodenselem4 $p |- ( ( ( A e. No /\ B e. No ) /\ A + |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On ) $= + ( csur wcel wa cslt wbr wne cv con0 crab cint simpll simplr wn wceq sltso + cfv wor sonr mpan adantr breq2 notbid syl5ibcom necon2ad nosepon syl3anc + imp ) ADEZBDEZFZABGHZFUKULABIZCJZASUPBSICKLMKEUKULUNNUKULUNOUMUNUOUMUNABU + MAAGHZPZABQZUNPUKURULDGTUKURRDAGUAUBUCUSUQUNABAGUDUEUFUGUJCABUHUI $. + $} + + ${ + $d A a $. $d B a $. + $( Lemma for ~ nodense . If the birthdays of two distinct surreals are + equal, then the ordinal from ~ nodenselem4 is an element of that + birthday. (Contributed by Scott Fenton, 16-Jun-2011.) $) + nodenselem5 $p |- ( ( ( A e. No /\ B e. No ) /\ + ( ( bday ` A ) = ( bday ` B ) /\ A + |^| { a e. On | ( + A ` a ) =/= ( B ` a ) } e. + ( bday ` A ) ) $= + ( csur wcel wa cbday cfv wceq cslt wbr cv wne con0 cdm cun wn bdayval syl + crab cint simpll simplr wi wor sltso sonr breq2 notbid syl5ibcom necon2ad + mpan adantr adantrl nosepdm syl3anc simprl uneq2d eqtr3di uneq12d 3eqtr3d + imp unidm eleqtrd eleqtrrd ) ADEZBDEZFZAGHZBGHZIZABJKZFZFZCLZAHVOBHMCNTUA + ZAOZVIVNVPVQBOZPZVQVNVFVGABMZVPVSEVFVGVMUBZVFVGVMUCZVHVLVTVKVHVLVTVFVLVTU + DVGVFVLABVFAAJKZQZABIZVLQDJUEVFWDUFDAJUGULWEWCVLABAJUHUIUJUKUMVBUNCABUOUP + VNVIVJPZVIVSVQVNVIVIPWFVIVNVIVJVIVHVKVLUQURVIVCUSVNVIVQVJVRVNVFVIVQIWAARS + ZVNVGVJVRIWBBRSUTWGVAVDWGVE $. + $} + + ${ + $d A a $. $d B a $. + $( The restriction of a surreal to the abstraction from ~ nodenselem4 is + still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) $) + nodenselem6 $p |- ( ( ( A e. No /\ B e. No ) /\ + ( ( bday ` A ) = ( bday ` B ) /\ A + ( A |` |^| { a e. On | ( + A ` a ) =/= ( B ` a ) } ) e. No ) $= + ( csur wcel wa cbday cfv wceq cslt wbr cv con0 crab cint cres nodenselem4 + wne simpll adantrl noreson syl2anc ) ADEZBDEZFZAGHBGHIZABJKZFZFUCCLZAHUIB + HRCMNOZMEZAUJPDEUCUDUHSUEUGUKUFABCQTAUJUAUB $. + $} + + ${ + $d A a $. $d B a $. $d C a $. + $( Lemma for ~ nodense . ` A ` and ` B ` are equal at all elements of the + abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) $) + nodenselem7 $p |- ( ( ( A e. No /\ B e. No ) /\ + ( ( bday ` A ) = ( bday ` B ) /\ A + ( C e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } + -> ( A ` C ) = ( B ` C ) ) ) $= + ( csur wcel wa cbday cfv wceq cslt wbr cv wne con0 crab cint w3a simpll + wn simplr wor sltso sonr mpan breq2 syl5ibcom necon2ad imp ad2ant2rl 3jca + notbid nosepeq sylan ex ) AEFZBEFZGAHIBHIJZABKLZGZGZCDMZAIVBBINDOPQFZCAIC + BIJZVAUPUQABNZRVCVDVAUPUQVEUPUQUTSUPUQUTUAUPUSVEUQURUPUSVEUPUSABUPAAKLZTZ + ABJZUSTEKUBUPVGUCEAKUDUEVHVFUSABAKUFULUGUHUIUJUKDABCUMUNUO $. + $} + + ${ + $d A a $. $d B a $. + $( Lemma for ~ nodense . Give a condition for surreal less than when two + surreals have the same birthday. (Contributed by Scott Fenton, + 19-Jun-2011.) $) + nodenselem8 $p |- ( ( A e. No /\ B e. No /\ + ( bday ` A ) = ( bday ` B ) ) -> + ( A + ( ( A ` + |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = + 1o /\ + ( B ` + |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = + 2o ) ) ) $= + ( csur wcel cbday cfv wceq wbr c1o c2o wa wi 3impia c0 cop wn nosgnn0 crn + fvex w3a cslt cv wne con0 crab cint nodenselem5 exp32 ctp sltval2 3adant3 + wb w3o brtp eleq2 biimpd cpr nofnbday fnfvelrn eleq1 syl5ibcom sylan norn + wfn sseld adantr syld mtoi ex adantl syl9r imp intnand 3ad2antl1 intnanrd + 3orel13 syl2anc com23 biimtrid sylbid mpdd 3mix2 sylibr syl5ibr impbid ) + ADEZBDEZAFGZBFGZHZUAZABUBIZCUCZAGWNBGUDCUEUFUGZAGZJHZWOBGZKHZLZWLWMWOWIEZ + WTWGWHWKWMXAMWGWHLZWKWMXAABCUHUINWLWMWPWRJOPJKPOKPUJIZXAWTMZWGWHWMXCUMWKA + BCUKULZXCWQWROHZLZWTWPOHZWSLZUNZWLXDJOJKOKWPWRWOATWOBTUOZWLXAXJWTWLXAXJWT + MZWLXALZXGQXIQXLXMXFWQWLXAXFQZWGWHWKXAXNMWKXAWOWJEZXBXNWKXAXOWIWJWOUPUQWH + XOXNMWGWHXOXNWHXOLZXFOJKURZEZRXPXFOBSZEZXRWHBWJVEZXOXFXTMBUSYAXOLWRXSEXFX + TWJWOBUTWROXSVAVBVCWHXTXRMXOWHXSXQOBVDVFVGVHVIVJVKVLNVMVNXMXHWSWGWHXAXHQW + KWGXALZXHXRRYBXHOASZEZXRWGAWIVEZXAXHYDMAUSYEXALWPYCEXHYDWIWOAUTWPOYCVAVBV + CWGYDXRMXAWGYCXQOAVDVFVGVHVIVOVPXGWTXIVQVRVJVSVTWAWBWTWMWLXCWTXJXCWTXGXIW + CXKWDXEWEWF $. + $} + + ${ + $d A a x y $. $d B a x y $. + $( Given two distinct surreals with the same birthday, there is an older + surreal lying between the two of them. Axiom SD of [Alling] p. 184. + (Contributed by Scott Fenton, 16-Jun-2011.) $) + nodense $p |- ( ( ( A e. No /\ B e. No ) /\ + ( ( bday ` A ) = ( bday ` B ) /\ A + E. x e. No ( ( bday ` x ) e. ( bday ` A ) /\ + A - ( B =/= C <-> ( B R C \/ C R B ) ) ) $= - ( wor wcel wa wbr wo wceq wn sotrieq bicomd necon1abid ) ADEBAFCAFGGZBCDHCB - DHIZBCOBCJPKABCDLMN $. - ${ $d F x y $. $d G x y $. $d X x y $. $d Y x y $. $( Law for adjoining an element to restrictions of functions. (Contributed @@ -533793,16 +534088,6 @@ Real and complex numbers (cont.) cun csuc ) ADBDEACFBCFGCAHICBHICAJCBJGKKACCLQZFBSFACRZFBTFABCCMTSACNZOTSBUA OP $. - $( If ` (/) ` is not part of the range of a function ` F ` , then ` A ` is in - the domain of ` F ` iff ` ( F `` A ) =/= (/) ` . (Contributed by Scott - Fenton, 7-Dec-2021.) $) - funeldmb $p |- ( ( Fun F /\ -. (/) e. ran F ) -> - ( A e. dom F <-> ( F ` A ) =/= (/) ) ) $= - ( wfun c0 crn wcel wn wa cdm cfv wi fvelrn ex adantr wb eleq1 adantl sylibd - wceq con3d impancom ndmfv impbid1 necon2abid ) BCZDBEZFZGZHZABIFZABJZDUIUKD - SZUJGZUEULUHUMUEULHZUJUGUNUJUKUFFZUGUEUJUOKULUEUJUOABLMNULUOUGOUEUKDUFPQRTU - AABUBUCUD $. - ${ $d A y z $. $d B y z $. $d F y z $. $d X y z $. elintfv.1 $e |- X e. _V $. @@ -536028,293 +536313,6 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= wss ) ADEZBDEZCDEZFZABPACGHZBCGHZPCAGHZCBGHZPABCITUAUCUBUDQSUAUCJRACKLRSUBU DJQBCKMNO $. -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Surreal Numbers: Birthday Function -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - ${ - $d x y $. - $( The birthday function maps the surreals onto the ordinals. Axiom B of - [Alling] p. 184. (Shortened proof on 2012-Apr-14, SF). (Contributed by - Scott Fenton, 11-Jun-2011.) $) - bdayfo $p |- bday : No -onto-> On $= - ( vx vy csur con0 cbday wfo wfn crn wceq cdm wcel wral dmexg rgen df-bday - cv cvv mptfng mpbi c1o wrex cab rnmpt csn cxp noxp1o 1oex snnz dmxp ax-mp - wne eqcomi dmeq rspceeqv sylancl nodmon eleq1a syl rexlimiv impbii abbi2i - c0 wi eqtr4i df-fo mpbir2an ) CDEFECGZEHZDIAPZJZQKZACLVGVKACVICMNACVJEAOZ - RSVHBPZVJIZACUAZBUBDABCVJEVLUCVOBDVMDKZVOVPVMTUDZUEZCKVMVRJZIVOVMUFVSVMVQ - VBUKVSVMITUGUHVMVQUIUJULAVRCVJVSVMVIVRUMUNUOVNVPACVICKVJDKVNVPVCVIUPVJDVM - UQURUSUTVAVDCDEVEVF $. - $} - - -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Surreal Numbers: Density -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - $( The value of a surreal at its birthday is ` (/) ` . (Contributed by Scott - Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) $) - fvnobday $p |- ( A e. No -> ( A ` ( bday ` A ) ) = (/) ) $= - ( csur wcel cbday cfv wn c0 wceq bdayval word nodmord ordirr eqneltrd ndmfv - cdm syl ) ABCZADEZAOZCFRAEGHQRSSAIQSJSSCFAKSLPMRANP $. - - ${ - $d A x $. $d B x $. - $( Lemma for ~ nosepne . (Contributed by Scott Fenton, 24-Nov-2021.) $) - nosepnelem $p |- ( ( A e. No /\ B e. No /\ A - ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= - ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) $= - ( csur wcel wbr cfv wne con0 wa c1o cop c2o wceq fvex simpl simpr neeq12d - c0 mpbiri cslt cv crab cint ctp sltval2 w3o brtp csuc df-2o df-1o eqeq12i - 1n0 wb 1on 0elon suc11 mp2an bitri necon3bii mpbir necomi 2on elexi prid2 - nosgnn0i 3jaoi sylbi syl6bi 3impia ) BDEZCDEZBCUAFZAUBZBGVNCGHAIUCUDZBGZV - OCGZHZVKVLJVMVPVQKSLKMLSMLUEFZVRBCAUFVSVPKNZVQSNZJZVTVQMNZJZVPSNZWCJZUGVR - KSKMSMVPVQVOBOVOCOUHWBVRWDWFWBVRKSHZUMWBVPKVQSVTWAPVTWAQRTWDVRKMHMKMKHWGU - MMKKSMKNKUIZSUIZNZKSNZMWHKWIUJUKULKIESIEWJWKUNUOUPKSUQURUSUTVAVBWDVPKVQMV - TWCPVTWCQRTWFVRSMHMKMMIVCVDVEVFWFVPSVQMWEWCPWEWCQRTVGVHVIVJ $. - - $( The value of two non-equal surreals at the first place they differ is - different. (Contributed by Scott Fenton, 24-Nov-2021.) $) - nosepne $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> - ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= - ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) $= - ( csur wcel wne cv cfv con0 crab cint wa cslt wbr wo wor nosepnelem necom - 3expia fveq2i wb sltso sotrine mpan wi rabbii inteqi neeq12i bitri sylibr - w3a ancoms jaod sylbid 3impia ) BDEZCDEZBCFZAGZBHZUSCHZFZAIJZKZBHZVDCHZFZ - UPUQLZURBCMNZCBMNZOZVGDMPVHURVKUAUBDBCMUCUDVHVIVGVJUPUQVIVGABCQSUQUPVJVGU - EUQUPVJVGUQUPVJUKVAUTFZAIJZKZCHZVNBHZFZVGACBQVGVPVOFVQVEVPVFVOVDVNBVCVMVB - VLAIUTVARUFUGZTVDVNCVRTUHVPVORUIUJSULUMUNUO $. - $} - - ${ - $d A x $. $d B x $. - $( If the value of a surreal at a separator is ` 1o ` then the surreal is - lesser. (Contributed by Scott Fenton, 7-Dec-2021.) $) - nosep1o $p |- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ - ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> - A - B - |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) $= - ( csur wcel wbr cfv wne con0 cdm wo wn wi wa c1o c0 cop c2o wceq syl cslt - w3a cv crab cint cun ctp sltval2 w3o fvex brtp df-3or ndmfv 1oex nosgnn0i - prid1 neeq1 mpbiri intnanrd ioran sylanbrc orel1 biimtrid 2on elexi prid2 - neneqd adantl con4i syl6 ex com23 sylbid 3impia orrd elun sylibr ) BDEZCD - EZBCUAFZUBZAUCZBGWBCGHAIUDUEZBJZEZWCCJZEZKWCWDWFUFEWAWEWGVRVSVTWELZWGMZVR - VSNZVTWCBGZWCCGZOPQORQPRQUGFZWIBCAUHWMWKOSZWLPSZNZWNWLRSZNZWKPSZWQNZUIZWJ - WIOPORPRWKWLWCBUJWCCUJUKWJWHXAWGWJWHXAWGMWJWHNZXAWTWGXAWPWRKZWTKZXBWTWPWR - WTULXBXCLZXDWTMWHXEWJWHWSXEWCBUMWSWPLWRLXEWSWNWOWSWKOWSWKOHPOHOORUNUPUOWK - POUQURVGZUSWSWNWQXFUSWPWRUTVATVHXCWTVBTVCWQWGWSWGWQWGLZWLRXGWOWLRHZWCCUMW - OXHPRHRORRIVDVEVFUOWLPRUQURTVGVIVHVJVKVLVCVMVNVOWCWDWFVPVQ $. - - $( The first place two surreals differ is an element of the larger of their - domains. (Contributed by Scott Fenton, 24-Nov-2021.) $) - nosepdm $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> - |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) $= - ( csur wcel wne cv cfv con0 crab cint cdm cun wa wbr wo wor wb nosepdmlem - cslt sltso sotrine 3expa simplr simpll simpr syl3anc necom rabbii 3eltr4g - mpan inteqi uncom jaodan ex sylbid 3impia ) BDEZCDEZBCFZAGZBHZVACHZFZAIJZ - KZBLZCLZMZEZURUSNZUTBCTOZCBTOZPZVJDTQVKUTVNRUADBCTUBUKVKVNVJVKVLVJVMURUSV - LVJABCSUCVKVMNZVCVBFZAIJZKZVHVGMZVFVIVOUSURVMVRVSEURUSVMUDURUSVMUEVKVMUFA - CBSUGVEVQVDVPAIVBVCUHUIULVGVHUMUJUNUOUPUQ $. - $} - - ${ - $d A x $. $d B x $. $d X x $. - $( The values of two surreals at a point less than their separators are - equal. (Contributed by Scott Fenton, 6-Dec-2021.) $) - nosepeq $p |- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ - X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> - ( A ` X ) = ( B ` X ) ) $= - ( csur wcel wne w3a cv cfv con0 crab cint wa wn wceq nosepon onelon sylan - fveq2 simpr neeq12d onnminsb sylc df-ne con2bii sylibr ) BEFCEFBCGHZDAIZB - JZUICJZGZAKLMZFZNZDBJZDCJZGZOZUPUQPZUODKFZUNUSUHUMKFUNVAABCQUMDRSUHUNUAUL - URADUIDPUJUPUKUQUIDBTUIDCTUBUCUDURUTUPUQUEUFUG $. - $} - - ${ - $d A x $. $d B x $. - $( Given two non-equal surreals, their separator is less than or equal to - the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. - (Contributed by Scott Fenton, 6-Dec-2021.) $) - nosepssdm $p |- ( ( A e. No /\ B e. No /\ A =/= B ) -> - |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A ) $= - ( csur wcel wne cfv con0 cdm wn wceq wa c0 wi word nodmord 3ad2ant1 ndmfv - wss syl w3a cv crab cint nosepne neneqd ordn2lp sylibr imp nosepeq simpl1 - imnan ordirr 3syl eqeq1d eqcom bitrdi crn wb simpl2 nofun c1o c2o nosgnn0 - wfun cpr norn sseld mtoi funeldmb syl2anc necon2bbid ordtr1 expdimp con3d - 3ad2ant2 sylbid mpd eqtr4d mtand nosepon nodmon ontri1 mpbird ) BDEZCDEZB - CFZUAZAUBZBGWICGFAHUCUDZBIZSZWKWJEZJZWHWMWJBGZWJCGZKWHWOWPABCUEUFWHWMLZWO - MWPWQWJWKEZJZWOMKWHWMWSWHWMWRLJZWMWSNWHWKOZWTWEWFXAWGBPZQWKWJUGTWMWRULUHU - IWJBRTWQWJCIZEZJZWPMKWQWKBGZWKCGZKZXEABCWKUJWQXHXGMKZXEWQXHMXGKXIWQXFMXGW - QXAWKWKEJXFMKWQWEXAWEWFWGWMUKXBTWKUMWKBRUNUOMXGUPUQWQXIWKXCEZJXEWQXJXGMWQ - CVEZMCURZEZJXJXGMFUSWQWFXKWEWFWGWMUTZCVATWQXMMVBVCVFZEVDWQXLXOMWQWFXLXOSX - NCVGTVHVIWKCVJVKVLWQXDXJWHWMXDXJWHXCOZWMXDLXJNWFWEXPWGCPVPWKWJXCVMTVNVOVQ - VQVRWJCRTVSVTWHWJHEWKHEZWLWNUSABCWAWEWFXQWGBWBQWJWKWCVKWD $. - $} - - ${ - $d A a $. $d B a $. - $( Lemma for ~ nodense . Show that a particular abstraction is an ordinal. - (Contributed by Scott Fenton, 16-Jun-2011.) $) - nodenselem4 $p |- ( ( ( A e. No /\ B e. No ) /\ A - |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On ) $= - ( csur wcel wa cslt wbr wne cv con0 crab cint simpll simplr wn wceq sltso - cfv wor sonr mpan adantr breq2 notbid syl5ibcom necon2ad nosepon syl3anc - imp ) ADEZBDEZFZABGHZFUKULABIZCJZASUPBSICKLMKEUKULUNNUKULUNOUMUNUOUMUNABU - MAAGHZPZABQZUNPUKURULDGTUKURRDAGUAUBUCUSUQUNABAGUDUEUFUGUJCABUHUI $. - $} - - ${ - $d A a $. $d B a $. - $( Lemma for ~ nodense . If the birthdays of two distinct surreals are - equal, then the ordinal from ~ nodenselem4 is an element of that - birthday. (Contributed by Scott Fenton, 16-Jun-2011.) $) - nodenselem5 $p |- ( ( ( A e. No /\ B e. No ) /\ - ( ( bday ` A ) = ( bday ` B ) /\ A - |^| { a e. On | ( - A ` a ) =/= ( B ` a ) } e. - ( bday ` A ) ) $= - ( csur wcel wa cbday cfv wceq cslt wbr cv wne con0 cdm cun wn bdayval syl - crab cint simpll simplr wi wor sltso sonr breq2 notbid syl5ibcom necon2ad - mpan adantr adantrl nosepdm syl3anc simprl uneq2d eqtr3di uneq12d 3eqtr3d - imp unidm eleqtrd eleqtrrd ) ADEZBDEZFZAGHZBGHZIZABJKZFZFZCLZAHVOBHMCNTUA - ZAOZVIVNVPVQBOZPZVQVNVFVGABMZVPVSEVFVGVMUBZVFVGVMUCZVHVLVTVKVHVLVTVFVLVTU - DVGVFVLABVFAAJKZQZABIZVLQDJUEVFWDUFDAJUGULWEWCVLABAJUHUIUJUKUMVBUNCABUOUP - VNVIVJPZVIVSVQVNVIVIPWFVIVNVIVJVIVHVKVLUQURVIVCUSVNVIVQVJVRVNVFVIVQIWAARS - ZVNVGVJVRIWBBRSUTWGVAVDWGVE $. - $} - - ${ - $d A a $. $d B a $. - $( The restriction of a surreal to the abstraction from ~ nodenselem4 is - still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) $) - nodenselem6 $p |- ( ( ( A e. No /\ B e. No ) /\ - ( ( bday ` A ) = ( bday ` B ) /\ A - ( A |` |^| { a e. On | ( - A ` a ) =/= ( B ` a ) } ) e. No ) $= - ( csur wcel wa cbday cfv wceq cslt wbr cv con0 crab cint cres nodenselem4 - wne simpll adantrl noreson syl2anc ) ADEZBDEZFZAGHBGHIZABJKZFZFUCCLZAHUIB - HRCMNOZMEZAUJPDEUCUDUHSUEUGUKUFABCQTAUJUAUB $. - $} - - ${ - $d A a $. $d B a $. $d C a $. - $( Lemma for ~ nodense . ` A ` and ` B ` are equal at all elements of the - abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) $) - nodenselem7 $p |- ( ( ( A e. No /\ B e. No ) /\ - ( ( bday ` A ) = ( bday ` B ) /\ A - ( C e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } - -> ( A ` C ) = ( B ` C ) ) ) $= - ( csur wcel wa cbday cfv wceq cslt wbr cv wne con0 crab cint w3a simpll - wn simplr wor sltso sonr mpan breq2 syl5ibcom necon2ad imp ad2ant2rl 3jca - notbid nosepeq sylan ex ) AEFZBEFZGAHIBHIJZABKLZGZGZCDMZAIVBBINDOPQFZCAIC - BIJZVAUPUQABNZRVCVDVAUPUQVEUPUQUTSUPUQUTUAUPUSVEUQURUPUSVEUPUSABUPAAKLZTZ - ABJZUSTEKUBUPVGUCEAKUDUEVHVFUSABAKUFULUGUHUIUJUKDABCUMUNUO $. - $} - - ${ - $d A a $. $d B a $. - $( Lemma for ~ nodense . Give a condition for surreal less than when two - surreals have the same birthday. (Contributed by Scott Fenton, - 19-Jun-2011.) $) - nodenselem8 $p |- ( ( A e. No /\ B e. No /\ - ( bday ` A ) = ( bday ` B ) ) -> - ( A - ( ( A ` - |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = - 1o /\ - ( B ` - |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = - 2o ) ) ) $= - ( csur wcel cbday cfv wceq wbr c1o c2o wa wi 3impia c0 cop wn nosgnn0 crn - fvex w3a cslt cv wne con0 crab cint nodenselem5 exp32 ctp sltval2 3adant3 - wb w3o brtp eleq2 biimpd cpr nofnbday fnfvelrn eleq1 syl5ibcom sylan norn - wfn sseld adantr syld mtoi ex adantl syl9r imp intnand 3ad2antl1 intnanrd - 3orel13 syl2anc com23 biimtrid sylbid mpdd 3mix2 sylibr syl5ibr impbid ) - ADEZBDEZAFGZBFGZHZUAZABUBIZCUCZAGWNBGUDCUEUFUGZAGZJHZWOBGZKHZLZWLWMWOWIEZ - WTWGWHWKWMXAMWGWHLZWKWMXAABCUHUINWLWMWPWRJOPJKPOKPUJIZXAWTMZWGWHWMXCUMWKA - BCUKULZXCWQWROHZLZWTWPOHZWSLZUNZWLXDJOJKOKWPWRWOATWOBTUOZWLXAXJWTWLXAXJWT - MZWLXALZXGQXIQXLXMXFWQWLXAXFQZWGWHWKXAXNMWKXAWOWJEZXBXNWKXAXOWIWJWOUPUQWH - XOXNMWGWHXOXNWHXOLZXFOJKURZEZRXPXFOBSZEZXRWHBWJVEZXOXFXTMBUSYAXOLWRXSEXFX - TWJWOBUTWROXSVAVBVCWHXTXRMXOWHXSXQOBVDVFVGVHVIVJVKVLNVMVNXMXHWSWGWHXAXHQW - KWGXALZXHXRRYBXHOASZEZXRWGAWIVEZXAXHYDMAUSYEXALWPYCEXHYDWIWOAUTWPOYCVAVBV - CWGYDXRMXAWGYCXQOAVDVFVGVHVIVOVPXGWTXIVQVRVJVSVTWAWBWTWMWLXCWTXJXCWTXGXIW - CXKWDXEWEWF $. - $} - - ${ - $d A a x y $. $d B a x y $. - $( Given two distinct surreals with the same birthday, there is an older - surreal lying between the two of them. Axiom SD of [Alling] p. 184. - (Contributed by Scott Fenton, 16-Jun-2011.) $) - nodense $p |- ( ( ( A e. No /\ B e. No ) /\ - ( ( bday ` A ) = ( bday ` B ) /\ A - E. x e. No ( ( bday ` x ) e. ( bday ` A ) /\ - A Date: Sun, 12 Jan 2025 13:56:08 -0500 Subject: [PATCH 2/2] document moves --- changes-set.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/changes-set.txt b/changes-set.txt index 22211ddeb..6e7f5cce8 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -87,6 +87,10 @@ make a github issue.) DONE: Date Old New Notes +12-Jan-25 --- --- Moved surreal birthday and density theorems + from SF's mathbox to main set.mm +12-Jan-25 sotrine [same] Moved from SF's mathbox to main set.mm +12-Jan-25 funeldmb [same] Moved from SF's mathbox to main set.mm 11-Jan-25 --- --- Moved surreal ordering theorems from SF's mathbox to main set.mm 11-Jan-25 --- --- Moved ordinal sequence theorems from