SetTheory.PGame.numeric_nat
theorem SetTheory.PGame.numeric_nat : ∀ (n : ℕ), (↑n).Numeric
This theorem states that all pre-games that are defined by natural numbers are numeric. In other words, if you have a pre-game that is represented by a natural number `n` (denoted as `↑n` in the code), the theorem guarantees that this pre-game will obey the properties of a numeric pre-game as defined in Set Theory and Game Theory.
More concisely: Every pre-game represented by a natural number is a numeric pre-game.
|
SetTheory.PGame.lf_iff_lt
theorem SetTheory.PGame.lf_iff_lt : ∀ {x y : SetTheory.PGame}, x.Numeric → y.Numeric → (x.LF y ↔ x < y)
The theorem `SetTheory.PGame.lf_iff_lt` states that for any two pre-games `x` and `y`, if both `x` and `y` are numeric pre-games, then `x` is less fuzzy (`LF`) than `y` if and only if `x` is less than `y`. Here, a pre-game is called numeric if for every pair of elements from its left (`L`) and right (`R`) sets, the left element is less than the right one, and all elements of `L` and `R` are numeric themselves. The less fuzzy (`LF`) relation on pre-games is defined such that if `0` is not less than or equal to `x`, then the Left player can win `x` as the first player.
More concisely: For any numeric pre-games x and y, x is less fuzzy than y if and only if x is strictly less than y.
|
SetTheory.PGame.Numeric.mk
theorem SetTheory.PGame.Numeric.mk :
∀ {x : SetTheory.PGame},
(∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) →
(∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) → (∀ (j : x.RightMoves), (x.moveRight j).Numeric) → x.Numeric
The theorem `SetTheory.PGame.Numeric.mk` states that, for any pre-game `x`, if every move by the Left player results in a game that is less than any resulting game from a move by the Right player, and if after every move by either the Left or Right player the resulting game is numeric, then the original pre-game `x` is also numeric. In other words, a pre-game is considered numeric if it satisfies two conditions: First, for any allowable move of the Left and Right players, the game resulting from the Left's move is always less than the one resulting from the Right's move. Second, every game resulting from an allowable move of either player is also numeric.
More concisely: If every move by the Left player in a pre-game results in a numeric game that is strictly less than the numeric game resulting from any move by the Right player, then the pre-game is numeric.
|
SetTheory.PGame.LF.lt
theorem SetTheory.PGame.LF.lt : ∀ {x y : SetTheory.PGame}, x.LF y → x.Numeric → y.Numeric → x < y
The theorem `SetTheory.PGame.LF.lt` establishes that for any two pre-games `x` and `y`, if the less or fuzzy relation holds for `x` and `y` (denoted as `SetTheory.PGame.LF x y`), and both `x` and `y` are numeric pre-games (that is, for all elements in the left set of `x` or `y`, there is an element in the right set that is greater, and all elements of the left and right sets are also numeric), then `x` is less than `y` (denoted as `x < y`). Here, a less or fuzzy relation implies that the second player cannot win the game when the game starts from `y`, assuming optimal play.
More concisely: If `x` and `y` are numeric pre-games such that the less or fuzzy relation `SetTheory.PGame.LF x y` holds, then `x < y`.
|
SetTheory.PGame.Relabelling.numeric_congr
theorem SetTheory.PGame.Relabelling.numeric_congr :
∀ {x y : SetTheory.PGame}, x.Relabelling y → (x.Numeric ↔ y.Numeric)
This theorem states that in the context of set theory and games, if a game `x` is relabelled to create a game `y`, the property of being numeric is preserved. In other words, if `x` is numeric, then `y` will be numeric as well, and vice versa. The term "numeric" in this context pertains to a property of a game in combinatorial game theory.
More concisely: If two combinatorial games `x` and `y` are related by a relabelling, then `x` being numeric implies `y` being numeric, and vice versa.
|
SetTheory.PGame.lt_def
theorem SetTheory.PGame.lt_def :
∀ {x y : SetTheory.PGame},
x.Numeric →
y.Numeric →
(x < y ↔
(∃ i,
(∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧
∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨
∃ j,
(∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧
∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j')
The theorem `SetTheory.PGame.lt_def` provides a definition for the less than (`<`) relation for numeric pre-games. For any two numeric pre-games `x` and `y`, `x` is less than `y` if and only if either there exists a left move `i` for `x` such that, for all `i'`, `x.moveLeft i'` is less than `y.moveLeft i` and for all right moves `j` of `y.moveLeft i`, `x` is less than `(y.moveLeft i).moveRight j`; or there exists a right move `j` for `x` such that, for all `i`, `(x.moveRight j).moveLeft i` is less than `y` and for all `j'`, `x.moveRight j` is less than `y.moveRight j'`.
More concisely: For any numeric pre-games x and y, x < y if and only if there exists an i (respectively j) such that x.moveLeft i < y.moveLeft i and for all j (respectively i) of y.moveLeft i and x.moveRight j, x < (y.moveLeft i).moveRight j (respectively x < y.moveRight j).
|
SetTheory.PGame.Numeric.moveLeft
theorem SetTheory.PGame.Numeric.moveLeft :
∀ {x : SetTheory.PGame}, x.Numeric → ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric
This theorem states that for any pre-game `x` in set theory, if `x` is numeric (i.e., every element in the left set `L` is less than every element in the right set `R`, and all elements of `L` and `R` are numeric), then for every allowable move `i` by the Left player, the resulting pre-game after Left makes move `i` will also be numeric. In other words, making a valid move in a numeric pre-game will result in another numeric pre-game.
More concisely: For any pre-game `x` in set theory that is numeric and for every allowable move `i` by the Left player, the resulting pre-game is also numeric.
|
SetTheory.PGame.le_iff_forall_lt
theorem SetTheory.PGame.le_iff_forall_lt :
∀ {x y : SetTheory.PGame},
x.Numeric →
y.Numeric → (x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i < y) ∧ ∀ (j : y.RightMoves), x < y.moveRight j)
This theorem defines the "less than or equal to" (`≤`) relation for numeric pre-games in set theory. Specifically, it states that for all numeric pre-games `x` and `y`, `x` is less than or equal to `y` if and only if for every possible left move from `x`, the result is less than `y`, and for every possible right move from `y`, `x` is less than the result of the move. In simpler terms, `x` is less than or equal to `y` if `x`'s every left move is less than `y` and `y`'s every right move is greater than `x`.
More concisely: For all numeric pre-games x and y, x ≤ y if and only if for every left move from x, the result is less than y, and for every right move from y, the result is greater than x.
|
SetTheory.PGame.numeric_zero
theorem SetTheory.PGame.numeric_zero : SetTheory.PGame.Numeric 0
The theorem `SetTheory.PGame.numeric_zero` states that the zero pre-game in set theory is numeric. In this context, a pre-game is numeric if all elements in the left set are less than all elements in the right set, and all elements of the left and right sets are also numeric. The zero pre-game, represented as `0`, satisfies these conditions and thus is considered numeric.
More concisely: The theorem `SetTheory.PGame.numeric_zero` asserts that the set `0` (zero) is numeric in the context of set theory pre-games, meaning that all elements in `0` are less than all elements outside of `0`.
|
SetTheory.PGame.Numeric.moveRight
theorem SetTheory.PGame.Numeric.moveRight :
∀ {x : SetTheory.PGame}, x.Numeric → ∀ (j : x.RightMoves), (x.moveRight j).Numeric
The theorem `SetTheory.PGame.Numeric.moveRight` states that for any pre-game `x` in set theory, if `x` is a numeric game (meaning that every element in the left set `L` is less than every element in the right set `R`, and all the elements of `L` and `R` are also numeric), then for any allowable move `j` by the right player, the resulting game after the right player makes move `j`, denoted by `SetTheory.PGame.moveRight x j`, is also a numeric game.
More concisely: For any pre-game `x` in set theory that is a numeric game, the resulting game obtained by a right player's move `j` is also a numeric game.
|
SetTheory.PGame.LF.le
theorem SetTheory.PGame.LF.le : ∀ {x y : SetTheory.PGame}, x.LF y → x.Numeric → y.Numeric → x ≤ y
This theorem, which is an alias of `SetTheory.PGame.le_of_lf`, states that for any two pre-games `x` and `y`, if the less or fuzzy relation holds between `x` and `y`, and if both `x` and `y` are numeric pre-games, then `x` is less than or equal to `y`. The less or fuzzy relation `SetTheory.PGame.LF x y` means that the second player cannot win when the game starts from `y`. A pre-game is numeric if all elements in the left set are less than all elements in the right set, and all elements of the left and right sets are also numeric.
More concisely: If pre-games x and y are numeric and the less or fuzzy relation LF holds between them (i.e., player 2 cannot win starting from y), then x ≤ y.
|
SetTheory.PGame.lt_iff_exists_le
theorem SetTheory.PGame.lt_iff_exists_le :
∀ {x y : SetTheory.PGame}, x.Numeric → y.Numeric → (x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) := by
sorry
This theorem defines the less than relation ('<') between two numeric pre-games `x` and `y`. According to this theorem, `x` is less than `y` if and only if there exists an index `i` such that `x` is less than or equal to the left move of `y` at `i`, or there exists an index `j` such that the right move of `x` at `j` is less than or equal to `y`. Both `x` and `y` are assumed to be numeric pre-games.
More concisely: The theorem states that `x` is less than `y` if and only if there exists an index `i` such that `x <= y.prev i` or there exists an index `j` such that `x.next j <= y`.
|
SetTheory.PGame.numeric_toPGame
theorem SetTheory.PGame.numeric_toPGame : ∀ (o : Ordinal.{u_1}), o.toPGame.Numeric
This theorem states that for every ordinal 'o', the corresponding positional game ('PGame') is numeric. In other words, it asserts that every ordinal can be translated into a positional game in such a way that the game has the property of being numeric. The numeric property of positional games is a fundamental concept in game theory that corresponds to having a specific mathematical structure.
More concisely: For every ordinal 'o', the ordinal game 'PGame(o)' is numeric.
|