Ordinal.toPGame_add
theorem Ordinal.toPGame_add : ∀ (a b : Ordinal.{u}), a.toPGame + b.toPGame ≈ (a.nadd b).toPGame
The theorem `Ordinal.toPGame_add` states that for any two ordinals `a` and `b`, the game sum of their corresponding games (`a.toPGame + b.toPGame`) is equivalent to the game corresponding to the natural addition of the two ordinals (`(a.nadd b).toPGame`). Here, "equivalence" refers to the notion of being the same in the context of the theory of games. This theorem essentially establishes that the operation of transforming ordinals into games and performing natural addition in the ordinal realm is consistent with performing game addition in the game realm.
More concisely: For any ordinals `a` and `b`, the games `a.toPGame + b.toPGame` and `(a.nadd b).toPGame` are equivalent.
|
Ordinal.toPGame_leftMoves
theorem Ordinal.toPGame_leftMoves : ∀ (o : Ordinal.{u_1}), o.toPGame.LeftMoves = (Quotient.out o).α
The theorem `Ordinal.toPGame_leftMoves` states that for every ordinal `o`, the set of allowable moves by Left in the pre-game corresponding to `o` is equal to the underlying set of the representative of the equivalence class of `o`. In other words, the set of possible left moves in the game derived from an ordinal matches the elements of that ordinal when we apply the axiom of choice to select a representative from its equivalence class.
More concisely: The set of Left's allowable moves in the pre-game corresponding to an ordinal `o` equals the underlying set of `o`'s representative in its equivalence class under the axiom of choice.
|
Ordinal.toPGame_le
theorem Ordinal.toPGame_le : ∀ {a b : Ordinal.{u_1}}, a ≤ b → a.toPGame ≤ b.toPGame
The theorem `Ordinal.toPGame_le` states that for any two ordinals `a` and `b`, if `a` is less than or equal to `b`, then the pre-game corresponding to `a` (obtained using the `Ordinal.toPGame` function) is also less than or equal to the pre-game corresponding to `b`. This means that the function `Ordinal.toPGame`, which converts ordinals into pre-games, preserves the order of the ordinals.
More concisely: For all ordinals `a` and `b`, if `a ≤ b`, then `Ordinal.toPGame a ≤ Ordinal.toPGame b`.
|
Ordinal.toPGame_moveLeft'
theorem Ordinal.toPGame_moveLeft' :
∀ {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves),
o.toPGame.moveLeft i = (↑(Ordinal.toLeftMovesToPGame.symm i)).toPGame
The theorem `Ordinal.toPGame_moveLeft'` states that for any ordinal 'o' and any valid move 'i' for the player Left in the positional game corresponding to 'o', making the move 'i' in this game results in a game that corresponds to a smaller ordinal. Specifically, the ordinal it corresponds to is the one that the move 'i' maps to under the inverse of the function `Ordinal.toLeftMovesToPGame`, which converts ordinals less than 'o' into moves for the game corresponding to 'o'.
More concisely: For any ordinal o and valid move i for player Left in the positional game of ordinal o, making move i results in a game corresponding to an ordinal less than o.
|
Ordinal.toPGame_lf
theorem Ordinal.toPGame_lf : ∀ {a b : Ordinal.{u_1}}, a < b → a.toPGame.LF b.toPGame
This theorem states that for any two ordinals 'a' and 'b', if 'a' is less than 'b', then in the corresponding pre-games converted from these ordinals, the first player (Left) can always win the game where the pre-game corresponding to 'b' is played first. In other words, the less or fuzzy relation holds for the pre-games corresponding to 'a' and 'b'. This relation, denoted by `SetTheory.PGame.LF`, is defined such that `SetTheory.PGame.LF x y` is true if and only if the first player can win the pre-game 'y' when it is played before pre-game 'x'.
More concisely: For any ordinals 'a' and 'b' with 'a' < 'b', the first player can win the corresponding pre-games when 'b' is played before 'a'. Equivalently, the less or fuzzy relation `SetTheory.PGame.LF` holds for pre-games corresponding to 'a' and 'b'.
|