Home | Metamath
Proof Explorer Theorem List (p. 270 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | padicabvf 26901* | The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) β β’ π½:ββΆπ΄ | ||
Theorem | padicabvcxp 26902* | All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) β β’ ((π β β β§ π β β+) β (π¦ β β β¦ (((π½βπ)βπ¦)βππ )) β π΄) | ||
Theorem | ostth1 26903* | - Lemma for ostth 26909: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If πΉ is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 20211 of the absolute value, πΉ is equal to 1 on all the integers, and ostthlem1 26897 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β βπ β β Β¬ 1 < (πΉβπ)) & β’ (π β βπ β β Β¬ (πΉβπ) < 1) β β’ (π β πΉ = πΎ) | ||
Theorem | ostth2lem2 26904* | Lemma for ostth2 26907. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β π β (β€β₯β2)) & β’ (π β 1 < (πΉβπ)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ (π β π β (β€β₯β2)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) β β’ ((π β§ π β β0 β§ π β (0...((πβπ) β 1))) β (πΉβπ) β€ ((π Β· π) Β· (πβπ))) | ||
Theorem | ostth2lem3 26905* | Lemma for ostth2 26907. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β π β (β€β₯β2)) & β’ (π β 1 < (πΉβπ)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ (π β π β (β€β₯β2)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) & β’ π = ((logβπ) / (logβπ)) β β’ ((π β§ π β β) β (((πΉβπ) / (πβππ))βπ) β€ (π Β· ((π Β· π) Β· (π + 1)))) | ||
Theorem | ostth2lem4 26906* | Lemma for ostth2 26907. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β π β (β€β₯β2)) & β’ (π β 1 < (πΉβπ)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ (π β π β (β€β₯β2)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) & β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) & β’ π = ((logβπ) / (logβπ)) β β’ (π β (1 < (πΉβπ) β§ π β€ π)) | ||
Theorem | ostth2 26907* | - Lemma for ostth 26909: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β π β (β€β₯β2)) & β’ (π β 1 < (πΉβπ)) & β’ π = ((logβ(πΉβπ)) / (logβπ)) β β’ (π β βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ))) | ||
Theorem | ostth3 26908* | - Lemma for ostth 26909: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) & β’ (π β πΉ β π΄) & β’ (π β βπ β β Β¬ 1 < (πΉβπ)) & β’ (π β π β β) & β’ (π β (πΉβπ) < 1) & β’ π = -((logβ(πΉβπ)) / (logβπ)) & β’ π = if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) β β’ (π β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) | ||
Theorem | ostth 26909* | Ostrowski's theorem, which classifies all absolute values on β. Any such absolute value must either be the trivial absolute value πΎ, a constant exponent 0 < π β€ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) & β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) β β’ (πΉ β π΄ β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+ βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) | ||
Syntax | csur 26910 | Declare the class of all surreal numbers (see df-no 26913). |
class No | ||
Syntax | cslt 26911 | Declare the less-than relation over surreal numbers (see df-slt 26914). |
class <s | ||
Syntax | cbday 26912 | Declare the birthday function for surreal numbers (see df-bday 26915). |
class bday | ||
Definition | df-no 26913* |
Define the class of surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Gonshor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1o and
2o, analagous to Gonshor's
( β ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
β’ No = {π β£ βπ β On π:πβΆ{1o, 2o}} | ||
Definition | df-slt 26914* | Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.) |
β’ <s = {β¨π, πβ© β£ ((π β No β§ π β No ) β§ βπ₯ β On (βπ¦ β π₯ (πβπ¦) = (πβπ¦) β§ (πβπ₯){β¨1o, β β©, β¨1o, 2oβ©, β¨β , 2oβ©} (πβπ₯)))} | ||
Definition | df-bday 26915 | Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.) |
β’ bday = (π₯ β No β¦ dom π₯) | ||
Theorem | elno 26916* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
β’ (π΄ β No β βπ₯ β On π΄:π₯βΆ{1o, 2o}) | ||
Theorem | sltval 26917* | The value of the surreal less-than relation. (Contributed by Scott Fenton, 14-Jun-2011.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ <s π΅ β βπ₯ β On (βπ¦ β π₯ (π΄βπ¦) = (π΅βπ¦) β§ (π΄βπ₯){β¨1o, β β©, β¨1o, 2oβ©, β¨β , 2oβ©} (π΅βπ₯)))) | ||
Theorem | bdayval 26918 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
β’ (π΄ β No β ( bday βπ΄) = dom π΄) | ||
Theorem | nofun 26919 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β Fun π΄) | ||
Theorem | nodmon 26920 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β dom π΄ β On) | ||
Theorem | norn 26921 | The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β ran π΄ β {1o, 2o}) | ||
Theorem | nofnbday 26922 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β π΄ Fn ( bday βπ΄)) | ||
Theorem | nodmord 26923 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β Ord dom π΄) | ||
Theorem | elno2 26924 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
β’ (π΄ β No β (Fun π΄ β§ dom π΄ β On β§ ran π΄ β {1o, 2o})) | ||
Theorem | elno3 26925 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ (π΄ β No β (π΄:dom π΄βΆ{1o, 2o} β§ dom π΄ β On)) | ||
Theorem | sltval2 26926* | Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ <s π΅ β (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β β©, β¨1o, 2oβ©, β¨β , 2oβ©} (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}))) | ||
Theorem | nofv 26927 | The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.) |
β’ (π΄ β No β ((π΄βπ) = β β¨ (π΄βπ) = 1o β¨ (π΄βπ) = 2o)) | ||
Theorem | nosgnn0 26928 | β is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ Β¬ β β {1o, 2o} | ||
Theorem | nosgnn0i 26929 | If π is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
β’ π β {1o, 2o} β β’ β β π | ||
Theorem | noreson 26930 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
β’ ((π΄ β No β§ π΅ β On) β (π΄ βΎ π΅) β No ) | ||
Theorem | sltintdifex 26931* | If π΄ <s π΅, then the intersection of all the ordinals that have differing signs in π΄ and π΅ exists. (Contributed by Scott Fenton, 22-Feb-2012.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ <s π΅ β β© {π β On β£ (π΄βπ) β (π΅βπ)} β V)) | ||
Theorem | sltres 26932 | If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.) |
β’ ((π΄ β No β§ π΅ β No β§ π β On) β ((π΄ βΎ π) <s (π΅ βΎ π) β π΄ <s π΅)) | ||
Theorem | noxp1o 26933 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
β’ (π΄ β On β (π΄ Γ {1o}) β No ) | ||
Theorem | noseponlem 26934* | Lemma for nosepon 26935. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
β’ ((π΄ β No β§ π΅ β No β§ dom π΄ β dom π΅) β Β¬ βπ₯ β On (π΄βπ₯) = (π΅βπ₯)) | ||
Theorem | nosepon 26935* | Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ β π΅) β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)} β On) | ||
Theorem | noextend 26936 | Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
β’ π β {1o, 2o} β β’ (π΄ β No β (π΄ βͺ {β¨dom π΄, πβ©}) β No ) | ||
Theorem | noextendseq 26937 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
β’ π β {1o, 2o} β β’ ((π΄ β No β§ π΅ β On) β (π΄ βͺ ((π΅ β dom π΄) Γ {π})) β No ) | ||
Theorem | noextenddif 26938* | Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021.) |
β’ π β {1o, 2o} β β’ (π΄ β No β β© {π₯ β On β£ (π΄βπ₯) β ((π΄ βͺ {β¨dom π΄, πβ©})βπ₯)} = dom π΄) | ||
Theorem | noextendlt 26939 | Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
β’ (π΄ β No β (π΄ βͺ {β¨dom π΄, 1oβ©}) <s π΄) | ||
Theorem | noextendgt 26940 | Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
β’ (π΄ β No β π΄ <s (π΄ βͺ {β¨dom π΄, 2oβ©})) | ||
Theorem | nolesgn2o 26941 | Given π΄ less-than or equal to π΅, equal to π΅ up to π, and π΄(π) = 2o, then π΅(π) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ (π΄βπ) = 2o) β§ Β¬ π΅ <s π΄) β (π΅βπ) = 2o) | ||
Theorem | nolesgn2ores 26942 | Given π΄ less-than or equal to π΅, equal to π΅ up to π, and π΄(π) = 2o, then (π΄ βΎ suc π) = (π΅ βΎ suc π). (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ (π΄βπ) = 2o) β§ Β¬ π΅ <s π΄) β (π΄ βΎ suc π) = (π΅ βΎ suc π)) | ||
Theorem | nogesgn1o 26943 | Given π΄ greater than or equal to π΅, equal to π΅ up to π, and π΄(π) = 1o, then π΅(π) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ (π΄βπ) = 1o) β§ Β¬ π΄ <s π΅) β (π΅βπ) = 1o) | ||
Theorem | nogesgn1ores 26944 | Given π΄ greater than or equal to π΅, equal to π΅ up to π, and π΄(π) = 1o, then (π΄ βΎ suc π) = (π΅ βΎ suc π). (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ (π΄βπ) = 1o) β§ Β¬ π΄ <s π΅) β (π΄ βΎ suc π) = (π΅ βΎ suc π)) | ||
Theorem | sltsolem1 26945 | Lemma for sltso 26946. The "sign expansion" binary relation totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) |
β’ {β¨1o, β β©, β¨1o, 2oβ©, β¨β , 2oβ©} Or ({1o, 2o} βͺ {β }) | ||
Theorem | sltso 26946 | Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
β’ <s Or No | ||
Theorem | bdayfo 26947 | 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.) |
β’ bday : No βontoβOn | ||
Theorem | fvnobday 26948 | The value of a surreal at its birthday is β . (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) |
β’ (π΄ β No β (π΄β( bday βπ΄)) = β ) | ||
Theorem | nosepnelem 26949* | Lemma for nosepne 26950. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ <s π΅) β (π΄ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)}) β (π΅ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)})) | ||
Theorem | nosepne 26950* | The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ β π΅) β (π΄ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)}) β (π΅ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)})) | ||
Theorem | nosep1o 26951* | If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π΄ β π΅) β§ (π΄ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)}) = 1o) β π΄ <s π΅) | ||
Theorem | nosep2o 26952* | If the value of a surreal at a separator is 2o then the surreal is greater. (Contributed by Scott Fenton, 7-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π΄ β π΅) β§ (π΄ββ© {π₯ β On β£ (π΅βπ₯) β (π΄βπ₯)}) = 2o) β π΅ <s π΄) | ||
Theorem | nosepdmlem 26953* | Lemma for nosepdm 26954. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ <s π΅) β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)} β (dom π΄ βͺ dom π΅)) | ||
Theorem | nosepdm 26954* | The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ β π΅) β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)} β (dom π΄ βͺ dom π΅)) | ||
Theorem | nosepeq 26955* | The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π΄ β π΅) β§ π β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)}) β (π΄βπ) = (π΅βπ)) | ||
Theorem | nosepssdm 26956* | 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.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ β π΅) β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)} β dom π΄) | ||
Theorem | nodenselem4 26957* | Lemma for nodense 26962. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ π΄ <s π΅) β β© {π β On β£ (π΄βπ) β (π΅βπ)} β On) | ||
Theorem | nodenselem5 26958* | Lemma for nodense 26962. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 26957 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β© {π β On β£ (π΄βπ) β (π΅βπ)} β ( bday βπ΄)) | ||
Theorem | nodenselem6 26959* | The restriction of a surreal to the abstraction from nodenselem4 26957 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β No ) | ||
Theorem | nodenselem7 26960* | Lemma for nodense 26962. π΄ and π΅ are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (πΆ β β© {π β On β£ (π΄βπ) β (π΅βπ)} β (π΄βπΆ) = (π΅βπΆ))) | ||
Theorem | nodenselem8 26961* | Lemma for nodense 26962. Give a condition for surreal less-than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011.) |
β’ ((π΄ β No β§ π΅ β No β§ ( bday βπ΄) = ( bday βπ΅)) β (π΄ <s π΅ β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o))) | ||
Theorem | nodense 26962* | 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.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β βπ₯ β No (( bday βπ₯) β ( bday βπ΄) β§ π΄ <s π₯ β§ π₯ <s π΅)) | ||
The theorems in this section are derived from "A clean way to separate sets of surreals" by Paolo Lipparini, https://doi.org/10.48550/arXiv.1712.03500. | ||
Theorem | bdayimaon 26963 | Lemma for full-eta properties. The successor of the union of the image of the birthday function under a set is an ordinal. (Contributed by Scott Fenton, 20-Aug-2011.) |
β’ (π΄ β π β suc βͺ ( bday β π΄) β On) | ||
Theorem | nolt02olem 26964 | Lemma for nolt02o 26965. If π΄(π) is undefined with π΄ surreal and π ordinal, then dom π΄ β π. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ ((π΄ β No β§ π β On β§ (π΄βπ) = β ) β dom π΄ β π) | ||
Theorem | nolt02o 26965 | Given π΄ less-than π΅, equal to π΅ up to π, and undefined at π, then π΅(π) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ π΄ <s π΅) β§ (π΄βπ) = β ) β (π΅βπ) = 2o) | ||
Theorem | nogt01o 26966 | Given π΄ greater than π΅, equal to π΅ up to π, and π΅(π) undefined, then π΄(π) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ (((π΄ β No β§ π΅ β No β§ π β On) β§ ((π΄ βΎ π) = (π΅ βΎ π) β§ π΄ <s π΅) β§ (π΅βπ) = β ) β (π΄βπ) = 1o) | ||
Theorem | noresle 26967* | Restriction law for surreals. Lemma 2.1.4 of [Lipparini] p. 3. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ (((π β No β§ π β No ) β§ (dom π β π΄ β§ dom π β π΄ β§ βπ β π΄ Β¬ (π βΎ suc π) <s (π βΎ suc π))) β Β¬ π <s π) | ||
Theorem | nomaxmo 26968* | A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ (π β No β β*π₯ β π βπ¦ β π Β¬ π₯ <s π¦) | ||
Theorem | nominmo 26969* | A class of surreals has at most one minimum. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π β No β β*π₯ β π βπ¦ β π Β¬ π¦ <s π₯) | ||
Theorem | nosupprefixmo 26970* | In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 26-Nov-2021.) |
β’ (π΄ β No β β*π₯βπ’ β π΄ (πΊ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc πΊ) = (π£ βΎ suc πΊ)) β§ (π’βπΊ) = π₯)) | ||
Theorem | noinfprefixmo 26971* | In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π΄ β No β β*π₯βπ’ β π΄ (πΊ β dom π’ β§ βπ£ β π΄ (Β¬ π’ <s π£ β (π’ βΎ suc πΊ) = (π£ βΎ suc πΊ)) β§ (π’βπΊ) = π₯)) | ||
Theorem | nosupcbv 26972* | Lemma to change bound variables in a surreal supremum. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ π = if(βπ β π΄ βπ β π΄ Β¬ π <s π, ((β©π β π΄ βπ β π΄ Β¬ π <s π) βͺ {β¨dom (β©π β π΄ βπ β π΄ Β¬ π <s π), 2oβ©}), (π β {π β£ βπ β π΄ (π β dom π β§ βπ β π΄ (Β¬ π <s π β (π βΎ suc π) = (π βΎ suc π)))} β¦ (β©πβπ β π΄ (π β dom π β§ βπ β π΄ (Β¬ π <s π β (π βΎ suc π) = (π βΎ suc π)) β§ (πβπ) = π)))) | ||
Theorem | nosupno 26973* | The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound π΄ below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((π΄ β No β§ π΄ β π) β π β No ) | ||
Theorem | nosupdm 26974* | The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ (Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β dom π = {π§ β£ βπ β π΄ (π§ β dom π β§ βπ β π΄ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))}) | ||
Theorem | nosupbday 26975* | Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ (((π΄ β No β§ π΄ β V) β§ (π β On β§ ( bday β π΄) β π)) β ( bday βπ) β π) | ||
Theorem | nosupfv 26976* | The value of surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ (π β π΄ β§ πΊ β dom π β§ βπ£ β π΄ (Β¬ π£ <s π β (π βΎ suc πΊ) = (π£ βΎ suc πΊ)))) β (πβπΊ) = (πβπΊ)) | ||
Theorem | nosupres 26977* | A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ (π β π΄ β§ πΊ β dom π β§ βπ£ β π΄ (Β¬ π£ <s π β (π βΎ suc πΊ) = (π£ βΎ suc πΊ)))) β (π βΎ suc πΊ) = (π βΎ suc πΊ)) | ||
Theorem | nosupbnd1lem1 26978* | Lemma for nosupbnd1 26984. Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ π β π΄) β Β¬ π <s (π βΎ dom π)) | ||
Theorem | nosupbnd1lem2 26979* | Lemma for nosupbnd1 26984. When there is no maximum, if any member of π΄ is a prolongment of π, then so are all elements of π΄ above it. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ ((π β π΄ β§ (π βΎ dom π) = π) β§ (π β π΄ β§ Β¬ π <s π))) β (π βΎ dom π) = π) | ||
Theorem | nosupbnd1lem3 26980* | Lemma for nosupbnd1 26984. If π is a prolongment of π and in π΄, then (πβdom π) is not 2o. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ (π β π΄ β§ (π βΎ dom π) = π)) β (πβdom π) β 2o) | ||
Theorem | nosupbnd1lem4 26981* | Lemma for nosupbnd1 26984. If π is a prolongment of π and in π΄, then (πβdom π) is not undefined. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ (π β π΄ β§ (π βΎ dom π) = π)) β (πβdom π) β β ) | ||
Theorem | nosupbnd1lem5 26982* | Lemma for nosupbnd1 26984. If π is a prolongment of π and in π΄, then (πβdom π) is not 1o. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ (π β π΄ β§ (π βΎ dom π) = π)) β (πβdom π) β 1o) | ||
Theorem | nosupbnd1lem6 26983* | Lemma for nosupbnd1 26984. Establish a hard upper bound when there is no maximum. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦ β§ (π΄ β No β§ π΄ β V) β§ π β π΄) β (π βΎ dom π) <s π) | ||
Theorem | nosupbnd1 26984* | Bounding law from below for the surreal supremum. Proposition 4.2 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((π΄ β No β§ π΄ β V β§ π β π΄) β (π βΎ dom π) <s π) | ||
Theorem | nosupbnd2lem1 26985* | Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ (((π β π΄ β§ βπ¦ β π΄ Β¬ π <s π¦) β§ (π΄ β No β§ π΄ β V β§ π β No ) β§ βπ β π΄ π <s π) β Β¬ (π βΎ suc dom π) <s (π βͺ {β¨dom π, 2oβ©})) | ||
Theorem | nosupbnd2 26986* | Bounding law from above for the surreal supremum. Proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((π΄ β No β§ π΄ β V β§ π β No ) β (βπ β π΄ π <s π β Β¬ (π βΎ dom π) <s π)) | ||
Theorem | noinfcbv 26987* | Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ π = if(βπ β π΅ βπ β π΅ Β¬ π <s π, ((β©π β π΅ βπ β π΅ Β¬ π <s π) βͺ {β¨dom (β©π β π΅ βπ β π΅ Β¬ π <s π), 1oβ©}), (π β {π β£ βπ β π΅ (π β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π) = (π βΎ suc π)))} β¦ (β©πβπ β π΅ (π β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π) = (π βΎ suc π)) β§ (πβπ) = π)))) | ||
Theorem | noinfno 26988* | The next several theorems deal with a surreal "infimum". This surreal will ultimately be shown to bound π΅ above and bound the restriction of any surreal below. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((π΅ β No β§ π΅ β π) β π β No ) | ||
Theorem | noinfdm 26989* | Next, we calculate the domain of π. This is mostly to change bound variables. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ (Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β dom π = {π§ β£ βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))}) | ||
Theorem | noinfbday 26990* | Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ (((π΅ β No β§ π΅ β π) β§ (π β On β§ ( bday β π΅) β π)) β ( bday βπ) β π) | ||
Theorem | noinffv 26991* | The value of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ (π β π΅ β§ πΊ β dom π β§ βπ£ β π΅ (Β¬ π <s π£ β (π βΎ suc πΊ) = (π£ βΎ suc πΊ)))) β (πβπΊ) = (πβπΊ)) | ||
Theorem | noinfres 26992* | The restriction of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ (π β π΅ β§ πΊ β dom π β§ βπ£ β π΅ (Β¬ π <s π£ β (π βΎ suc πΊ) = (π£ βΎ suc πΊ)))) β (π βΎ suc πΊ) = (π βΎ suc πΊ)) | ||
Theorem | noinfbnd1lem1 26993* | Lemma for noinfbnd1 26999. Establish a soft lower bound. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ π β π΅) β Β¬ (π βΎ dom π) <s π) | ||
Theorem | noinfbnd1lem2 26994* | Lemma for noinfbnd1 26999. When there is no minimum, if any member of π΅ is a prolongment of π, then so are all elements below it. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ ((π β π΅ β§ (π βΎ dom π) = π) β§ (π β π΅ β§ Β¬ π <s π))) β (π βΎ dom π) = π) | ||
Theorem | noinfbnd1lem3 26995* | Lemma for noinfbnd1 26999. If π is a prolongment of π and in π΅, then (πβdom π) is not 1o. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ (π β π΅ β§ (π βΎ dom π) = π)) β (πβdom π) β 1o) | ||
Theorem | noinfbnd1lem4 26996* | Lemma for noinfbnd1 26999. If π is a prolongment of π and in π΅, then (πβdom π) is not undefined. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ (π β π΅ β§ (π βΎ dom π) = π)) β (πβdom π) β β ) | ||
Theorem | noinfbnd1lem5 26997* | Lemma for noinfbnd1 26999. If π is a prolongment of π and in π΅, then (πβdom π) is not 2o. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ (π β π΅ β§ (π βΎ dom π) = π)) β (πβdom π) β 2o) | ||
Theorem | noinfbnd1lem6 26998* | Lemma for noinfbnd1 26999. Establish a hard lower bound when there is no minimum. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((Β¬ βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ (π΅ β No β§ π΅ β π) β§ π β π΅) β π <s (π βΎ dom π)) | ||
Theorem | noinfbnd1 26999* | Bounding law from above for the surreal infimum. Analagous to proposition 4.2 of [Lipparini] p. 6. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) β β’ ((π΅ β No β§ π΅ β π β§ π β π΅) β π <s (π βΎ dom π)) | ||
Theorem | noinfbnd2lem1 27000* | Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024.) |
β’ (((π β π΅ β§ βπ¦ β π΅ Β¬ π¦ <s π) β§ (π΅ β No β§ π΅ β π β§ π β No ) β§ βπ β π΅ π <s π) β Β¬ (π βͺ {β¨dom π, 1oβ©}) <s (π βΎ suc dom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |