LeanAide GPT-4 documentation

Module: Mathlib.SetTheory.Game.PGame

SetTheory.PGame.Relabelling.equiv

theorem SetTheory.PGame.Relabelling.equiv : ∀ {x y : SetTheory.PGame}, x.Relabelling y → x ≈ y

This theorem states that if we have a relabelling of any two games `x` and `y` in Set Theory's Game theory, then `x` and `y` are equivalent. In other words, if we can essentially rename the moves in game `x` to match the moves in game `y` without changing the structure of the game itself, then the two games are equivalent in terms of strategy and outcome. Here, equivalence (≈) is a specific mathematical concept that means the two games have the same outcomes for optimal play.

More concisely: If two games in Set Theory's Game theory are relabeling equivalent, then they are strategically and outcome-wise equal.

SetTheory.PGame.fuzzy_congr

theorem SetTheory.PGame.fuzzy_congr : ∀ {x₁ y₁ x₂ y₂ : SetTheory.PGame}, x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁.Fuzzy y₁ ↔ x₂.Fuzzy y₂)

This theorem, `SetTheory.PGame.fuzzy_congr`, states that for any four pre-games `x₁`, `y₁`, `x₂`, and `y₂`, if `x₁` is equivalent to `x₂` and `y₁` is equivalent to `y₂`, then the fuzzy relationship between `x₁` and `y₁` is the same as the fuzzy relationship between `x₂` and `y₂`. In other words, if two pairs of pre-games are each equivalent within their pair, then the "fuzziness" or confusion between the games in the first pair is the same as that in the second pair. Here, a fuzzy relationship between two pre-games means that the first player can always win either game.

More concisely: If pre-games x₁, y₁, x₂, and y₂ satisfy x₁ ≈ x₂ and y₁ ≈ y₂, then the fuzzy relationship between x₁ and y₁ is equal to the fuzzy relationship between x₂ and y₂.

SetTheory.PGame.rightResponse_spec

theorem SetTheory.PGame.rightResponse_spec : ∀ {x : SetTheory.PGame} (h : x ≤ 0) (i : x.LeftMoves), (x.moveLeft i).moveRight (SetTheory.PGame.rightResponse h i) ≤ 0

This theorem states that for any game `x` from Set Theory that the right player wins when they play second, for any move `i` made by the left player, the response given by the `rightResponse` function ensures the right-player-wins condition. Here, the `rightResponse` function is defined such that it takes a game `x` that is won by the right player playing second and a move `i` by the left player, and it returns a valid move for the right player. The theorem verifies that after executing such a response move, the game remains in a state where the right player, if playing second, would win.

More concisely: For any game `x` won by the right player playing second and any move `i` by the left player, the right player's response move guarantees that they still win when playing second in the resulting game.

SetTheory.PGame.neg_lt_neg_iff

theorem SetTheory.PGame.neg_lt_neg_iff : ∀ {x y : SetTheory.PGame}, -y < -x ↔ x < y

This theorem states that for any two games `x` and `y` in set theory, the negative of `y` is less than the negative of `x` if and only if `x` is less than `y`. This is a reflection of the property of order inversion when multiplying by a negative number in real numbers.

More concisely: For any two sets x and y, -x < -y if and only if x < y.

LE.le.not_gf

theorem LE.le.not_gf : ∀ {x y : SetTheory.PGame}, x ≤ y → ¬y.LF x

This theorem states that for any two pre-games `x` and `y` in set theory, if `x` is less than or equal to `y`, then it is not the case that `y` is less fuzzy than `x`. In other words, if `x` is less than or equal to `y`, then Left cannot win `x` as the first player when playing `y`. This is a fundamental property connecting the less-or-equal and less fuzzy relations in the theory of pre-games.

More concisely: For any pre-games x and y in set theory, if x <= y then y is not less fuzzy than x (i.e., Left cannot win x as the first player when playing y).

SetTheory.PGame.lf_moveRight

theorem SetTheory.PGame.lf_moveRight : ∀ {x : SetTheory.PGame} (j : x.RightMoves), x.LF (x.moveRight j)

This theorem states that for any pre-game `x` and any allowable right move `j` in this game, if `x` is less fuzzy than the new game resulting after Right makes the move `j`, then Left can win the new game as the first player. In other words, this theorem is capturing a particular dynamic of the pre-game: if the game after Right's allowed move is in a "fuzzy" relation with the original game (not clearly greater or less), then Left has a winning strategy for the new game.

More concisely: If a pre-game `x` is less fuzzy than the game resulting after Right makes an allowable move `j`, then Left has a winning strategy as the first player in the new game.

SetTheory.PGame.lf_of_le_moveLeft

theorem SetTheory.PGame.lf_of_le_moveLeft : ∀ {x y : SetTheory.PGame} {i : y.LeftMoves}, x ≤ y.moveLeft i → x.LF y := by sorry

This theorem establishes a property of pre-games in set theory. Specifically, it states that for all pre-games `x` and `y`, and for any allowed move `i` by the 'Left' player in the game `y`, if `x` is less than or equal to the game resulting after the 'Left' player makes move `i` in `y`, then `x` is in a less or fuzzy relation with `y`. In other words, if the 'Left' player can transition the game `y` to a state `x` or better (from their perspective), then the 'Left' player has a winning strategy for the game `y`.

More concisely: For all pre-games x and y, and allowed move i for the 'Left' player in y, if x ≤ y[i] then x ⪯ y. (Here, ≤ denotes the preorder relation in the set of pre-games, and ⪯ denotes the reflexive and transitive closure of the relation that holds between two pre-games x and y if there exists a winning strategy for player 'Left' in the game y starting from initial state x.)

SetTheory.PGame.neg_equiv_iff

theorem SetTheory.PGame.neg_equiv_iff : ∀ {x y : SetTheory.PGame}, -x ≈ y ↔ x ≈ -y

This theorem states that for any two games `x` and `y` in Set Theory, the negation of `x` is equivalent to `y` if and only if `x` is equivalent to the negation of `y`. Here, `≈` represents the equivalence of games in set theory and `-` represents the negation of a game.

More concisely: For any games x and y in Set Theory, x ≈ y if and only if -x ≈ -y.

SetTheory.PGame.add_lf_add_right

theorem SetTheory.PGame.add_lf_add_right : ∀ {y z : SetTheory.PGame}, y.LF z → ∀ (x : SetTheory.PGame), (y + x).LF (z + x)

The theorem `SetTheory.PGame.add_lf_add_right` states that for any pre-games `y` and `z`, if `y` is less or fuzzy compared to `z` (meaning that if you start with `z` instead of `0`, the Left player can win), then for any pre-game `x`, the addition of `x` to `y` is also less or fuzzy compared to the addition of `x` to `z`. In other words, adding the same pre-game `x` to both `y` and `z` maintains the less or fuzzy relation between `y` and `z`.

More concisely: If pre-games `y` is less or fuzzy than `z`, then the sum of any pre-game `x` with `y` is less or fuzzy than the sum of `x` with `z`.

SetTheory.PGame.zero_lt_one

theorem SetTheory.PGame.zero_lt_one : 0 < 1

The theorem `SetTheory.PGame.zero_lt_one` in Lean 4 asserts that zero is less than one. In the context of set theory and game theory, this compares the game numbers 0 and 1, and states that 0 is less than 1. This theorem is fundamental in mathematics and is used as a basis for many other mathematical concepts and theories.

More concisely: The theorem `SetTheory.PGame.zero_lt_one` in Lean 4 asserts that 0 < 1.

SetTheory.PGame.sub_zero

theorem SetTheory.PGame.sub_zero : ∀ (x : SetTheory.PGame), x - 0 = x + 0

This theorem states that for any "PGame" in set theory, the difference of the game and zero is equal to the sum of the game and zero. Here, "PGame" refers to the mathematical concept of games, which are combinatorial structures used in game theory and math. It essentially asserts that zero works as an identity element both in subtraction and addition within the context of "PGames".

More concisely: For any "PGame" P in set theory, P - 0 = P + 0.

LT.lt.trans_lf

theorem LT.lt.trans_lf : ∀ {x y z : SetTheory.PGame}, x < y → y.LF z → x.LF z

This theorem, `LT.lt.trans_lf`, states that for any three elements `x`, `y`, and `z` in the set of `SetTheory.PGame`, if `x` is less than `y` and `y` is a left follower of `z`, then `x` is a left follower of `z`. This theorem demonstrates the transitivity of "left-following" in relation to the less than relation in the context of P-games in set theory.

More concisely: If `x` is less than `y` and `y` is a left follower of `z` in `SetTheory.PGame`, then `x` is a left follower of `z`.

SetTheory.PGame.zero_le_add_right_neg

theorem SetTheory.PGame.zero_le_add_right_neg : ∀ (x : SetTheory.PGame), 0 ≤ x + -x

This theorem states that for every PGame `x` in set theory, adding its negation to it results in a value that is greater than or equal to 0. In other words, the sum of any PGame `x` and its negation `-x` is always nonnegative. In traditional mathematical notation, this would be expressed as `0 ≤ x + -x` for all `x`.

More concisely: For all PGame `x`, we have `0 ≤ x + (-x)`.

SetTheory.PGame.zero_le

theorem SetTheory.PGame.zero_le : ∀ {x : SetTheory.PGame}, 0 ≤ x ↔ ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i

The theorem `SetTheory.PGame.zero_le` states that for any pre-game `x`, `0` is less than or equal to `x` if and only if for every allowable move `j` by the right player in game `x`, there exists a move `i` by the left player such that `0` is less than or equal to the new game obtained after right's move `j` and left's subsequent move `i`. This definition of `0 ≤ x` on pre-games reflects the concept that `0 ≤ x` if, no matter what move the right player makes, the left player can respond in a way that maintains the inequality.

More concisely: For any pre-game `x`, `0` is less than or equal to `x` if and only if for every allowable move `j` by the right player, there exists a move `i` by the left player such that `0 ≤ x'` where `x'` is the new game obtained after right's move `j` and left's subsequent move `i`.

SetTheory.PGame.equiv_rfl

theorem SetTheory.PGame.equiv_rfl : ∀ {x : SetTheory.PGame}, x ≈ x

This theorem states that for any given PGame `x` in Set Theory, `x` is equivalent to itself. In other words, it establishes the reflexivity of equivalence (`≈`) for PGames, confirming that any PGame is always considered equivalent to itself. This is a fundamental property of equivalence relations in mathematics.

More concisely: For any PGame x in Set Theory, x ≈ x holds. (Reflexivity of equivalence for PGames)

SetTheory.PGame.le_iff_forall_lf

theorem SetTheory.PGame.le_iff_forall_lf : ∀ {x y : SetTheory.PGame}, x ≤ y ↔ (∀ (i : x.LeftMoves), (x.moveLeft i).LF y) ∧ ∀ (j : y.RightMoves), x.LF (y.moveRight j)

This theorem is defining an ordering of pre-games (`x ≤ y`) in the mathematical field of set theory. The ordering is determined in terms of the less or fuzzy relation (`SetTheory.PGame.LF`), which indicates if the right game (`y`) is not less than or equal to the left game (`x`). The theorem states that a pre-game `x` is less than or equal to another pre-game `y` if and only if two conditions hold: 1. For all allowed moves for the left player in the game `x`, if the left player makes that move, the resulting game is less or fuzzy than the game `y`. 2. For all allowed moves for the right player in the game `y`, if the right player makes that move, the game `x` is less or fuzzy than the resulting game. In other words, `x` is less than or equal to `y` if Left cannot improve `x` to beat `y` and Right can defend `y` to keep it from being worse than `x`.

More concisely: A pre-game x is less than or equal to another pre-game y if and only if for all allowed moves for the left player in x, the resulting game is less or fuzzy than y, and for all allowed moves for the right player in y, the game x is less or fuzzy than the resulting game.

SetTheory.PGame.le_zero_lf

theorem SetTheory.PGame.le_zero_lf : ∀ {x : SetTheory.PGame}, x ≤ 0 ↔ ∀ (i : x.LeftMoves), (x.moveLeft i).LF 0 := by sorry

This theorem defines the concept of a pre-game `x` being less than or equal to zero in the context of set theory games. It states that `x` is less than or equal to zero if and only if for all possible left moves `i` in `x`, the game resulting from that move is a "left-facing" zero game, as indicated by `(x.moveLeft i).LF 0`. In other terms, a pre-game `x` is less than or equal to zero if every possible move for the left player results in a game that is left-facing, denoted as `LF`, and equivalent to zero.

More concisely: A pre-game x is less than or equal to zero if and only if for all its left moves i, the resulting game is a left-facing zero game.

SetTheory.PGame.add_left_neg_le_zero

theorem SetTheory.PGame.add_left_neg_le_zero : ∀ (x : SetTheory.PGame), -x + x ≤ 0

This theorem states that for any given game `x` in set theory, the sum of the negative of `x` and `x` itself is less than or equal to zero. In mathematical terms, it's asserting that ∀x (in the space of Games), -x + x ≤ 0. This is analogous to the property in real numbers where the sum of a number and its negative is always zero. However, in the context of games, the inequality is used instead of an equality because there is no total ordering in games.

More concisely: For all games x, the sum of the negative of x and x is less than or equal to zero: ∀x, -x + x ≤ 0.

SetTheory.PGame.add_zero_equiv

theorem SetTheory.PGame.add_zero_equiv : ∀ (x : SetTheory.PGame), x + 0 ≈ x

This theorem states that for every element `x` of the set `SetTheory.PGame`, the sum of `x` and zero is equivalent to `x`. In mathematical terms, it expresses the property `x + 0 ≈ x` for all `x` in the set of games in set theory. This is a formal expression in Lean 4 of the standard mathematical property that adding zero to any number does not change its value.

More concisely: For all `x` in the set of games in set theory, `x + 0 ≈ x`. (This statement expresses that the sum of any game `x` with zero is equivalent to `x` itself.)

SetTheory.PGame.add_comm_le

theorem SetTheory.PGame.add_comm_le : ∀ {x y : SetTheory.PGame}, x + y ≤ y + x

This theorem states that, for all elements `x` and `y` of the type `SetTheory.PGame` (which represents games in set theory), the sum `x + y` is less than or equal to the sum `y + x`. In mathematical terms, this means that addition of these games is commutative with respect to the 'less than or equal to' relation. This essentially says that swapping the order of summands doesn't increase the value of the sum.

More concisely: For all `x` and `y` in `SetTheory.PGame`, `x + y` is less than or equal to `y + x`. (Or, equivalently, addition of games in `SetTheory.PGame` is commutative with respect to the 'less than or equal to' relation.)

SetTheory.PGame.Fuzzy.lf

theorem SetTheory.PGame.Fuzzy.lf : ∀ {x y : SetTheory.PGame}, x.Fuzzy y → x.LF y

This theorem, `SetTheory.PGame.Fuzzy.lf`, is an alias of `SetTheory.PGame.lf_of_fuzzy`. It states that for any two games `x` and `y` in Set Theory, if `x` is fuzzy with respect to `y`, then `x` is left-favorable to `y`. In simpler terms, if `x` and `y` are such that their outcome cannot be determined with certainty (i.e., they are 'fuzzy'), then `x` is more likely to be won by the left player.

More concisely: If two games are fuzzy (i.e., their outcomes are indeterminate with respect to each other), then the first game is left-favorable (has a higher expected value for the left player).

SetTheory.PGame.not_lf

theorem SetTheory.PGame.not_lf : ∀ {x y : SetTheory.PGame}, ¬x.LF y ↔ y ≤ x

This theorem states that for any two pre-games `x` and `y` in Set Theory, the negation of the less or fuzzy relation `SetTheory.PGame.LF x y` holds if and only if `y` is less than or equal to `x`. In other words, if `y` is not strictly better for the first player than `x` (that is, the first player cannot win `y` when `x` is played), then `y` is less than or equal to `x`.

More concisely: The theorem asserts that for all pre-games x and y in Set Theory, the negation of x having a strict less or fuzzy relation to y holds if and only if y is less than or equal to x.

SetTheory.PGame.zero_lf

theorem SetTheory.PGame.zero_lf : ∀ {x : SetTheory.PGame}, SetTheory.PGame.LF 0 x ↔ ∃ i, ∀ (j : (x.moveLeft i).RightMoves), SetTheory.PGame.LF 0 ((x.moveLeft i).moveRight j)

The theorem `SetTheory.PGame.zero_lf` characterizes the "less or fuzzy" relation between the zero game and any pre-game `x`, denoted as `0 ⧏ x`. It states that `0` is less or fuzzy than `x`, if and only if there exists a legal left move for `x` such that for every subsequent legal right move, `0` is still less or fuzzy than the resulting game. Essentially, this means that the first player, Left, can always make a move in `x` such that no matter how Right responds, Left can still win, indicating that Left has a winning strategy in the game `x`.

More concisely: The theorem `SetTheory.PGame.zero_lf` asserts that `0 ⧏ x` if and only if there exists a legal move for `x` such that the resulting game, after any sequence of legal right moves, still has `0` as the less or fuzzy relation. In other words, Left has a winning strategy in every possible continuation of the game `x` starting from a legal move.

SetTheory.PGame.le_of_forall_lt

theorem SetTheory.PGame.le_of_forall_lt : ∀ {x y : SetTheory.PGame}, (∀ (i : x.LeftMoves), x.moveLeft i < y) → (∀ (j : y.RightMoves), x < y.moveRight j) → x ≤ y

This theorem, `SetTheory.PGame.le_of_forall_lt`, establishes a special condition for determining whether one surreal number (or PGame) is less than or equal to another. Specifically, it states that for any two surreal numbers `x` and `y`, if for all left moves `i` in `x`, moving left from `x` results in a number less than `y`, and if for all right moves `j` in `y`, `x` is less than the result of moving right from `y`, then `x` is less than or equal to `y`.

More concisely: If for all left moves in x and for all right moves in y, moving in that direction from x and y, respectively, results in a number strictly less than the other, then x is less than or equal to y.

SetTheory.PGame.add_lf_add_left

theorem SetTheory.PGame.add_lf_add_left : ∀ {y z : SetTheory.PGame}, y.LF z → ∀ (x : SetTheory.PGame), (x + y).LF (x + z)

This theorem states that for all pre-games 'y' and 'z', if 'y' is strictly less fuzzy than 'z' (i.e., Left can win 'z' as the first player but not 'y'), then for any pre-game 'x', the pre-game 'x + y' is also strictly less fuzzy than 'x + z'. In other words, adding the same pre-game 'x' to both 'y' and 'z' preserves the less fuzzy relation.

More concisely: For all pre-games 'x', 'y', and 'z', if 'y' is strictly less fuzzy than 'z', then 'x + y' is strictly less fuzzy than 'x + z'.

SetTheory.PGame.le_zero

theorem SetTheory.PGame.le_zero : ∀ {x : SetTheory.PGame}, x ≤ 0 ↔ ∀ (i : x.LeftMoves), ∃ j, (x.moveLeft i).moveRight j ≤ 0

The theorem `SetTheory.PGame.le_zero` is defining what `x ≤ 0` means for pre-games in set theory. Specifically, a pre-game `x` is less than or equal to 0 if and only if, for every possible move `i` that Left can make in `x`, there exists a counter-move `j` that Right can make such that after these two moves, the resulting pre-game is less than or equal to 0. In other words, no matter what move Left makes, Right can always respond in such a way that the game state stays less than or equal to 0.

More concisely: A pre-game x is less than or equal to 0 if and only if for every move i by Left, Right has a counter-move j such that the resulting pre-game is less than or equal to 0.

SetTheory.PGame.lt_congr

theorem SetTheory.PGame.lt_congr : ∀ {x₁ y₁ x₂ y₂ : SetTheory.PGame}, x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ < y₁ ↔ x₂ < y₂) := by sorry

This theorem states that in set theory, specifically regarding games, if two games `x₁` and `x₂` are equivalent, and two other games `y₁` and `y₂` are also equivalent, then the inequality (less than) relationship between `x₁` and `y₁` is the same as the inequality relationship between `x₂` and `y₂`. Essentially, equivalence in games preserves the inequality relationship.

More concisely: If games `x₁` and `x₂`, and `y₁` and `y₂` are equivalent, then `x₁ < y₁` if and only if `x₂ < y₂`.

SetTheory.PGame.Subsequent.trans

theorem SetTheory.PGame.Subsequent.trans : ∀ {x y z : SetTheory.PGame}, x.Subsequent y → y.Subsequent z → x.Subsequent z

The theorem `SetTheory.PGame.Subsequent.trans` states that for any three games `x`, `y`, and `z` in the context of set theory games (`SetTheory.PGame`), if game `x` can be obtained by playing some nonempty sequence of moves from game `y` (which is expressed as `SetTheory.PGame.Subsequent x y`) and game `y` can be similarly obtained from game `z` (`SetTheory.PGame.Subsequent y z`), then game `x` can also be obtained by playing some nonempty sequence of moves from game `z` (`SetTheory.PGame.Subsequent x z`). This is a statement of transitivity in the context of obtaining one game from another through a sequence of moves.

More concisely: If games `x`, `y`, and `z` in set theory have the property that `x` can be obtained from `y` and `y` can be obtained from `z`, then `x` can be obtained from `z`. (Transitivity of game subsequence relation in set theory)

SetTheory.PGame.Equiv.symm

theorem SetTheory.PGame.Equiv.symm : ∀ {x y : SetTheory.PGame}, x ≈ y → y ≈ x

This theorem states that in the framework of Set Theory and specifically with PGames, if a PGame `x` is equivalent to PGame `y` then `y` is also equivalent to `x`. In other words, the equivalence relation between PGames is symmetric.

More concisely: In the context of Set Theory and PGames, the equivalence relation on PGames is symmetric.

SetTheory.PGame.zero_le_lf

theorem SetTheory.PGame.zero_le_lf : ∀ {x : SetTheory.PGame}, 0 ≤ x ↔ ∀ (j : x.RightMoves), SetTheory.PGame.LF 0 (x.moveRight j)

This theorem is about the definition of `0 ≤ x` on pre-games in the mathematical field of Set Theory. It states that for any pre-game `x`, `0` is less than or equal to `x` if and only if for all possible right moves `j` in `x`, `0` is in a "less or fuzzy" relation with the pre-game resulting from making right move `j` in `x`. In other words, the "less or fuzzy" relation is being used to define when `0` is less than or equal to a pre-game `x`: it is when, no matter what right move is made, `0` can't be overtaken by `x`.

More concisely: For any pre-game `x`, `0` is less than or equal to `x` if and only if `0` is in the "less or fuzzy" relation with the result of making any right move in `x`.

SetTheory.PGame.LF.not_ge

theorem SetTheory.PGame.LF.not_ge : ∀ {x y : SetTheory.PGame}, x.LF y → ¬y ≤ x

This theorem states that for any two pre-games `x` and `y` in set theory, if the "less or fuzzy" relation holds between `x` and `y` (i.e., `SetTheory.PGame.LF x y`), then `y` is not less than or equal to `x` (denoted as `¬y ≤ x`). The less or fuzzy relation is defined such that if `0` is not less than or equal to `x` (`0 ⧏ x`), then the Left player can win `x` as the first player. Therefore, this theorem is essentially asserting that if the Left player has a winning strategy for `x` as the first player, then `y` cannot be less than or equal to `x`.

More concisely: For any pre-games x and y in set theory, if the Left player has a winning strategy as the first player in game x then y is strictly greater than x (i.e., y > x).

SetTheory.PGame.Equiv.trans

theorem SetTheory.PGame.Equiv.trans : ∀ {x y z : SetTheory.PGame}, x ≈ y → y ≈ z → x ≈ z

This theorem states that the equivalence relation on the type of games, denoted by `≈`, is transitive. In other words, for any three games `x`, `y`, and `z` in set theory, if game `x` is equivalent to game `y` and game `y` is equivalent to game `z`, then game `x` is also equivalent to game `z`. This is a fundamental property of equivalence relations in mathematics.

More concisely: If `x ≈ y` and `y ≈ z` then `x ≈ z` for the equivalence relation `≈` on the type of games.

SetTheory.PGame.not_le

theorem SetTheory.PGame.not_le : ∀ {x y : SetTheory.PGame}, ¬x ≤ y ↔ y.LF x

The theorem `SetTheory.PGame.not_le` states that for any two pre-games `x` and `y` in Set Theory, the statement "it is not the case that `x` is less than or equal to `y`" is equivalent to the statement "`y` is in a less or fuzzy relation with `x`". The less or fuzzy relation, denoted by `SetTheory.PGame.LF y x`, means that the game `y` is not less than or equal to game `x`, or in other words, Left can win the game `x` when playing first.

More concisely: The theorem `SetTheory.PGame.not_le` asserts that `x not<= y` is equivalent to `y SetTheory.PGame.LF x` in Set Theory.

SetTheory.PGame.lf_congr

theorem SetTheory.PGame.lf_congr : ∀ {x₁ y₁ x₂ y₂ : SetTheory.PGame}, x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁.LF y₁ ↔ x₂.LF y₂) := by sorry

This theorem states that for any four pre-games `x₁`, `y₁`, `x₂`, and `y₂`, if `x₁` is equivalent to `x₂` and `y₁` is equivalent to `y₂`, then the 'less or fuzzy' relation (`SetTheory.PGame.LF`) holds between `x₁` and `y₁` if and only if it holds between `x₂` and `y₂`. In other words, the 'less or fuzzy' relationship is preserved under equivalence of pre-games. 'Less or fuzzy' relation, denoted as `SetTheory.PGame.LF x y`, implies that Left can win the game `y` as the first player if `0` is not less or equal to `x`.

More concisely: Given any pre-games x₁, y₁, x₂, and y₂, if x₁ is equivalent to x₂ and y₁ is equivalent to y₂, then the 'less or fuzzy' relation (SetTheory.PGame.LF) between x₁ and y₁ holds if and only if it holds between x₂ and y₂.

SetTheory.PGame.LF.trans_lt

theorem SetTheory.PGame.LF.trans_lt : ∀ {x y z : SetTheory.PGame}, x.LF y → y < z → x.LF z

This theorem, `SetTheory.PGame.LF.trans_lt`, states that for any three elements `x`, `y`, and `z` of the type `SetTheory.PGame` (which represents games in set theory), if `x` is less than or equal to `y` in the "left-first" (LF) ordering and `y` is strictly less than `z`, then `x` is less than or equal to `z` in the LF ordering. Essentially, this theorem shows the transitivity property of the LF ordering in the context of set theory games.

More concisely: If `x ≤ y` and `y < z` in the LF ordering of Set Theory games, then `x ≤ z`.

SetTheory.PGame.Subsequent.mk_right

theorem SetTheory.PGame.Subsequent.mk_right : ∀ {xl xr : Type u_1} (xL : xl → SetTheory.PGame) (xR : xr → SetTheory.PGame) (j : xr), (xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)

The theorem `SetTheory.PGame.Subsequent.mk_right` states that for any positions `xl` and `xr`, and any moves `xL` from `xl` and `xR` from `xr`, and any element `j` of `xr`, the position reached by playing the move `xR j` from the game `SetTheory.PGame.mk xl xr xL xR` is subsequent to the original game. In other words, there exists some nonempty sequence of moves starting from the game `SetTheory.PGame.mk xl xr xL xR` that leads to the position `xR j`. This is a formalization of a fundamental aspect of game theory in the context of set theory.

More concisely: For any positions `xl`, `xr`, moves `xL` from `xl` and `xR` from `xr`, and element `j` of `xr` in set theory games, the position obtained by playing move `xR j` from the game `SetTheory.PGame.mk xl xr xL xR` is subsequent to the original game.

SetTheory.PGame.zero_add_equiv

theorem SetTheory.PGame.zero_add_equiv : ∀ (x : SetTheory.PGame), 0 + x ≈ x

This theorem states that adding zero to any element `x` from the set of games in set theory (`SetTheory.PGame`) is equivalent to the element `x` itself. This is quite similar to the common arithmetic rule where the addition of zero to any number does not change the value of the number.

More concisely: For all games `x` in `SetTheory.PGame`, `x + 0 = x`.

LE.le.lf_moveRight

theorem LE.le.lf_moveRight : ∀ {x y : SetTheory.PGame}, x ≤ y → ∀ (j : y.RightMoves), x.LF (y.moveRight j)

This theorem, also known as 'Alias of `SetTheory.PGame.lf_moveRight_of_le`', establishes that for any two games `x` and `y` in Set Theory, if `x` is less than or equal to `y`, then for any right move `j` that can be made in game `y`, the left-first strategy (LF) can be applied to the resulting game `y.moveRight j` starting from game `x`. In other words, it asserts the existence of a valid left-first strategy after a right move in a game that is greater or equal to the other.

More concisely: For any games x and y in Set Theory such that x ≤ y, there exists a left-first strategy for game y.moveRight j starting from x for any right move j in game y.

SetTheory.PGame.lf_of_moveRight_le

theorem SetTheory.PGame.lf_of_moveRight_le : ∀ {x y : SetTheory.PGame} {j : x.RightMoves}, x.moveRight j ≤ y → x.LF y

The theorem `SetTheory.PGame.lf_of_moveRight_le` states that for any games `x` and `y`, and for any allowable move `j` by the Right player in the game `x`, if the new game resulting from the Right player making the move `j` in game `x` is less or equal to game `y` (i.e., `SetTheory.PGame.moveRight x j ≤ y`), then the Left player can win game `x` as the first player when playing against game `y` (i.e., `SetTheory.PGame.LF x y`). In other words, this theorem provides a condition under which the Left player has a winning strategy in the game `x` against `y`.

More concisely: If for any game `x`, allowable move `j` by the Right player, and game `y`, `SetTheory.PGame.moveRight x j ≤ y` implies `SetTheory.PGame.LF x y`.

LE.le.trans_lf

theorem LE.le.trans_lf : ∀ {x y z : SetTheory.PGame}, x ≤ y → y.LF z → x.LF z

This theorem, `LE.le.trans_lf`, is an alias of `SetTheory.PGame.lf_of_le_of_lf`. In the context of set theory and games, it states that for any three given games `x`, `y`, and `z`, if game `x` is less than or equal to game `y` and game `y` has a Left-First move to game `z` (`y.LF z`), then game `x` also has a Left-First move to game `z` (`x.LF z`). In other words, the 'less than or equal to' relation and 'Left-First move' relation are transitive in this context.

More concisely: If game x <= game y and y.LF z holds, then x.LF z holds. (In other words, the relation of being less than or equal to and having a Left-First move is transitive for games.)

SetTheory.PGame.neg_lf_neg_iff

theorem SetTheory.PGame.neg_lf_neg_iff : ∀ {x y : SetTheory.PGame}, (-y).LF (-x) ↔ x.LF y

The theorem `SetTheory.PGame.neg_lf_neg_iff` states that for all pre-games `x` and `y`, the relation `SetTheory.PGame.LF` holds for `-y` and `-x` if and only if it also holds for `x` and `y`. In other words, the less or fuzzy (LF) relationship for the negations of two pre-games is equivalent to the LF relationship of the pre-games themselves. This theorem is related to the notion of winning strategies in game theory. Specifically, if the first player cannot win game `y` when preceded by game `x`, then the first player also cannot win the game `-x` when it is preceded by `-y`.

More concisely: For all pre-games x and y, the less or fuzzy relation SetTheory.PGame.LF holds between -x and -y if and only if it holds between x and y.

SetTheory.PGame.add_congr

theorem SetTheory.PGame.add_congr : ∀ {w x y z : SetTheory.PGame}, w ≈ x → y ≈ z → w + y ≈ x + z

This theorem states that in the context of set theory, and more specifically in the theory of Games, if two games `w` and `x` are equivalent, and two other games `y` and `z` are also equivalent, then the game obtained by adding `w` and `y` is equivalent to the game obtained by adding `x` and `z`. Here, equivalence (≈) between two games means that they have the same outcome when played by perfect players.

More concisely: If games `w` and `x`, and `y` and `z` are equivalent in set theory's games theory context, then `w + y` and `x + z` are equivalent. (Here, `+` denotes the game sum operation, and equivalence means having the same outcome for perfect players.)

SetTheory.PGame.Subsequent.moveRight

theorem SetTheory.PGame.Subsequent.moveRight : ∀ {x : SetTheory.PGame} (j : x.RightMoves), (x.moveRight j).Subsequent x

This theorem in set theory states that for any game `x` and any legal move `j` for the player Right, the game that results after Right makes the move `j` is a subsequent of the game `x`. In other words, the game that you get after Right's move can be reached from `x` by playing some nonempty sequence of moves.

More concisely: For any game `x` and legal move `j` for player Right, there exists a nonempty sequence of moves leading from `x` to the game resulting from Right making move `j`.

SetTheory.PGame.lt_or_equiv_or_gt_or_fuzzy

theorem SetTheory.PGame.lt_or_equiv_or_gt_or_fuzzy : ∀ (x y : SetTheory.PGame), x < y ∨ x ≈ y ∨ y < x ∨ x.Fuzzy y := by sorry

This theorem from set theory, dealing with PGames, states that for any two PGames `x` and `y`, exactly one of the following is true (although it's not proven in this context): `x` is less than `y`, `x` is equivalent to `y`, `y` is less than `x`, or `x` is fuzzy with `y`. In other words, it classifies the relationship between any two PGames into one of these four categories.

More concisely: For any two PGames x and y, there is a reflexive, transitive, and total relation R on PGames such that xRy holds if and only if x is less than or equivalent to y.

SetTheory.PGame.le_def

theorem SetTheory.PGame.le_def : ∀ {x y : SetTheory.PGame}, x ≤ y ↔ (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧ ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j

This theorem defines the order relation "less than or equal to" (≤) for pre-games in terms of the same relation two moves later. Specifically, it states that for any two pre-games x and y, x is less than or equal to y if and only if the following two conditions are met: - For every allowed move i by the Left player in the game x, there exists either a move i' in the game y such that moving Left in x followed by i results in a game less than or equal to moving Left in y followed by i', or there exists a move j such that moving Right after moving Left in x results in a game less than or equal to y. - For every allowed move j by the Right player in the game y, there exists either a move i such that x is less than or equal to moving Left after moving Right in y, or there exists a move j' in x such that moving Right in x results in a game less than or equal to moving Right in y.

More concisely: For pre-games x and y, x ≤ y if and only if, for every move i by the Left player in x and every move j by the Right player in y, there exist corresponding moves with x ≤ moving Left after moving i in y and moving j in x ≤ moving Right in y.

SetTheory.PGame.lf_iff_exists_le

theorem SetTheory.PGame.lf_iff_exists_le : ∀ {x y : SetTheory.PGame}, x.LF y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

The theorem `SetTheory.PGame.lf_iff_exists_le` provides a definition of the less or fuzzy (⧏) relation on pre-games. This definition is expressed in terms of the less than or equal to (≤) relation. Specifically, for any two pre-games `x` and `y`, `x` is less or fuzzy to `y` if and only if there exists a move `i` by Left such that `x` is less than or equal to the game resulting from making move `i` in `y`, or there exists a move `j` by Right such that the game resulting from making move `j` in `x` is less than or equal to `y`.

More concisely: For any pre-games x and y, x is less or fuzzy (⧏) to y if and only if there exists i (Left move) such that x ≤ y\_{i}, or there exists j (Right move) such that y\_{j} ≤ x.

LE.le.moveLeft_lf

theorem LE.le.moveLeft_lf : ∀ {x y : SetTheory.PGame}, x ≤ y → ∀ (i : x.LeftMoves), (x.moveLeft i).LF y

This theorem, `LE.le.moveLeft_lf`, in the context of the Set Theory of Games, asserts that for any two games `x` and `y` such that `x` is less than or equal to `y`, for every possible left move `i` in `x`, the state of the game `x` after the left move `i` (represented as `(x.moveLeft i)`) is a legal position (`LF`) for `y`.

More concisely: For all games x that are less than or equal to y, and for all left moves i in x, the state of x after the left move i is a legal position for y.

SetTheory.PGame.Relabelling.le

theorem SetTheory.PGame.Relabelling.le : ∀ {x y : SetTheory.PGame}, x.Relabelling y → x ≤ y

This theorem states that for any two "Games" `x` and `y` in Set Theory, if there is a 'Relabelling' from `x` to `y`, then `x` is less than or equal to `y`. Here, `SetTheory.PGame` refers to games in the context of Set Theory and `SetTheory.PGame.Relabelling` is a relation that represents a renaming of the positions of a game.

More concisely: For any two Set Theory games `x` and `y`, if there exists a relabelling from `x` to `y` in Set Theory, then `x` is less than or equal to `y` in the game lattice.

SetTheory.PGame.Subsequent.moveLeft

theorem SetTheory.PGame.Subsequent.moveLeft : ∀ {x : SetTheory.PGame} (i : x.LeftMoves), (x.moveLeft i).Subsequent x

This theorem states that for any game `x` in set theory and any allowable move `i` by the Left player in that game, the game that results after the Left player makes move `i` is 'Subsequent' to the original game `x`. In other words, the new game can be obtained from the original game `x` by playing some nonempty sequence of moves. This sequence in our case is just the single move `i` by the Left player.

More concisely: For any game `x` and allowable move `i` by the Left player, the game obtained by making move `i` is a subsequence of the original game `x`. (Note: In Lean, this would be expressed as a definition or proposition stating that the relation of being a subsequence holds between the games.)

SetTheory.PGame.lf_of_lt

theorem SetTheory.PGame.lf_of_lt : ∀ {x y : SetTheory.PGame}, x < y → x.LF y

This theorem states that for any two pre-games `x` and `y` in set theory, if `x` is less than `y` (`x < y`), then the less or fuzzy (`LF`) relation holds between `x` and `y`. In game theory terms, 'less or fuzzy' means that the second player cannot win the game. So, this theorem says that if `x` is a game in which Left has a winning strategy, then it is not true that `y` is a game in which Right has a winning strategy; or in other words, Left can win the game `y` as the first player.

More concisely: In set theory, if `x` is strictly less than `y`, then `x` does not have a winning strategy for the less or fuzzy relation (i.e., the second player has a winning strategy for game `y`).

SetTheory.PGame.mk_le_mk

theorem SetTheory.PGame.mk_le_mk : ∀ {xl xr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yl yr : Type u_1} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame}, SetTheory.PGame.mk xl xr xL xR ≤ SetTheory.PGame.mk yl yr yL yR ↔ (∀ (i : xl), (xL i).LF (SetTheory.PGame.mk yl yr yL yR)) ∧ ∀ (j : yr), (SetTheory.PGame.mk xl xr xL xR).LF (yR j)

This theorem defines the concept of less than or equal to (`≤`) for pre-games in set theory, specifically those constructed using the `SetTheory.PGame.mk` constructor. According to the theorem, a pre-game `SetTheory.PGame.mk xl xr xL xR` is less than or equal to another pre-game `SetTheory.PGame.mk yl yr yL yR` if and only if for every option `i` in `xl`, the left option of the first pre-game is less than or equal to the second pre-game, and for every option `j` in `yr`, the first pre-game is less than or equal to the right option of the second pre-game.

More concisely: For pre-games `xl xr xL xR` and `yl yr yL yR` in set theory constructed using `SetTheory.PGame.mk`, `xl ≤ yl ⊎ xr ≤ yR` if and only if for all `i ∈ xl`, `xL i ≤ yl` and for all `j ∈ yr`, `xl ≤ yR i`.

SetTheory.PGame.lf_zero

theorem SetTheory.PGame.lf_zero : ∀ {x : SetTheory.PGame}, x.LF 0 ↔ ∃ j, ∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF 0 := by sorry

This theorem in set theory and game theory is about pre-games. It states that for any pre-game `x`, `x` looking forward (LF) to a 0 game is equivalent to the existence of a right move `j` of `x` such that for all left moves `i` of the resulting game after moving right, the resulting game after moving left looks forward to a 0 game. In other words, `x` has a winning strategy if there exists a move for `x` such that no matter what the opponent does next, `x` can still force a win.

More concisely: For any pre-game x, x has a winning strategy if and only if there exists a move j of x such that the resulting game after moving right j has the property that for all left moves i of the opponent, the resulting game after moving left i is a 0 game.

SetTheory.PGame.mk_lf_mk

theorem SetTheory.PGame.mk_lf_mk : ∀ {xl xr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yl yr : Type u_1} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame}, (SetTheory.PGame.mk xl xr xL xR).LF (SetTheory.PGame.mk yl yr yL yR) ↔ (∃ i, SetTheory.PGame.mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ SetTheory.PGame.mk yl yr yL yR

This theorem in Set Theory pertains to pre-games and establishes a relationship between the "left-first" (`LF`) ordering on games. Specifically, it states that for any pre-games constructed using the `SetTheory.PGame.mk` constructor, the game `SetTheory.PGame.mk xl xr xL xR` is left-first (`LF`) of the game `SetTheory.PGame.mk yl yr yL yR` if and only if there exists an index `i` such that game `SetTheory.PGame.mk xl xr xL xR` is less than or equal to the left move `yL i` of the second game, or there exists an index `j` such that the right move `xR j` of the first game is less than or equal to the game `SetTheory.PGame.mk yl yr yL yR`.

More concisely: For any pre-games constructed using `SetTheory.PGame.mk`, the first game is left-first with respect to the second if and only if there exists an index in the first game's left sequence that is less than or equal to some move in the second game's left sequence, or there exists an index in the first game's right sequence that is less than or equal to the second game.

SetTheory.PGame.neg_le_neg_iff

theorem SetTheory.PGame.neg_le_neg_iff : ∀ {x y : SetTheory.PGame}, -y ≤ -x ↔ x ≤ y

This theorem states that for any two games 'x' and 'y' in set theory, the negation of 'y' is less than or equal to the negation of 'x' if and only if 'x' is less than or equal to 'y'. This theorem demonstrates an important property of negation that can be found in many mathematical structures, not just games in set theory.

More concisely: For any games x and y in set theory, x ≤ y if and only if �� /******/x/��\] ≤ �� /******/y/��\] in the lattice of sets under inclusion. (Note: The notation �� /******/x/��\] and �� /******/y/��\] represent the negations of sets x and y, respectively.)

