SetTheory.PGame.turnBound_ne_zero_of_right_move
theorem SetTheory.PGame.turnBound_ne_zero_of_right_move :
∀ {S : Type u} [inst : SetTheory.PGame.State S] {s t : S},
t ∈ SetTheory.PGame.State.r s → SetTheory.PGame.State.turnBound s ≠ 0
This theorem states that for any type 'S' that is a state in set theoretic game theory, and for any states 's' and 't' in this set, if 't' belongs to the right moves from state 's', then the turn bound of state 's' must not be zero. In other words, if there's a right move possible from a state in a positional game, then the number of turns allowed in the game from that state can't be zero.
More concisely: In set theoretic game theory, if state 's' has a successor state 't' with a right move, then the turn bound of state 's' is non-zero.
|
SetTheory.PGame.turnBound_ne_zero_of_left_move
theorem SetTheory.PGame.turnBound_ne_zero_of_left_move :
∀ {S : Type u} [inst : SetTheory.PGame.State S] {s t : S},
t ∈ SetTheory.PGame.State.l s → SetTheory.PGame.State.turnBound s ≠ 0
The theorem `SetTheory.PGame.turnBound_ne_zero_of_left_move` states that for any type `S` equipped with a structure of a game state (`SetTheory.PGame.State S`), given any two states `s` and `t` of type `S`, if `t` is a possible left move from `s` (i.e., `t` is in the set of left moves from `s`, denoted by `SetTheory.PGame.State.l s`), then the turn bound of the state `s`, given by `SetTheory.PGame.State.turnBound s`, cannot be zero. In other words, if a game state has a valid left move, then its turn bound must be non-zero.
More concisely: If `s` is a game state with a non-empty set of left moves `l s`, then the turn bound of `s` is non-zero.
|
SetTheory.PGame.ofState.proof_1
theorem SetTheory.PGame.ofState.proof_1 :
∀ {S : Type u_1} [inst : SetTheory.PGame.State S] (s : S),
SetTheory.PGame.State.turnBound s ≤ SetTheory.PGame.State.turnBound s
The theorem `SetTheory.PGame.ofState.proof_1` in Lean 4 states that for any type `S` that has an instance of structure `SetTheory.PGame.State`, and any value `s` of type `S`, the `turnBound` of `s` is less than or equal to the `turnBound` of `s` itself. In other words, it guarantees that the `turnBound` of a state in a positional game (a Set Theory Game) is always less than or equal to its own `turnBound`, which enforces the reflexive property of the less than or equal to relation on the `turnBound` of a game state.
More concisely: For any positional game state `s`, the reflexive property holds for its turn bound, that is, the turn bound of `s` is less than or equal to itself.
|
SetTheory.PGame.ofStateAux.proof_8
theorem SetTheory.PGame.ofStateAux.proof_8 :
∀ {S : Type u_1} [inst : SetTheory.PGame.State S] (n : ℕ) (s : S),
SetTheory.PGame.State.turnBound s ≤ n + 1 →
∀ (t : { t // t ∈ SetTheory.PGame.State.r s }), SetTheory.PGame.State.turnBound ↑t ≤ n
This theorem, `SetTheory.PGame.ofStateAux.proof_8`, states that for any type `S` that has a structure of a State in game theory, any natural number `n`, and any state `s` from `S`, if the turn bound of the state `s` is less than or equal to `n + 1`, then for any state `t` from the reachable states of `s`, the turn bound of `t` is less than or equal to `n`.
The turn bound of a state gives a limit on the number of turns that can be made from that state. The reachable states of a state are the states that can be reached from that state in one move. This theorem thus suggests a form of "monotonicity" of the turn bound in relation to reachable states and their turns in the context of positional games.
More concisely: For any State type `S`, natural number `n`, and states `s` and `t` in `S` with `s` reachable from `t` and turn bound of `s` less than or equal to `n+1`, the turn bound of `t` is less than or equal to `n`.
|
SetTheory.PGame.turnBound_of_left
theorem SetTheory.PGame.turnBound_of_left :
∀ {S : Type u} [inst : SetTheory.PGame.State S] {s t : S},
t ∈ SetTheory.PGame.State.l s →
∀ (n : ℕ), SetTheory.PGame.State.turnBound s ≤ n + 1 → SetTheory.PGame.State.turnBound t ≤ n
This theorem is about states in a positional game theory. It states that for any type `S` which is a state in a positional game, for any two states `s` and `t` of `S`, if state `t` is in the set of left moves from `s` (denoted by `SetTheory.PGame.State.l s`), then for any natural number `n`, if the turn bound of `s` (denoted by `SetTheory.PGame.State.turnBound s`) is less than or equal to `n + 1`, then the turn bound of `t` is less than or equal to `n`. In simple terms, it means if you can reach the state `t` by making a move from state `s`, then the turn bound of `t` is always less than or equal to the turn bound of `s` minus 1.
More concisely: For any positional game state `S`, if `t` is in the set of left moves from state `s` in `S` and the turn bound of `s` is less than or equal to `n + 1`, then the turn bound of `t` is less than or equal to `n`.
|
SetTheory.PGame.turnBound_of_right
theorem SetTheory.PGame.turnBound_of_right :
∀ {S : Type u} [inst : SetTheory.PGame.State S] {s t : S},
t ∈ SetTheory.PGame.State.r s →
∀ (n : ℕ), SetTheory.PGame.State.turnBound s ≤ n + 1 → SetTheory.PGame.State.turnBound t ≤ n
This theorem, `SetTheory.PGame.turnBound_of_right`, states that for any type `S` that has an instance of `SetTheory.PGame.State`, and for any two states `s` and `t` of `S`, if `t` is in the successor relation of `s` (denoted by `SetTheory.PGame.State.r s`), then for any natural number `n`, if the turn-bound of `s` (denoted by `SetTheory.PGame.State.turnBound s`) is less than or equal to `n + 1`, it follows that the turn-bound of `t` (denoted by `SetTheory.PGame.State.turnBound t`) is less than or equal to `n`. In plain language, this means that if you consider a game where `s` and `t` are possible states, if `t` can be reached from `s` and the turn-bound of `s` is at most `n+1`, then the turn-bound of `t` will be at most `n`. This places an upper limit on the number of turns that the game can be in state `t` after moving from state `s`.
More concisely: For any type `S` with `SetTheory.PGame.State`, if `s` and `t` are states in `S` with `t` being the successor of `s`, and the turn-bound of `s` is less than or equal to `n + 1`, then the turn-bound of `t` is less than or equal to `n`.
|
SetTheory.PGame.ofStateAux.proof_7
theorem SetTheory.PGame.ofStateAux.proof_7 :
∀ {S : Type u_1} [inst : SetTheory.PGame.State S] (n : ℕ) (s : S),
SetTheory.PGame.State.turnBound s ≤ n + 1 →
∀ (t : { t // t ∈ SetTheory.PGame.State.l s }), SetTheory.PGame.State.turnBound ↑t ≤ n
This theorem from Set Theory in the context of Partizan Games states that for any type `S` (representing a game state) that is an instance of `SetTheory.PGame.State`, any natural number `n`, and any game state `s` of type `S`, if the turn bound of `s` is less than or equal to `n + 1`, then for any `t` that is in the state `s`'s left options (`SetTheory.PGame.State.l s`), the turn bound of `t` is less than or equal to `n`. Here, the "turn bound" of a game state is a measure of how many more moves are possible from that state, and the "left options" of a game state are the potential next states reachable by the left player's moves.
More concisely: For any game state `s` of type `S` in Set Theory's `PGame.State` where `S` is an instance of `SetTheory.PGame.State`, if the turn bound of `s` is less than or equal to `n + 1`, then the turn bound of every `t` in `s.l` is less than or equal to `n`.
|