SetTheory.PGame.powHalf_moveLeft
theorem SetTheory.PGame.powHalf_moveLeft :
∀ (n : ℕ) (i : (SetTheory.PGame.powHalf n).LeftMoves), (SetTheory.PGame.powHalf n).moveLeft i = 0
This theorem from set theory, in the context of combinatorial game theory, states that for any natural number `n` and any valid move `i` for the Left player in the game `SetTheory.PGame.powHalf n`, the game that results after the Left player makes move `i` is the zero game. In other words, no matter what move the Left player makes in the game `SetTheory.PGame.powHalf n`, the resulting game is equivalent to the game where no moves are possible, which is denoted as `0` in game theory.
More concisely: For all natural numbers `n` and valid moves `i` for the Left player in the game `SetTheory.PGame.powHalf n`, the resulting game is the zero game.
|
SetTheory.PGame.powHalf_succ_lt_powHalf
theorem SetTheory.PGame.powHalf_succ_lt_powHalf :
∀ (n : ℕ), SetTheory.PGame.powHalf (n + 1) < SetTheory.PGame.powHalf n
This theorem states that for every non-negative integer 'n', the 'n+1'-th power of one half is less than the 'n'-th power of one half in the context of set theory games. In other words, it's an assertion about the monotonically decreasing nature of the function f(x)=0.5^x in the domain of non-negative integers.
More concisely: For all non-negative integers n, 0.5^(n+1) < 0.5^n.
|
SetTheory.PGame.numeric_powHalf
theorem SetTheory.PGame.numeric_powHalf : ∀ (n : ℕ), (SetTheory.PGame.powHalf n).Numeric
This theorem states that for every natural number `n`, the pre-game denoted as `powHalf n` is numeric. In the context of Set Theory and Game Theory, a numeric game is one that can be assigned a specific numerical value. Here, `powHalf n` represents a game corresponding to a power of `1/2`, and the theorem confirms that each of these games is indeed numeric.
More concisely: For every natural number n, the power of 1/2 game powHalf n is a numeric value.
|