![]() |
Metamath
Proof Explorer Theorem List (p. 276 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sletrd 27501 | Surreal less-than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) & âĒ (ð â ðī âĪs ðĩ) & âĒ (ð â ðĩ âĪs ðķ) â âĒ (ð â ðī âĪs ðķ) | ||
Theorem | slerflex 27502 | Surreal less-than or equal is reflexive. Theorem 0(iii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ (ðī â No â ðī âĪs ðī) | ||
Theorem | sletric 27503 | Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī âĪs ðĩ âĻ ðĩ âĪs ðī)) | ||
Theorem | maxs1 27504 | A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.) |
âĒ (ðī â No â ðī âĪs if(ðī âĪs ðĩ, ðĩ, ðī)) | ||
Theorem | maxs2 27505 | A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â ðĩ âĪs if(ðī âĪs ðĩ, ðĩ, ðī)) | ||
Theorem | mins1 27506 | The minimum of two surreals is less than or equal to the first. (Contributed by Scott Fenton, 14-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â if(ðī âĪs ðĩ, ðī, ðĩ) âĪs ðī) | ||
Theorem | mins2 27507 | The minimum of two surreals is less than or equal to the second. (Contributed by Scott Fenton, 14-Feb-2025.) |
âĒ (ðĩ â No â if(ðī âĪs ðĩ, ðī, ðĩ) âĪs ðĩ) | ||
Theorem | sltled 27508 | Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðī <s ðĩ) â âĒ (ð â ðī âĪs ðĩ) | ||
Theorem | sltne 27509 | Surreal less-than implies not equal. (Contributed by Scott Fenton, 12-Mar-2025.) |
âĒ ((ðī â No â§ ðī <s ðĩ) â ðĩ â ðī) | ||
Theorem | bdayfun 27510 | The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.) |
âĒ Fun bday | ||
Theorem | bdayfn 27511 | The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.) |
âĒ bday Fn No | ||
Theorem | bdaydm 27512 | The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.) |
âĒ dom bday = No | ||
Theorem | bdayrn 27513 | The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.) |
âĒ ran bday = On | ||
Theorem | bdayelon 27514 | The value of the birthday function is always an ordinal. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by Scott Fenton, 8-Dec-2021.) |
âĒ ( bday âðī) â On | ||
Theorem | nocvxminlem 27515* | Lemma for nocvxmin 27516. Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011.) |
âĒ ((ðī â No â§ âðĨ â ðī âðĶ â ðī âð§ â No ((ðĨ <s ð§ â§ ð§ <s ðĶ) â ð§ â ðī)) â (((ð â ðī â§ ð â ðī) â§ (( bday âð) = âĐ ( bday â ðī) â§ ( bday âð) = âĐ ( bday â ðī))) â ÂŽ ð <s ð)) | ||
Theorem | nocvxmin 27516* | Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of [Alling] p. 185. (Contributed by Scott Fenton, 30-Jun-2011.) |
âĒ ((ðī â â â§ ðī â No â§ âðĨ â ðī âðĶ â ðī âð§ â No ((ðĨ <s ð§ â§ ð§ <s ðĶ) â ð§ â ðī)) â â!ðĪ â ðī ( bday âðĪ) = âĐ ( bday â ðī)) | ||
Theorem | noprc 27517 | The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.) |
âĒ ÂŽ No â V | ||
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. | ||
Syntax | csslt 27518 | Declare the syntax for surreal set less-than. |
class <<s | ||
Definition | df-sslt 27519* | Define the relation that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021.) |
âĒ <<s = {âĻð, ðâĐ âĢ (ð â No â§ ð â No â§ âðĨ â ð âðĶ â ð ðĨ <s ðĶ)} | ||
Syntax | cscut 27520 | Declare the syntax for the surreal cut operator. |
class |s | ||
Definition | df-scut 27521* | Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. Definition from [Gonshor] p. 7. (Contributed by Scott Fenton, 7-Dec-2021.) |
âĒ |s = (ð â ðŦ No , ð â ( <<s â {ð}) âĶ (âĐðĨ â {ðĶ â No âĢ (ð <<s {ðĶ} â§ {ðĶ} <<s ð)} ( bday âðĨ) = âĐ ( bday â {ðĶ â No âĢ (ð <<s {ðĶ} â§ {ðĶ} <<s ð)}))) | ||
Theorem | noeta2 27522* | A version of noeta 27482 with fewer hypotheses but a weaker upper bound (Contributed by Scott Fenton, 7-Dec-2021.) |
âĒ (((ðī â No â§ ðī â ð) â§ (ðĩ â No â§ ðĩ â ð) â§ âðĨ â ðī âðĶ â ðĩ ðĨ <s ðĶ) â âð§ â No (âðĨ â ðī ðĨ <s ð§ â§ âðĶ â ðĩ ð§ <s ðĶ â§ ( bday âð§) â suc ⊠( bday â (ðī ⊠ðĩ)))) | ||
Theorem | brsslt 27523* | Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ((ðī â V â§ ðĩ â V) â§ (ðī â No â§ ðĩ â No â§ âðĨ â ðī âðĶ â ðĩ ðĨ <s ðĶ))) | ||
Theorem | ssltex1 27524 | The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ðī â V) | ||
Theorem | ssltex2 27525 | The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ðĩ â V) | ||
Theorem | ssltss1 27526 | The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ðī â No ) | ||
Theorem | ssltss2 27527 | The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ðĩ â No ) | ||
Theorem | ssltsep 27528* | The separation property of surreal set less-than. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â âðĨ â ðī âðĶ â ðĩ ðĨ <s ðĶ) | ||
Theorem | ssltd 27529* | Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ ((ð â§ ðĨ â ðī â§ ðĶ â ðĩ) â ðĨ <s ðĶ) â âĒ (ð â ðī <<s ðĩ) | ||
Theorem | ssltsn 27530 | Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðī <s ðĩ) â âĒ (ð â {ðī} <<s {ðĩ}) | ||
Theorem | ssltsepc 27531 | Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ ((ðī <<s ðĩ â§ ð â ðī â§ ð â ðĩ) â ð <s ð) | ||
Theorem | ssltsepcd 27532 | Two elements of separated sets obey less-than. Deduction form of ssltsepc 27531. (Contributed by Scott Fenton, 25-Sep-2024.) |
âĒ (ð â ðī <<s ðĩ) & âĒ (ð â ð â ðī) & âĒ (ð â ð â ðĩ) â âĒ (ð â ð <s ð) | ||
Theorem | sssslt1 27533 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðĩ â§ ðķ â ðī) â ðķ <<s ðĩ) | ||
Theorem | sssslt2 27534 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðĩ â§ ðķ â ðĩ) â ðī <<s ðķ) | ||
Theorem | nulsslt 27535 | The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī â ðŦ No â â <<s ðī) | ||
Theorem | nulssgt 27536 | The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī â ðŦ No â ðī <<s â ) | ||
Theorem | conway 27537* | Conway's Simplicity Theorem. Given ðī preceeding ðĩ, there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from [Alling] p. 185. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â â!ðĨ â {ðĶ â No âĢ (ðī <<s {ðĶ} â§ {ðĶ} <<s ðĩ)} ( bday âðĨ) = âĐ ( bday â {ðĶ â No âĢ (ðī <<s {ðĶ} â§ {ðĶ} <<s ðĩ)})) | ||
Theorem | scutval 27538* | 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 27539 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No â§ ðī <<s {(ðī |s ðĩ)} â§ {(ðī |s ðĩ)} <<s ðĩ)) | ||
Theorem | scutcl 27540 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
âĒ (ðī <<s ðĩ â (ðī |s ðĩ) â No ) | ||
Theorem | scutcld 27541 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
âĒ (ð â ðī <<s ðĩ) â âĒ (ð â (ðī |s ðĩ) â No ) | ||
Theorem | scutbday 27542* | 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 27543* | 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 27544* | 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 27545 | Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðĩ â§ ðĩ <<s ðķ â§ ðĩ â â ) â ðī <<s ðķ) | ||
Theorem | ssltun1 27546 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðķ â§ ðĩ <<s ðķ) â (ðī ⊠ðĩ) <<s ðķ) | ||
Theorem | ssltun2 27547 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðĩ â§ ðī <<s ðķ) â ðī <<s (ðĩ ⊠ðķ)) | ||
Theorem | scutun12 27548 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
âĒ ((ðī <<s ðĩ â§ ðķ <<s {(ðī |s ðĩ)} â§ {(ðī |s ðĩ)} <<s ð·) â ((ðī ⊠ðķ) |s (ðĩ ⊠ð·)) = (ðī |s ðĩ)) | ||
Theorem | dmscut 27549 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
âĒ dom |s = <<s | ||
Theorem | scutf 27550 | Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
âĒ |s : <<s âķ No | ||
Theorem | etasslt 27551* | A restatement of noeta 27482 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.) |
âĒ ((ðī <<s ðĩ â§ ð â On â§ ( bday â (ðī ⊠ðĩ)) â ð) â âðĨ â No (ðī <<s {ðĨ} â§ {ðĨ} <<s ðĩ â§ ( bday âðĨ) â ð)) | ||
Theorem | etasslt2 27552* | A version of etasslt 27551 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.) |
âĒ (ðī <<s ðĩ â âðĨ â No (ðī <<s {ðĨ} â§ {ðĨ} <<s ðĩ â§ ( bday âðĨ) â suc ⊠( bday â (ðī ⊠ðĩ)))) | ||
Theorem | scutbdaybnd 27553 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.) |
âĒ ((ðī <<s ðĩ â§ ð â On â§ ( bday â (ðī ⊠ðĩ)) â ð) â ( bday â(ðī |s ðĩ)) â ð) | ||
Theorem | scutbdaybnd2 27554 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
âĒ (ðī <<s ðĩ â ( bday â(ðī |s ðĩ)) â suc ⊠( bday â (ðī ⊠ðĩ))) | ||
Theorem | scutbdaybnd2lim 27555 | 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 27556 | 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 27557* | 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 27558* | 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 27559 | If ðī preceeds ðĩ, then ðī and ðĩ are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.) |
âĒ (ðī <<s ðĩ â (ðī âĐ ðĩ) = â ) | ||
Syntax | c0s 27560 | Declare the class syntax for surreal zero. |
class 0s | ||
Syntax | c1s 27561 | Declare the class syntax for surreal one. |
class 1s | ||
Definition | df-0s 27562 | 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 27563 | 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 27564 | Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ 0s â No | ||
Theorem | 1sno 27565 | Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ 1s â No | ||
Theorem | bday0s 27566 | Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ ( bday â 0s ) = â | ||
Theorem | 0slt1s 27567 | Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ 0s <s 1s | ||
Theorem | bday0b 27568 | The only surreal with birthday â is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
âĒ (ð â No â (( bday âð) = â â ð = 0s )) | ||
Theorem | bday1s 27569 | The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.) |
âĒ ( bday â 1s ) = 1o | ||
Theorem | cuteq0 27570 | Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ð â ðī <<s { 0s }) & âĒ (ð â { 0s } <<s ðĩ) â âĒ (ð â (ðī |s ðĩ) = 0s ) | ||
Theorem | cuteq1 27571 | Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.) |
âĒ (ð â 0s â ðī) & âĒ (ð â ðī <<s { 1s }) & âĒ (ð â { 1s } <<s ðĩ) â âĒ (ð â (ðī |s ðĩ) = 1s ) | ||
Theorem | sgt0ne0 27572 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
âĒ ( 0s <s ðī â ðī â 0s ) | ||
Theorem | sgt0ne0d 27573 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
âĒ (ð â 0s <s ðī) â âĒ (ð â ðī â 0s ) | ||
Syntax | cmade 27574 | Declare the symbol for the made by function. |
class M | ||
Syntax | cold 27575 | Declare the symbol for the older than function. |
class O | ||
Syntax | cnew 27576 | Declare the symbol for the new on function. |
class N | ||
Syntax | cleft 27577 | Declare the symbol for the left option function. |
class L | ||
Syntax | cright 27578 | Declare the symbol for the right option function. |
class R | ||
Definition | df-made 27579 | 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 27580 | 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 27581 | 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 27582* | 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 27583* | 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 27584 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
âĒ (ðī â On â ( M âðī) = ( |s â (ðŦ ⊠( M â ðī) à ðŦ ⊠( M â ðī)))) | ||
Theorem | madeval2 27585* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
âĒ (ðī â On â ( M âðī) = {ðĨ â No âĢ âð â ðŦ ⊠( M â ðī)âð â ðŦ ⊠( M â ðī)(ð <<s ð â§ (ð |s ð) = ðĨ)}) | ||
Theorem | oldval 27586 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ (ðī â On â ( O âðī) = ⊠( M â ðī)) | ||
Theorem | newval 27587 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( N âðī) = (( M âðī) â ( O âðī)) | ||
Theorem | madef 27588 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ M :OnâķðŦ No | ||
Theorem | oldf 27589 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ O :OnâķðŦ No | ||
Theorem | newf 27590 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ N :OnâķðŦ No | ||
Theorem | old0 27591 | No surreal is older than â . (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ ( O ââ ) = â | ||
Theorem | madessno 27592 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( M âðī) â No | ||
Theorem | oldssno 27593 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( O âðī) â No | ||
Theorem | newssno 27594 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( N âðī) â No | ||
Theorem | leftval 27595* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( L âðī) = {ðĨ â ( O â( bday âðī)) âĢ ðĨ <s ðī} | ||
Theorem | rightval 27596* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
âĒ ( R âðī) = {ðĨ â ( O â( bday âðī)) âĢ ðī <s ðĨ} | ||
Theorem | leftf 27597 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ L : No âķðŦ No | ||
Theorem | rightf 27598 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ R : No âķðŦ No | ||
Theorem | elmade 27599* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
âĒ (ðī â On â (ð â ( M âðī) â âð â ðŦ ⊠( M â ðī)âð â ðŦ ⊠( M â ðī)(ð <<s ð â§ (ð |s ð) = ð))) | ||
Theorem | elmade2 27600* | Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024.) |
âĒ (ðī â On â (ð â ( M âðī) â âð â ðŦ ( O âðī)âð â ðŦ ( O âðī)(ð <<s ð â§ (ð |s ð) = ð))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |