SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero'
theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero' :
∀ (G : SetTheory.PGame) [inst : G.Impartial] (H : SetTheory.PGame), G ≈ H ↔ G + H ≈ 0
This theorem states that for any impartial game `G` and any game `H` in set theory, `G` is equivalent to `H` if and only if the sum of `G` and `H` is equivalent to zero. Notably, this lemma doesn't require `H` to be impartial.
More concisely: For any impartial games G and H in set theory, G is equivalent to H if and only if G ⊕ H ≈ 0, where ⊕ denotes the sum of games and ≈ denotes game equivalence.
|
SetTheory.PGame.Impartial.fuzzy_zero_iff_lf
theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_lf :
∀ (G : SetTheory.PGame) [inst : G.Impartial], G.Fuzzy 0 ↔ G.LF 0
This theorem, in the field of set theory and game theory, states that for any impartial pre-game `G`, the pre-game `G` is fuzzy relative to the zero game if and only if the less or fuzzy relation holds between `G` and the zero game.
In this context, an impartial game is one in which the available moves and resulting positions are identical for both players, the fuzzy relation indicates that the first player can always win, and the less or fuzzy relation indicates that the Left player can win when they play first. So, essentially, the theorem is about a certain equivalence between two different win conditions in the pre-game `G`.
More concisely: For an impartial pre-game G in set theory, G is fuzzy relative to the zero game if and only if the Left player can win the less or fuzzy version of G.
|
SetTheory.PGame.impartial_def
theorem SetTheory.PGame.impartial_def :
∀ {G : SetTheory.PGame},
G.Impartial ↔
G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).Impartial) ∧ ∀ (j : G.RightMoves), (G.moveRight j).Impartial
The theorem `SetTheory.PGame.impartial_def` states that for any game `G` in set theory, `G` is impartial if and only if `G` is equivalent to the negation of `G` and for every allowable move `i` by the Left player that transitions the game to a new state, the new game is also impartial, and for every allowable move `j` by the Right player that transitions the game to a new state, the new game is also impartial. In other words, an impartial game is one where neither player has a definite advantage from the start, and every possible game state that can be reached by either player's allowable moves is also impartial.
More concisely: A game in set theory is impartial if and only if it is self-complementary and every allowable move by both players results in an impartial game.
|
SetTheory.PGame.Impartial.neg_equiv_self
theorem SetTheory.PGame.Impartial.neg_equiv_self : ∀ (G : SetTheory.PGame) [h : G.Impartial], G ≈ -G
This theorem states that for any impartial game `G` in set theory, the game `G` is equivalent to its negation `-G`. Here, an impartial game is defined as a game in which the possible moves for each player are the same, given the same position. The equivalence between `G` and `-G` is a concept in the field of combinatorial game theory where two games are considered equivalent if no matter who starts, the outcome (win, lose or draw) will be the same.
More concisely: For any impartial game G in set theory, G is equivalent to its negation -G.
|
SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero
theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero :
∀ (G : SetTheory.PGame) [inst : G.Impartial] (H : SetTheory.PGame), H ≈ G ↔ H + G ≈ 0
This theorem states that for any impartial game `G` and any other game `H` in set theory, `H` is equivalent to `G` if and only if the sum of `H` and `G` is equivalent to zero. The impartiality of `H` is not a prerequisite for this theorem.
More concisely: For any two games G and H in set theory, they are equivalent if and only if the sum of G and H is equal to the empty game.
|
SetTheory.PGame.Impartial.equiv_or_fuzzy_zero
theorem SetTheory.PGame.Impartial.equiv_or_fuzzy_zero :
∀ (G : SetTheory.PGame) [inst : G.Impartial], G ≈ 0 ∨ G.Fuzzy 0
This theorem states that in the field of set theory, for any given impartial game (represented by 'G'), one of two conditions is always true: either the game is equivalent to the zero game (meaning the first player always wins), or the game is 'fuzzy' at zero, meaning it is not distinguishable from the zero game within any finite number of moves, implying that the second player always wins. This theorem underlies the fundamental principle of impartial games.
More concisely: In set theory, every impartial game is either equivalent to the zero game or indistinguishable from it within finite moves.
|