SetTheory.PGame.LF.trans_le

theorem SetTheory.PGame.LF.trans_le : ∀ {x y z : SetTheory.PGame}, x.LF y → y ≤ z → x.LF z

This theorem, `SetTheory.PGame.LF.trans_le`, states that for any three games `x`, `y`, and `z` in the domain of set-theoretic games (a branch of mathematical logic), if `x` is less than or equal from `y` in the lexicographically first order (`x.LF y`) and `y` is less than or equal to `z` (`y ≤ z`), then `x` is also less than or equal from `z` in the lexicographically first order (`x.LF z`). Essentially, it is a transitivity property pertaining to set-theoretic games.

More concisely: If `x ≤ y` and `y ≤ z` in the lexicographically first order of set-theoretic games, then `x ≤ z`.

SetTheory.PGame.neg_equiv_neg_iff

theorem SetTheory.PGame.neg_equiv_neg_iff : ∀ {x y : SetTheory.PGame}, -x ≈ -y ↔ x ≈ y

This theorem states that for any two games `x` and `y` in set theory, the game resulting from negating `x` is equivalent to the game resulting from negating `y` if and only if `x` is equivalent to `y`. In other words, the negation operation on games preserves equivalence.

More concisely: For all games x and y in set theory, x ��IVE y if and only if ∨x ��IVE ∨y, where ��IVE denotes game equivalence and ∨ denotes the negation of a game.

SetTheory.PGame.leftResponse_spec

theorem SetTheory.PGame.leftResponse_spec : ∀ {x : SetTheory.PGame} (h : 0 ≤ x) (j : x.RightMoves), 0 ≤ (x.moveRight j).moveLeft (SetTheory.PGame.leftResponse h j)

This theorem, `SetTheory.PGame.leftResponse_spec`, shows that given a game `x` in set theory, if the left player can win when playing second (0 ≤ x), then for any move `j` by the right player, the resulting game after the left player responds using the strategy defined by `leftResponse` still satisfies the condition that the left player can win when playing second. In other words, the `leftResponse` strategy ensures that the left player maintains the winning condition irrespective of the move made by the right player.

More concisely: Given a game `x` in set theory and a move `j` by the right player, if the left player can win `x` when playing second, then the resulting game after the left player responds using the strategy `leftResponse` also allows the left player to win.

SetTheory.PGame.not_fuzzy_of_le

theorem SetTheory.PGame.not_fuzzy_of_le : ∀ {x y : SetTheory.PGame}, x ≤ y → ¬x.Fuzzy y

This theorem states that for any two pre-games `x` and `y` in set theory, if `x` is less than or equal to `y`, then we can say that `x` and `y` are not in a fuzzy relationship. In other words, if the first player has a strategy to either win or draw playing `x` against `y`, then it is not the case that the first player has a strategy to win regardless of whether they are playing `x` or `y`.

More concisely: If `x` is less than or equal to `y` in set theory, then there does not exist a strategy for the first player to win consistently against both `x` and `y`.

SetTheory.PGame.lf_iff_lt_or_fuzzy

theorem SetTheory.PGame.lf_iff_lt_or_fuzzy : ∀ {x y : SetTheory.PGame}, x.LF y ↔ x < y ∨ x.Fuzzy y

This theorem in the context of Set Theory and Pregames states that for any two pre-games `x` and `y`, the "less or fuzzy" relation `LF` holds between `x` and `y` if and only if `x` is strictly less than `y` or `x` and `y` are in a fuzzy (or confused or incomparable) relation. In game-theoretic terms, this means that Left can win `x` as the first player if and only if `x` is a position that is strictly worse for Left than `y`, or neither player has a winning strategy in the comparison of `x` and `y` (i.e., the games `x` and `y` are fuzzy relative to each other).

More concisely: For any pre-games x and y in Set Theory and Pregames, x is less or fuzzy related to y if and only if Left does not have a winning strategy in x against Right's best response, and x is not strictly better than y for Left.

SetTheory.PGame.moveLeft_lf

theorem SetTheory.PGame.moveLeft_lf : ∀ {x : SetTheory.PGame} (i : x.LeftMoves), (x.moveLeft i).LF x

This theorem from set theory's game theory, `SetTheory.PGame.moveLeft_lf`, states that for any pre-game `x` and any allowable move `i` by the Left player in `x`, the post-move game (obtained by applying `SetTheory.PGame.moveLeft` to `x` and `i`) is less fuzzy than the original game `x`. In other words, after Left makes an allowable move `i` in a pre-game `x`, Left can win the resulting game as the first player.

More concisely: For any pre-game `x` and allowable move `i` by the Left player, the post-move game obtained by applying `moveLeft` is a Left-winning game.

SetTheory.PGame.le_congr

theorem SetTheory.PGame.le_congr : ∀ {x₁ y₁ x₂ y₂ : SetTheory.PGame}, x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ≤ y₁ ↔ x₂ ≤ y₂) := by sorry

This theorem, `SetTheory.PGame.le_congr`, states that for any four games `x₁`, `y₁`, `x₂`, and `y₂` from the set theory of games, if game `x₁` is equivalent to game `x₂` and game `y₁` is equivalent to game `y₂`, then game `x₁` is less than or equal to game `y₁` if and only if game `x₂` is less than or equal to game `y₂`. This implies that the relative order of games is preserved under equivalence.

More concisely: For all games x₁, y₁, x₂, and y₂, if x₁ ≈ x₂ and y₁ ≈ y₂ then x₁ ≤ y₁ if and only if x₂ ≤ y₂, where ≈ denotes equivalence in the set theory of games.

SetTheory.PGame.zero_lf_le

theorem SetTheory.PGame.zero_lf_le : ∀ {x : SetTheory.PGame}, SetTheory.PGame.LF 0 x ↔ ∃ i, 0 ≤ x.moveLeft i

This theorem explains the definition of the "less or fuzzy" relation (`0 ⧏ x`) on pre-games in the context of the "less or equal" (`0 ≤`) relationship. It states the following: for any pre-game `x`, the relation `0 ⧏ x` holds if and only if there exists some left move `i` such that after Left makes that move, the game `x` is in a state where it is "less or equal" to `0`. In other words, it implies that Left can make a winning move by placing the game in a state where they have at least as good of a position as having no moves to make.

More concisely: The "less or fuzzy" relation `0 ⧏ x` holds for a pre-game `x` if and only if there exists a Left move leading to a game state where `0 ≤ x`.

SetTheory.PGame.lf_def

theorem SetTheory.PGame.lf_def : ∀ {x y : SetTheory.PGame}, x.LF y ↔ (∃ i, (∀ (i' : x.LeftMoves), (x.moveLeft i').LF (y.moveLeft i)) ∧ ∀ (j : (y.moveLeft i).RightMoves), x.LF ((y.moveLeft i).moveRight j)) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF y) ∧ ∀ (j' : y.RightMoves), (x.moveRight j).LF (y.moveRight j')

This theorem defines the "less or fuzzy" (⧏) relation between two pre-games, `x` and `y`. According to this definition, `x` is less or fuzzy to `y` if and only if one of two conditions is met: first, there exists a move for Left in `y` such that for all moves for Left in `x`, the game state after Left's move in `x` is less or fuzzy to the game state after Left's move in `y`, and for all moves for Right in the game state after Left's move in `y`, `x` is less or fuzzy to the game resulting after Right's move; or secondly, there exists a move for Right in `x` such that for all moves for Left in the game state after Right's move in `x`, the game state after Left's move is less or fuzzy to `y`, and for all moves for Right in `y`, the game state after Right's move in `x` is less or fuzzy to the game state after Right's move in `y`.

More concisely: For pre-games x and y, x is less or fuzzy to y if and only if there exists a move for Left in y such that the sub-game starting from the resulting state in y is less or fuzzy to the sub-game starting from the corresponding move in x, and the reverse holds for a move for Right.

SetTheory.PGame.lf_zero_le

theorem SetTheory.PGame.lf_zero_le : ∀ {x : SetTheory.PGame}, x.LF 0 ↔ ∃ j, x.moveRight j ≤ 0

This theorem defines the left-favoring zero (`x ⧏ 0`) on pre-games in terms of less than or equal to zero (`≤ 0`). Specifically, it states that for any pre-game `x`, `x` left-favors zero if and only if there exists a move `j` to the right such that the resulting pre-game after making that move is less than or equal to zero.

More concisely: A pre-game x left-favors zero if and only if there exists a move to the right resulting in a pre-game less than or equal to zero.

LT.lt.lf

theorem LT.lt.lf : ∀ {x y : SetTheory.PGame}, x < y → x.LF y

This theorem, known as an alias of `SetTheory.PGame.lf_of_lt`, states that for any two pre-games `x` and `y` from set theory, if `x` is less than `y`, then the less or fuzzy relation `SetTheory.PGame.LF` holds between `x` and `y`. In other words, if `x` is a losing position for the first player, then Left can win the game `y` as the first player.

More concisely: For any pre-games x and y in set theory, if x is less than y then there exists a winning strategy for the first player in game y starting from position x.