SetTheory.PGame.mul_assoc_equiv
theorem SetTheory.PGame.mul_assoc_equiv : ∀ (x y z : SetTheory.PGame), x * y * z ≈ x * (y * z)
This theorem states that for any three elements `x`, `y`, and `z` of the type `SetTheory.PGame`, the operation of multiplication is associative. That is, the product of `x`, `y`, and `z`, when grouped as `x * y * z`, is equivalent to the product when grouped as `x * (y * z)`. This is a fundamental property in many mathematical systems, ensuring that the way in which calculations are grouped does not affect the final outcome.
More concisely: For all `x`, `y`, and `z` in `SetTheory.PGame`, `x * (y * z)` equals `(x * y) * z`.
|
SetTheory.PGame.zero_mul_equiv
theorem SetTheory.PGame.zero_mul_equiv : ∀ (x : SetTheory.PGame), 0 * x ≈ 0
This theorem states that, in set theory games, the multiplication of 0 with any game `x` is equivalent to 0. In other words, for any instance of a set theory game, the product of 0 and that game is always indistinguishable from 0.
More concisely: For any set theory game `x`, the product of 0 and `x` is equal to 0.
|
SetTheory.PGame.quot_left_distrib
theorem SetTheory.PGame.quot_left_distrib : ∀ (x y z : SetTheory.PGame), ⟦x * (y + z)⟧ = ⟦x * y⟧ + ⟦x * z⟧
This theorem states that for any three elements `x`, `y`, and `z` in Set Theory's PGame, the game equivalence of `x` multiplied by the game sum of `y` and `z` is equal to the game sum of the game equivalence of `x` multiplied by `y` and the game equivalence of `x` multiplied by `z`. In other words, it asserts the left-distributive property of multiplication over addition within the context of surreal number games.
More concisely: For any elements `x`, `y`, and `z` in Set Theory's PGame, the game equivalence of `x` × (`y` ⊕ `z`) is equal to (`x` ⊕ₗ `y`) × `z` + (`x` ⊕ₗ `z`), where × denotes multiplication and ⊕ denotes addition in the context of surreal number games.
|
SetTheory.Game.PGame.equiv_iff_game_eq
theorem SetTheory.Game.PGame.equiv_iff_game_eq : ∀ {x y : SetTheory.PGame}, x ≈ y ↔ ⟦x⟧ = ⟦y⟧
This theorem states that for any two pre-games `x` and `y` in the domain of Set Theory, `x` is equivalent to `y` if and only if the game equivalence classes of `x` and `y` are equal. In other words, two pre-games are considered equivalent if they belong to the same equivalence class under the game equivalence relation.
More concisely: Two pre-games in Set Theory are equal if and only if their game equivalence classes are equal.
|
SetTheory.PGame.right_distrib_equiv
theorem SetTheory.PGame.right_distrib_equiv : ∀ (x y z : SetTheory.PGame), (x + y) * z ≈ x * z + y * z
The theorem `SetTheory.PGame.right_distrib_equiv` states that for all `x`, `y`, and `z` in the class of Games (`SetTheory.PGame`), the algebraic property of right distributivity holds. That is, multiplying `z` by the sum of `x` and `y` (`(x + y) * z`) is equivalent to the sum of `z` multiplied by `x` and `z` multiplied by `y` (`x * z + y * z`), where equivalence (`≈`) is defined in the context of games. This theorem is a formalization of the distributive law from basic arithmetic in the setting of combinatorial game theory.
More concisely: For all games x, y, and z, the operation of multiplying a game by the sum of two other games is equivalent to the sum of the individual multiplications in the context of combinatorial game theory. (SetTheory.PGame.right_distrib_equiv)
|
SetTheory.PGame.mul_comm_equiv
theorem SetTheory.PGame.mul_comm_equiv : ∀ (x y : SetTheory.PGame), x * y ≈ y * x
This theorem states that for any two elements `x` and `y` of the type `SetTheory.PGame`, the result of multiplying `x` by `y` is equivalent to the result of multiplying `y` by `x`. This is a formalization of the commutative property of multiplication in the context of games in set theory.
More concisely: For all `x` and `y` in `SetTheory.PGame`, `x * y = y * x`.
|
SetTheory.PGame.mul_zero_equiv
theorem SetTheory.PGame.mul_zero_equiv : ∀ (x : SetTheory.PGame), x * 0 ≈ 0
This theorem states that for any given surreal number `x` from the theory of games, the product of `x` and zero is equivalent to zero. In mathematical terms, this would be expressed as `x * 0 ≈ 0`. This follows the general mathematical principle that any number multiplied by zero is zero.
More concisely: The theorem asserts that the product of a surreal number `x` and zero is equal to zero: `x * 0 = 0`.
|
SetTheory.PGame.mul_one_equiv
theorem SetTheory.PGame.mul_one_equiv : ∀ (x : SetTheory.PGame), x * 1 ≈ x
This theorem states that for any element `x` of the type `SetTheory.PGame` (which stands for games in set theory), the product of `x` and `1` is equivalent to `x` itself. In mathematical terms, it realizes the multiplicative identity property in the context of games in set theory, i.e., multiplying any game by one leaves the game unchanged.
More concisely: For any game `x` in set theory, `x * 1` equals `x`.
|
SetTheory.Game.not_lf
theorem SetTheory.Game.not_lf : ∀ {x y : SetTheory.Game}, ¬x.LF y ↔ y ≤ x
This theorem, named `SetTheory.Game.not_lf`, states that for any two games `x` and `y` from the Game set theory, the statement that `x` is not left-first with respect to `y` is equivalent to stating that `y` is less than or equal to `x`. Here, 'left-first' refers to the property of a game where the left option is played first. In other words, the theorem establishes a relationship between the absence of the 'left-first' property and the inequality between two games in Set Theory.
More concisely: For any games x and y, x not being left-first with respect to y is equivalent to y being less than or equal to x.
|
SetTheory.PGame.left_distrib_equiv
theorem SetTheory.PGame.left_distrib_equiv : ∀ (x y z : SetTheory.PGame), x * (y + z) ≈ x * y + x * z
This theorem states that for any three games `x`, `y`, and `z` in set theoretic game theory, the distributive property holds: multiplying `x` with the sum of `y` and `z` is equivalent to the sum of `x` multiplied by `y` and `x` multiplied by `z`. This is a game-theoretic version of the standard distributive law in arithmetic: `x * (y + z) = x * y + x * z`.
More concisely: For any games x, y, and z in set theoretic game theory, x \* (y + z) = x \* y + x \* z.
|
SetTheory.PGame.one_mul_equiv
theorem SetTheory.PGame.one_mul_equiv : ∀ (x : SetTheory.PGame), 1 * x ≈ x
This theorem states that for any element `x` of the type `SetTheory.PGame`, multiplying `x` by `1` is equivalent to `x` itself. Here, the `≈` symbol denotes the equivalence relation in the context of games in set theory. So, in more informal terms, the theorem is saying that in the game theory, multiplying any game by one doesn't change the game.
More concisely: For any `x` in `SetTheory.PGame`, `x ≈ x * 1` holds in the equivalence relation `≈` of Set Theory game theory.
|
SetTheory.Game.not_le
theorem SetTheory.Game.not_le : ∀ {x y : SetTheory.Game}, ¬x ≤ y ↔ y.LF x
This theorem is about the structure `SetTheory.Game` in Lean 4. It states that for any two instances `x` and `y` of `SetTheory.Game`, the negation of the statement "x is less than or equal to y" is equivalent to the application of the `LF` function on `y` and `x`. In other words, `x` is not less than or equal to `y` if and only if `y.LF x` holds. This is done to simplify inequalities in game theory and minimize the use of negations.
More concisely: For any `SetTheory.Game` instances `x` and `y` in Lean 4, `~(x ≤ y)` is equivalent to `y.LF x`.
|