![]() |
Metamath
Proof Explorer Theorem List (p. 283 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | seqsp1 28201 | The value of the surreal sequence builder at a successor. (Contributed by Scott Fenton, 19-Apr-2025.) |
β’ (π β π β No ) & β’ (π β π = (rec((π₯ β V β¦ (π₯ +s 1s )), π) β Ο)) & β’ (π β π β π) β β’ (π β (seqsπ( + , πΉ)β(π +s 1s )) = ((seqsπ( + , πΉ)βπ) + (πΉβ(π +s 1s )))) | ||
Syntax | cnn0s 28202 | Declare the syntax for surreal non-negative integers. |
class β0s | ||
Syntax | cnns 28203 | Declare the syntax for surreal positive integers. |
class βs | ||
Definition | df-n0s 28204 | Define the set of non-negative surreal integers. This set behaves similarly to Ο and β0, but it is a set of surreal numbers. Like those two sets, it satisfies the Peano axioms and is closed under (surreal) addition and multiplication. Compare df-nn 12238. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s = (rec((π₯ β V β¦ (π₯ +s 1s )), 0s ) β Ο) | ||
Definition | df-nns 28205 | Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs = (β0s β { 0s }) | ||
Theorem | n0sex 28206 | The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s β V | ||
Theorem | nnsex 28207 | The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β V | ||
Theorem | peano5n0s 28208* | Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (( 0s β π΄ β§ βπ₯ β π΄ (π₯ +s 1s ) β π΄) β β0s β π΄) | ||
Theorem | n0ssno 28209 | The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s β No | ||
Theorem | nnssn0s 28210 | The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β β0s | ||
Theorem | nnssno 28211 | The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β No | ||
Theorem | n0sno 28212 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β β0s β π΄ β No ) | ||
Theorem | nnsno 28213 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β π΄ β No ) | ||
Theorem | n0snod 28214 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π β π΄ β β0s) β β’ (π β π΄ β No ) | ||
Theorem | nnsnod 28215 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π β π΄ β βs) β β’ (π β π΄ β No ) | ||
Theorem | nnn0s 28216 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β βs β π΄ β β0s) | ||
Theorem | nnn0sd 28217 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π β π΄ β βs) β β’ (π β π΄ β β0s) | ||
Theorem | 0n0s 28218 | Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ 0s β β0s | ||
Theorem | peano2n0s 28219 | Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (π΄ β β0s β (π΄ +s 1s ) β β0s) | ||
Theorem | dfn0s2 28220* | Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s = β© {π₯ β£ ( 0s β π₯ β§ βπ¦ β π₯ (π¦ +s 1s ) β π₯)} | ||
Theorem | n0sind 28221* | Principle of Mathematical Induction (inference schema). Compare nnind 12255 and finds 7898. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (π₯ = 0s β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ +s 1s ) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β β0s β (π β π)) β β’ (π΄ β β0s β π) | ||
Theorem | n0scut 28222 | A cut form for surreal naturals. (Contributed by Scott Fenton, 2-Apr-2025.) |
β’ (π΄ β β0s β π΄ = ({(π΄ -s 1s )} |s β )) | ||
Theorem | n0ons 28223 | A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.) |
β’ (π΄ β β0s β π΄ β Ons) | ||
Theorem | nnne0s 28224 | A surreal positive integer is non-zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β π΄ β 0s ) | ||
Theorem | n0sge0 28225 | A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β β0s β 0s β€s π΄) | ||
Theorem | nnsgt0 28226 | A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β 0s <s π΄) | ||
Theorem | elnns 28227 | Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β (π΄ β β0s β§ π΄ β 0s )) | ||
Theorem | elnns2 28228 | A positive surreal integer is a non-negative surreal integer greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β (π΄ β β0s β§ 0s <s π΄)) | ||
Theorem | n0addscl 28229 | The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ ((π΄ β β0s β§ π΅ β β0s) β (π΄ +s π΅) β β0s) | ||
Theorem | n0mulscl 28230 | The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ ((π΄ β β0s β§ π΅ β β0s) β (π΄ Β·s π΅) β β0s) | ||
Theorem | nnaddscl 28231 | The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ ((π΄ β βs β§ π΅ β βs) β (π΄ +s π΅) β βs) | ||
Theorem | nnmulscl 28232 | The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ ((π΄ β βs β§ π΅ β βs) β (π΄ Β·s π΅) β βs) | ||
Theorem | 1n0s 28233 | Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ 1s β β0s | ||
Theorem | 1nns 28234 | Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ 1s β βs | ||
Theorem | peano2nns 28235 | Peano postulate for positive surreal integers. One plus a positive surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β (π΄ +s 1s ) β βs) | ||
Theorem | n0sbday 28236 | A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.) |
β’ (π΄ β β0s β ( bday βπ΄) β Ο) | ||
Theorem | n0ssold 28237 | The non-negative surreal integers are a subset of the old set of Ο. (Contributed by Scott Fenton, 18-Apr-2025.) |
β’ β0s β ( O βΟ) | ||
Theorem | nnsrecgt0d 28238 | The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.) |
β’ (π β π΄ β βs) β β’ (π β 0s <s ( 1s /su π΄)) | ||
Theorem | seqn0sfn 28239 | The surreal sequence builder is a function over β0s when started from zero. (Contributed by Scott Fenton, 19-Apr-2025.) |
β’ (π β seqs 0s ( + , πΉ) Fn β0s) | ||
Theorem | eln0s 28240 | A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β0s β (π΄ β βs β¨ π΄ = 0s )) | ||
Theorem | n0s0m1 28241 | Every non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β0s β (π΄ = 0s β¨ (π΄ -s 1s ) β β0s)) | ||
Theorem | n0subs 28242 | Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.) |
β’ ((π β β0s β§ π β β0s) β (π β€s π β (π -s π) β β0s)) | ||
Theorem | n0p1nns 28243 | One plus a non-negative surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β0s β (π΄ +s 1s ) β βs) | ||
Syntax | czs 28244 | Declare the syntax for surreal integers. |
class β€s | ||
Definition | df-zs 28245 | Define the surreal integers. Compare dfz2 12602. (Contributed by Scott Fenton, 17-May-2025.) |
β’ β€s = ( -s β (βs Γ βs)) | ||
Theorem | zsex 28246 | The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.) |
β’ β€s β V | ||
Theorem | zssno 28247 | The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.) |
β’ β€s β No | ||
Theorem | zno 28248 | A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.) |
β’ (π΄ β β€s β π΄ β No ) | ||
Theorem | znod 28249 | A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.) |
β’ (π β π΄ β β€s) β β’ (π β π΄ β No ) | ||
Theorem | elzs 28250* | Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.) |
β’ (π΄ β β€s β βπ₯ β βs βπ¦ β βs π΄ = (π₯ -s π¦)) | ||
Theorem | nnzs 28251 | A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025.) |
β’ (π΄ β βs β π΄ β β€s) | ||
Theorem | nnzsd 28252 | A positive surreal integer is a surreal integer. Deduction form. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π β π΄ β βs) β β’ (π β π΄ β β€s) | ||
Theorem | 0zs 28253 | Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ 0s β β€s | ||
Theorem | n0zs 28254 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β0s β π΄ β β€s) | ||
Theorem | n0zsd 28255 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π β π΄ β β0s) β β’ (π β π΄ β β€s) | ||
Theorem | znegscl 28256 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β€s β ( -us βπ΄) β β€s) | ||
Theorem | znegscld 28257 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π β π΄ β β€s) β β’ (π β ( -us βπ΄) β β€s) | ||
Theorem | elzn0s 28258 | A surreal integer is a surreal that is a non-negative integer or whose negative is a non-negative integer. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β€s β (π΄ β No β§ (π΄ β β0s β¨ ( -us βπ΄) β β0s))) | ||
Theorem | zsbday 28259 | A surreal integer has a finite birthday. (Contributed by Scott Fenton, 26-May-2025.) |
β’ (π΄ β β€s β ( bday βπ΄) β Ο) | ||
Syntax | creno 28260 | Declare the syntax for the surreal reals. |
class βs | ||
Definition | df-reno 28261* | Define the surreal reals. These are the finite numbers without any infintesimal parts. Definition from [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ βs = {π₯ β No β£ (βπ β βs (( -us βπ) <s π₯ β§ π₯ <s π) β§ π₯ = ({π¦ β£ βπ β βs π¦ = (π₯ -s ( 1s /su π))} |s {π¦ β£ βπ β βs π¦ = (π₯ +s ( 1s /su π))}))} | ||
Theorem | elreno 28262* | Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β (π΄ β No β§ (βπ β βs (( -us βπ) <s π΄ β§ π΄ <s π) β§ π΄ = ({π₯ β£ βπ β βs π₯ = (π΄ -s ( 1s /su π))} |s {π₯ β£ βπ β βs π₯ = (π΄ +s ( 1s /su π))})))) | ||
Theorem | recut 28263* | The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β No β {π₯ β£ βπ β βs π₯ = (π΄ -s ( 1s /su π))} <<s {π₯ β£ βπ β βs π₯ = (π΄ +s ( 1s /su π))}) | ||
Theorem | 0reno 28264 | Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ 0s β βs | ||
Theorem | renegscl 28265 | The surreal reals are closed under negation. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ (π΄ β βs β ( -us βπ΄) β βs) | ||
Theorem | readdscl 28266 | The surreal reals are closed under addition. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.) |
β’ ((π΄ β βs β§ π΅ β βs) β (π΄ +s π΅) β βs) | ||
Theorem | remulscllem1 28267* | Lemma for remulscl 28269. Split a product of reciprocals of naturals. (Contributed by Scott Fenton, 16-Apr-2025.) |
β’ (βπ β βs βπ β βs π΄ = (π΅πΉ(( 1s /su π) Β·s ( 1s /su π))) β βπ β βs π΄ = (π΅πΉ( 1s /su π))) | ||
Theorem | remulscllem2 28268* | Lemma for remulscl 28269. Bound π΄ and π΅ above and below. (Contributed by Scott Fenton, 16-Apr-2025.) |
β’ (((π΄ β No β§ π΅ β No ) β§ ((π β βs β§ π β βs) β§ ((( -us βπ) <s π΄ β§ π΄ <s π) β§ (( -us βπ) <s π΅ β§ π΅ <s π)))) β βπ β βs (( -us βπ) <s (π΄ Β·s π΅) β§ (π΄ Β·s π΅) <s π)) | ||
Theorem | remulscl 28269 | The surreal reals are closed under multiplication. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 16-Apr-2025.) |
β’ ((π΄ β βs β§ π΅ β βs) β (π΄ Β·s π΅) β βs) | ||
This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure π is a set (of points) (Baseβπ) together with functions (Itvβπ) and (distβπ) on ((Baseβπ) Γ (Baseβπ)) satisfying certain axioms (given in Definitions df-trkg 28296 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17110). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure π. One defines a betweenness ternary predicate Btw by positing that, for any π₯, π¦, π§ β (Baseβπ), one has "Btw π₯π¦π§ " if and only if π¦ β π₯(Itvβπ)π§, and a congruence quaternary predicate Congr by positing that, for any π₯, π¦, π§, π‘ β (Baseβπ), one has "Congr π₯π¦π§π‘ " if and only if π₯(distβπ)π¦ = π§(distβπ)π‘. It is easy to check that if π satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Baseβπ) is interpreted as the universe of discourse. Conversely, suppose that one is given a set π, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure π such that (Baseβπ) is π, and (Itvβπ) is the function which associates with each β¨π₯, π¦β© β (π Γ π) the set of points π§ β π such that "Btw π₯π§π¦", and (distβπ) is the function which associates with each β¨π₯, π¦β© β (π Γ π) the set of ordered pairs β¨π§, π‘β© β (π Γ π) such that "Congr π₯π¦π§π‘". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when π is interpreted as the universe of discourse, then π satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as π₯(distβπ)π¦ = π§(distβπ)π‘ instead of "Congr π₯π¦π§π‘", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when conguence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form π₯(distβπ)π¦ = π§(distβπ)π‘ causes no loss of generality in tgjustc1 28318 and tgjustc2 28319, which in turn are supported by tgjustf 28316 and tgjustr 28317. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/ 28317. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents π β) by insert a β€ β in each hypothesis, using a1i 11, then using mptru 1540 to remove the final β€ β prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 483, the theorem as stated, and ex 411. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 28296), of "Euclidean dimensionless Tarski structures" (df-trkge 28294) and of "Tarski structures of dimension no less than N" (df-trkgld 28295). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28651 and iscgra 28652). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 28354. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement. | ||
Syntax | cstrkg 28270 | Extends class notation with the class of Tarski geometries. |
class TarskiG | ||
Syntax | cstrkgc 28271 | Extends class notation with the class of geometries fulfilling the congruence axioms. |
class TarskiGC | ||
Syntax | cstrkgb 28272 | Extends class notation with the class of geometries fulfilling the betweenness axioms. |
class TarskiGB | ||
Syntax | cstrkgcb 28273 | Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms. |
class TarskiGCB | ||
Syntax | cstrkgld 28274 | Extends class notation with the relation for geometries fulfilling the lower dimension axioms. |
class DimTarskiGβ₯ | ||
Syntax | cstrkge 28275 | Extends class notation with the class of geometries fulfilling Euclid's axiom. |
class TarskiGE | ||
Syntax | citv 28276 | Declare the syntax for the Interval (segment) index extractor. |
class Itv | ||
Syntax | clng 28277 | Declare the syntax for the Line function. |
class LineG | ||
Definition | df-itv 28278 | Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 28282 instead. (New usage is discouraged.) |
β’ Itv = Slot ;16 | ||
Definition | df-lng 28279 | Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 28283 instead. (New usage is discouraged.) |
β’ LineG = Slot ;17 | ||
Theorem | itvndx 28280 | Index value of the Interval (segment) slot. Use ndxarg 17159. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.) |
β’ (Itvβndx) = ;16 | ||
Theorem | lngndx 28281 | Index value of the "line" slot. Use ndxarg 17159. (Contributed by Thierry Arnoux, 27-Mar-2019.) (New usage is discouraged.) |
β’ (LineGβndx) = ;17 | ||
Theorem | itvid 28282 | Utility theorem: index-independent form of df-itv 28278. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ Itv = Slot (Itvβndx) | ||
Theorem | lngid 28283 | Utility theorem: index-independent form of df-lng 28279. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
β’ LineG = Slot (LineGβndx) | ||
Theorem | slotsinbpsd 28284 | The slots Base, +g, Β·π and dist are different from the slot Itv. Formerly part of ttglem 28720 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
β’ (((Itvβndx) β (Baseβndx) β§ (Itvβndx) β (+gβndx)) β§ ((Itvβndx) β ( Β·π βndx) β§ (Itvβndx) β (distβndx))) | ||
Theorem | slotslnbpsd 28285 | The slots Base, +g, Β·π and dist are different from the slot LineG. Formerly part of ttglem 28720 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
β’ (((LineGβndx) β (Baseβndx) β§ (LineGβndx) β (+gβndx)) β§ ((LineGβndx) β ( Β·π βndx) β§ (LineGβndx) β (distβndx))) | ||
Theorem | lngndxnitvndx 28286 | The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 28718. (Contributed by AV, 9-Nov-2024.) |
β’ (LineGβndx) β (Itvβndx) | ||
Theorem | trkgstr 28287 | Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ π Struct β¨1, ;16β© | ||
Theorem | trkgbas 28288 | The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (π β π β π = (Baseβπ)) | ||
Theorem | trkgdist 28289 | The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (π· β π β π· = (distβπ)) | ||
Theorem | trkgitv 28290 | The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (πΌ β π β πΌ = (Itvβπ)) | ||
Definition | df-trkgc 28291* | Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2748, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ TarskiGC = {π β£ [(Baseβπ) / π][(distβπ) / π](βπ₯ β π βπ¦ β π (π₯ππ¦) = (π¦ππ₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ππ¦) = (π§ππ§) β π₯ = π¦))} | ||
Definition | df-trkgb 28292* | Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ TarskiGB = {π β£ [(Baseβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)))} | ||
Definition | df-trkgcb 28293* | Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ TarskiGCB = {π β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ β π βπ β π βπ β π βπ£ β π (((π₯ β π¦ β§ π¦ β (π₯ππ§) β§ π β (πππ)) β§ (((π₯ππ¦) = (πππ) β§ (π¦ππ§) = (πππ)) β§ ((π₯ππ’) = (πππ£) β§ (π¦ππ’) = (πππ£)))) β (π§ππ’) = (πππ£)) β§ βπ₯ β π βπ¦ β π βπ β π βπ β π βπ§ β π (π¦ β (π₯ππ§) β§ (π¦ππ§) = (πππ)))} | ||
Definition | df-trkge 28294* | Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ TarskiGE = {π β£ [(Baseβπ) / π][(Itvβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ£) β§ π’ β (π¦ππ§) β§ π₯ β π’) β βπ β π βπ β π (π¦ β (π₯ππ) β§ π§ β (π₯ππ) β§ π£ β (πππ)))} | ||
Definition | df-trkgld 28295* | Define the class of geometries fulfilling the lower dimension axiom for dimension π. For such geometries, there are three non-colinear points that are equidistant from π β 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.) (Revised by Thierry Arnoux, 23-Nov-2019.) |
β’ DimTarskiGβ₯ = {β¨π, πβ© β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} | ||
Definition | df-trkg 28296* |
Define the class of Tarski geometries. A Tarski geometry is a set of
points, equipped with a betweenness relation (denoting that a point lies
on a line segment between two other points) and a congruence relation
(denoting equality of line segment lengths).
Here, we are using the following:
Tarski originally had more axioms, but later reduced his list to 11:
So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5). It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained. Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) (Revised by Thierry Arnoux, 27-Apr-2019.) |
β’ TarskiG = ((TarskiGC β© TarskiGB) β© (TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) | ||
Theorem | istrkgc 28297* | Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGC β (πΊ β V β§ (βπ₯ β π βπ¦ β π (π₯ β π¦) = (π¦ β π₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦)))) | ||
Theorem | istrkgb 28298* | Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGB β (πΊ β V β§ (βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))))) | ||
Theorem | istrkgcb 28299* | Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGCB β (πΊ β V β§ (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ β π βπ β π βπ β π βπ£ β π (((π₯ β π¦ β§ π¦ β (π₯πΌπ§) β§ π β (ππΌπ)) β§ (((π₯ β π¦) = (π β π) β§ (π¦ β π§) = (π β π)) β§ ((π₯ β π’) = (π β π£) β§ (π¦ β π’) = (π β π£)))) β (π§ β π’) = (π β π£)) β§ βπ₯ β π βπ¦ β π βπ β π βπ β π βπ§ β π (π¦ β (π₯πΌπ§) β§ (π¦ β π§) = (π β π))))) | ||
Theorem | istrkge 28300* | Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGE β (πΊ β V β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ£) β§ π’ β (π¦πΌπ§) β§ π₯ β π’) β βπ β π βπ β π (π¦ β (π₯πΌπ) β§ π§ β (π₯πΌπ) β§ π£ β (ππΌπ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |