![]() |
Metamath
Proof Explorer Theorem List (p. 274 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scutval 27301* | The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β (π΄ |s π΅) = (β©π₯ β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)} ( bday βπ₯) = β© ( bday β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)}))) | ||
Theorem | scutcut 27302 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β ((π΄ |s π΅) β No β§ π΄ <<s {(π΄ |s π΅)} β§ {(π΄ |s π΅)} <<s π΅)) | ||
Theorem | scutcl 27303 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
β’ (π΄ <<s π΅ β (π΄ |s π΅) β No ) | ||
Theorem | scutcld 27304 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
β’ (π β π΄ <<s π΅) β β’ (π β (π΄ |s π΅) β No ) | ||
Theorem | scutbday 27305* | The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β ( bday β(π΄ |s π΅)) = β© ( bday β {π₯ β No β£ (π΄ <<s {π₯} β§ {π₯} <<s π΅)})) | ||
Theorem | eqscut 27306* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((πΏ <<s π β§ π β No ) β ((πΏ |s π ) = π β (πΏ <<s {π} β§ {π} <<s π β§ ( bday βπ) = β© ( bday β {π¦ β No β£ (πΏ <<s {π¦} β§ {π¦} <<s π )})))) | ||
Theorem | eqscut2 27307* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((πΏ <<s π β§ π β No ) β ((πΏ |s π ) = π β (πΏ <<s {π} β§ {π} <<s π β§ βπ¦ β No ((πΏ <<s {π¦} β§ {π¦} <<s π ) β ( bday βπ) β ( bday βπ¦))))) | ||
Theorem | sslttr 27308 | Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ π΅ <<s πΆ β§ π΅ β β ) β π΄ <<s πΆ) | ||
Theorem | ssltun1 27309 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s πΆ β§ π΅ <<s πΆ) β (π΄ βͺ π΅) <<s πΆ) | ||
Theorem | ssltun2 27310 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ π΄ <<s πΆ) β π΄ <<s (π΅ βͺ πΆ)) | ||
Theorem | scutun12 27311 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ πΆ <<s {(π΄ |s π΅)} β§ {(π΄ |s π΅)} <<s π·) β ((π΄ βͺ πΆ) |s (π΅ βͺ π·)) = (π΄ |s π΅)) | ||
Theorem | dmscut 27312 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ dom |s = <<s | ||
Theorem | scutf 27313 | Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
β’ |s : <<s βΆ No | ||
Theorem | etasslt 27314* | A restatement of noeta 27246 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ π β On β§ ( bday β (π΄ βͺ π΅)) β π) β βπ₯ β No (π΄ <<s {π₯} β§ {π₯} <<s π΅ β§ ( bday βπ₯) β π)) | ||
Theorem | etasslt2 27315* | A version of etasslt 27314 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.) |
β’ (π΄ <<s π΅ β βπ₯ β No (π΄ <<s {π₯} β§ {π₯} <<s π΅ β§ ( bday βπ₯) β suc βͺ ( bday β (π΄ βͺ π΅)))) | ||
Theorem | scutbdaybnd 27316 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ π β On β§ ( bday β (π΄ βͺ π΅)) β π) β ( bday β(π΄ |s π΅)) β π) | ||
Theorem | scutbdaybnd2 27317 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
β’ (π΄ <<s π΅ β ( bday β(π΄ |s π΅)) β suc βͺ ( bday β (π΄ βͺ π΅))) | ||
Theorem | scutbdaybnd2lim 27318 | An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ Lim ( bday β(π΄ |s π΅))) β ( bday β(π΄ |s π΅)) β βͺ ( bday β (π΄ βͺ π΅))) | ||
Theorem | scutbdaylt 27319 | If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ ((π β No β§ (π΄ <<s {π} β§ {π} <<s π΅) β§ π β (π΄ |s π΅)) β ( bday β(π΄ |s π΅)) β ( bday βπ)) | ||
Theorem | slerec 27320* | A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ (((π΄ <<s π΅ β§ πΆ <<s π·) β§ (π = (π΄ |s π΅) β§ π = (πΆ |s π·))) β (π β€s π β (βπ β π· π <s π β§ βπ β π΄ π <s π))) | ||
Theorem | sltrec 27321* | A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ (((π΄ <<s π΅ β§ πΆ <<s π·) β§ (π = (π΄ |s π΅) β§ π = (πΆ |s π·))) β (π <s π β (βπ β πΆ π β€s π β¨ βπ β π΅ π β€s π))) | ||
Theorem | ssltdisj 27322 | If π΄ preceeds π΅, then π΄ and π΅ are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.) |
β’ (π΄ <<s π΅ β (π΄ β© π΅) = β ) | ||
Syntax | c0s 27323 | Declare the class syntax for surreal zero. |
class 0s | ||
Syntax | c1s 27324 | Declare the class syntax for surreal one. |
class 1s | ||
Definition | df-0s 27325 | Define surreal zero. This is the simplest cut of surreal number sets. Definition from [Conway] p. 17. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s = (β |s β ) | ||
Definition | df-1s 27326 | Define surreal one. This is the simplest number greater than surreal zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 1s = ({ 0s } |s β ) | ||
Theorem | 0sno 27327 | Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s β No | ||
Theorem | 1sno 27328 | Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 1s β No | ||
Theorem | bday0s 27329 | Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( bday β 0s ) = β | ||
Theorem | 0slt1s 27330 | Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s <s 1s | ||
Theorem | bday0b 27331 | The only surreal with birthday β is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π β No β (( bday βπ) = β β π = 0s )) | ||
Theorem | bday1s 27332 | The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ( bday β 1s ) = 1o | ||
Theorem | cuteq0 27333 | Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.) |
β’ (π β π΄ <<s { 0s }) & β’ (π β { 0s } <<s π΅) β β’ (π β (π΄ |s π΅) = 0s ) | ||
Theorem | cuteq1 27334 | Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ (π β 0s β π΄) & β’ (π β π΄ <<s { 1s }) & β’ (π β { 1s } <<s π΅) β β’ (π β (π΄ |s π΅) = 1s ) | ||
Theorem | sgt0ne0 27335 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ ( 0s <s π΄ β π΄ β 0s ) | ||
Theorem | sgt0ne0d 27336 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ (π β 0s <s π΄) β β’ (π β π΄ β 0s ) | ||
Syntax | cmade 27337 | Declare the symbol for the made by function. |
class M | ||
Syntax | cold 27338 | Declare the symbol for the older than function. |
class O | ||
Syntax | cnew 27339 | Declare the symbol for the new on function. |
class N | ||
Syntax | cleft 27340 | Declare the symbol for the left option function. |
class L | ||
Syntax | cright 27341 | Declare the symbol for the right option function. |
class R | ||
Definition | df-made 27342 | Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ M = recs((π β V β¦ ( |s β (π« βͺ ran π Γ π« βͺ ran π)))) | ||
Definition | df-old 27343 | Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ O = (π₯ β On β¦ βͺ ( M β π₯)) | ||
Definition | df-new 27344 | Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ N = (π₯ β On β¦ (( M βπ₯) β ( O βπ₯))) | ||
Definition | df-left 27345* | Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ L = (π₯ β No β¦ {π¦ β ( O β( bday βπ₯)) β£ π¦ <s π₯}) | ||
Definition | df-right 27346* | Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ R = (π₯ β No β¦ {π¦ β ( O β( bday βπ₯)) β£ π₯ <s π¦}) | ||
Theorem | madeval 27347 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ (π΄ β On β ( M βπ΄) = ( |s β (π« βͺ ( M β π΄) Γ π« βͺ ( M β π΄)))) | ||
Theorem | madeval2 27348* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ (π΄ β On β ( M βπ΄) = {π₯ β No β£ βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯)}) | ||
Theorem | oldval 27349 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ (π΄ β On β ( O βπ΄) = βͺ ( M β π΄)) | ||
Theorem | newval 27350 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( N βπ΄) = (( M βπ΄) β ( O βπ΄)) | ||
Theorem | madef 27351 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ M :OnβΆπ« No | ||
Theorem | oldf 27352 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ O :OnβΆπ« No | ||
Theorem | newf 27353 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ N :OnβΆπ« No | ||
Theorem | old0 27354 | No surreal is older than β . (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( O ββ ) = β | ||
Theorem | madessno 27355 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( M βπ΄) β No | ||
Theorem | oldssno 27356 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( O βπ΄) β No | ||
Theorem | newssno 27357 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( N βπ΄) β No | ||
Theorem | leftval 27358* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π₯ <s π΄} | ||
Theorem | rightval 27359* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π΄ <s π₯} | ||
Theorem | leftf 27360 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ L : No βΆπ« No | ||
Theorem | rightf 27361 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ R : No βΆπ« No | ||
Theorem | elmade 27362* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ (π΄ β On β (π β ( M βπ΄) β βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π))) | ||
Theorem | elmade2 27363* | Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β On β (π β ( M βπ΄) β βπ β π« ( O βπ΄)βπ β π« ( O βπ΄)(π <<s π β§ (π |s π) = π))) | ||
Theorem | elold 27364* | Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β On β (π β ( O βπ΄) β βπ β π΄ π β ( M βπ))) | ||
Theorem | ssltleft 27365 | A surreal is greater than its left options. Theorem 0(ii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β No β ( L βπ΄) <<s {π΄}) | ||
Theorem | ssltright 27366 | A surreal is less than its right options. Theorem 0(i) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β No β {π΄} <<s ( R βπ΄)) | ||
Theorem | lltropt 27367 | The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) (Revised by Scott Fenton, 21-Feb-2025.) |
β’ ( L βπ΄) <<s ( R βπ΄) | ||
Theorem | made0 27368 | The only surreal made on day β is 0s. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( M ββ ) = { 0s } | ||
Theorem | new0 27369 | The only surreal new on day β is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ( N ββ ) = { 0s } | ||
Theorem | old1 27370 | The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( O β1o) = { 0s } | ||
Theorem | madess 27371 | If π΄ is less than or equal to ordinal π΅, then the made set of π΄ is included in the made set of π΅. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ((π΅ β On β§ π΄ β π΅) β ( M βπ΄) β ( M βπ΅)) | ||
Theorem | oldssmade 27372 | The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( O βπ΄) β ( M βπ΄) | ||
Theorem | leftssold 27373 | The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ) β ( O β( bday βπ)) | ||
Theorem | rightssold 27374 | The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ) β ( O β( bday βπ)) | ||
Theorem | leftssno 27375 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ΄) β No | ||
Theorem | rightssno 27376 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ΄) β No | ||
Theorem | madecut 27377 | Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (((π΄ β On β§ πΏ <<s π ) β§ (πΏ β ( O βπ΄) β§ π β ( O βπ΄))) β (πΏ |s π ) β ( M βπ΄)) | ||
Theorem | madeun 27378 | The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( M βπ΄) = (( O βπ΄) βͺ ( N βπ΄)) | ||
Theorem | madeoldsuc 27379 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π΄ β On β ( M βπ΄) = ( O βsuc π΄)) | ||
Theorem | oldsuc 27380 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π΄ β On β ( O βsuc π΄) = (( O βπ΄) βͺ ( N βπ΄))) | ||
Theorem | oldlim 27381 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((Lim π΄ β§ π΄ β π) β ( O βπ΄) = βͺ ( O β π΄)) | ||
Theorem | madebdayim 27382 | If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ (π β ( M βπ΄) β ( bday βπ) β π΄) | ||
Theorem | oldbdayim 27383 | If π is in the old set for π΄, then the birthday of π is less than π΄. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ (π β ( O βπ΄) β ( bday βπ) β π΄) | ||
Theorem | oldirr 27384 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ Β¬ π β ( O β( bday βπ)) | ||
Theorem | leftirr 27385 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ Β¬ π β ( L βπ) | ||
Theorem | rightirr 27386 | No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ Β¬ π β ( R βπ) | ||
Theorem | left0s 27387 | The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ( L β 0s ) = β | ||
Theorem | right0s 27388 | The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ( R β 0s ) = β | ||
Theorem | left1s 27389 | The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( L β 1s ) = { 0s } | ||
Theorem | right1s 27390 | The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( R β 1s ) = β | ||
Theorem | lrold 27391 | The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ (( L βπ΄) βͺ ( R βπ΄)) = ( O β( bday βπ΄)) | ||
Theorem | madebdaylemold 27392* | Lemma for madebday 27394. If the inductive hypothesis of madebday 27394 is satisfied, the converse of oldbdayim 27383 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((π΄ β On β§ βπ β π΄ βπ¦ β No (( bday βπ¦) β π β π¦ β ( M βπ)) β§ π β No ) β (( bday βπ) β π΄ β π β ( O βπ΄))) | ||
Theorem | madebdaylemlrcut 27393* | Lemma for madebday 27394. If the inductive hypothesis of madebday 27394 is satisfied up to the birthday of π, then the conclusion of lrcut 27397 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((βπ β ( bday βπ)βπ¦ β No (( bday βπ¦) β π β π¦ β ( M βπ)) β§ π β No ) β (( L βπ) |s ( R βπ)) = π) | ||
Theorem | madebday 27394 | A surreal is part of the set made by ordinal π΄ iff its birthday is less than or equal to π΄. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((π΄ β On β§ π β No ) β (π β ( M βπ΄) β ( bday βπ) β π΄)) | ||
Theorem | oldbday 27395 | A surreal is part of the set older than ordinal π΄ iff its birthday is less than π΄. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((π΄ β On β§ π β No ) β (π β ( O βπ΄) β ( bday βπ) β π΄)) | ||
Theorem | newbday 27396 | A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((π΄ β On β§ π β No ) β (π β ( N βπ΄) β ( bday βπ) = π΄)) | ||
Theorem | lrcut 27397 | A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ (π β No β (( L βπ) |s ( R βπ)) = π) | ||
Theorem | scutfo 27398 | The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.) |
β’ |s : <<s βontoβ No | ||
Theorem | sltn0 27399 | If π is less than π, then either ( L βπ) or ( R βπ) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.) |
β’ ((π β No β§ π β No β§ π <s π) β (( L βπ) β β β¨ ( R βπ) β β )) | ||
Theorem | lruneq 27400 | If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024.) |
β’ ((π β No β§ π β No β§ ( bday βπ) = ( bday βπ)) β (( L βπ) βͺ ( R βπ)) = (( L βπ) βͺ ( R βπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |