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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | padicabv 26901* | The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ π = (βfld βΎs β) & β’ π΄ = (AbsValβπ) & β’ πΉ = (π₯ β β β¦ if(π₯ = 0, 0, (πβ(π pCnt π₯)))) β β’ ((π β β β§ π β (0(,)1)) β πΉ β π΄) | ||
Theorem | padicabvf 26902* | 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 26903* | 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 26904* | - Lemma for ostth 26910: 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 20212 of the absolute value, πΉ is equal to 1 on all the integers, and ostthlem1 26898 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 26905* | Lemma for ostth2 26908. (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 26906* | Lemma for ostth2 26908. (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 26907* | Lemma for ostth2 26908. (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 26908* | - Lemma for ostth 26910: 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 26909* | - Lemma for ostth 26910: 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 26910* | 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 26911 | Declare the class of all surreal numbers (see df-no 26914). |
class No | ||
Syntax | cslt 26912 | Declare the less-than relation over surreal numbers (see df-slt 26915). |
class <s | ||
Syntax | cbday 26913 | Declare the birthday function for surreal numbers (see df-bday 26916). |
class bday | ||
Definition | df-no 26914* |
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 26915* | 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 26916 | 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 26917* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
β’ (π΄ β No β βπ₯ β On π΄:π₯βΆ{1o, 2o}) | ||
Theorem | sltval 26918* | 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 26919 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
β’ (π΄ β No β ( bday βπ΄) = dom π΄) | ||
Theorem | nofun 26920 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β Fun π΄) | ||
Theorem | nodmon 26921 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β dom π΄ β On) | ||
Theorem | norn 26922 | 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 26923 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β π΄ Fn ( bday βπ΄)) | ||
Theorem | nodmord 26924 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (π΄ β No β Ord dom π΄) | ||
Theorem | elno2 26925 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
β’ (π΄ β No β (Fun π΄ β§ dom π΄ β On β§ ran π΄ β {1o, 2o})) | ||
Theorem | elno3 26926 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ (π΄ β No β (π΄:dom π΄βΆ{1o, 2o} β§ dom π΄ β On)) | ||
Theorem | sltval2 26927* | 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 26928 | 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 26929 | β is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ Β¬ β β {1o, 2o} | ||
Theorem | nosgnn0i 26930 | If π is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
β’ π β {1o, 2o} β β’ β β π | ||
Theorem | noreson 26931 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
β’ ((π΄ β No β§ π΅ β On) β (π΄ βΎ π΅) β No ) | ||
Theorem | sltintdifex 26932* | 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 26933 | 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 26934 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
β’ (π΄ β On β (π΄ Γ {1o}) β No ) | ||
Theorem | noseponlem 26935* | Lemma for nosepon 26936. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
β’ ((π΄ β No β§ π΅ β No β§ dom π΄ β dom π΅) β Β¬ βπ₯ β On (π΄βπ₯) = (π΅βπ₯)) | ||
Theorem | nosepon 26936* | 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 26937 | 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 26938 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
β’ π β {1o, 2o} β β’ ((π΄ β No β§ π΅ β On) β (π΄ βͺ ((π΅ β dom π΄) Γ {π})) β No ) | ||
Theorem | noextenddif 26939* | 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 26940 | 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 26941 | 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 26942 | 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 26943 | 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 26944 | 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 26945 | 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 26946 | Lemma for sltso 26947. 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 26947 | Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
β’ <s Or No | ||
Theorem | bdayfo 26948 | 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 26949 | 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 26950* | Lemma for nosepne 26951. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ <s π΅) β (π΄ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)}) β (π΅ββ© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)})) | ||
Theorem | nosepne 26951* | 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 26952* | 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 26953* | 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 26954* | Lemma for nosepdm 26955. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ ((π΄ β No β§ π΅ β No β§ π΄ <s π΅) β β© {π₯ β On β£ (π΄βπ₯) β (π΅βπ₯)} β (dom π΄ βͺ dom π΅)) | ||
Theorem | nosepdm 26955* | 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 26956* | 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 26957* | 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 26958* | Lemma for nodense 26963. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ π΄ <s π΅) β β© {π β On β£ (π΄βπ) β (π΅βπ)} β On) | ||
Theorem | nodenselem5 26959* | Lemma for nodense 26963. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 26958 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β© {π β On β£ (π΄βπ) β (π΅βπ)} β ( bday βπ΄)) | ||
Theorem | nodenselem6 26960* | The restriction of a surreal to the abstraction from nodenselem4 26958 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β No ) | ||
Theorem | nodenselem7 26961* | Lemma for nodense 26963. π΄ and π΅ are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) |
β’ (((π΄ β No β§ π΅ β No ) β§ (( bday βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (πΆ β β© {π β On β£ (π΄βπ) β (π΅βπ)} β (π΄βπΆ) = (π΅βπΆ))) | ||
Theorem | nodenselem8 26962* | Lemma for nodense 26963. 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 26963* | 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 26964 | 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 26965 | Lemma for nolt02o 26966. If π΄(π) is undefined with π΄ surreal and π ordinal, then dom π΄ β π. (Contributed by Scott Fenton, 6-Dec-2021.) |
β’ ((π΄ β No β§ π β On β§ (π΄βπ) = β ) β dom π΄ β π) | ||
Theorem | nolt02o 26966 | 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 26967 | 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 26968* | 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 26969* | A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.) |
β’ (π β No β β*π₯ β π βπ¦ β π Β¬ π₯ <s π¦) | ||
Theorem | nominmo 26970* | A class of surreals has at most one minimum. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π β No β β*π₯ β π βπ¦ β π Β¬ π¦ <s π₯) | ||
Theorem | nosupprefixmo 26971* | 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 26972* | 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 26973* | 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 26974* | 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 26975* | 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 26976* | 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 26977* | 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 26978* | 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 26979* | Lemma for nosupbnd1 26985. 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 26980* | Lemma for nosupbnd1 26985. 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 26981* | Lemma for nosupbnd1 26985. 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 26982* | Lemma for nosupbnd1 26985. 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 26983* | Lemma for nosupbnd1 26985. 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 26984* | Lemma for nosupbnd1 26985. 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 26985* | 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 26986* | 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 26987* | 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 26988* | 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 26989* | 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 26990* | 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 26991* | 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 26992* | 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 26993* | 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 26994* | Lemma for noinfbnd1 27000. 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 26995* | Lemma for noinfbnd1 27000. 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 26996* | Lemma for noinfbnd1 27000. 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 26997* | Lemma for noinfbnd1 27000. 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 26998* | Lemma for noinfbnd1 27000. 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 26999* | Lemma for noinfbnd1 27000. 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 27000* | 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 π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |