exists_grundyValue_moveRight_of_lt

English

If G is impartial and o < Grundy(G), then there exists a right move i with Grundy(G.moveRight i) = o.

Русский

Если G непредвзятая, и o < Grundy(G), то существует правый ход i, такой что Grundy(G.moveRight i) = o.

LaTeX

$$$\\\\text{If } o < \\\\operatorname{grundyValue}(G) \\\\text{, then } \\\\exists i: G. RightMoves, \\\\operatorname{grundyValue}(G.moveRight(i)) = o.$$$

Lean4

theorem exists_grundyValue_moveRight_of_lt {G : PGame} [G.Impartial] {o : Nimber} (h : o < grundyValue G) :
    ∃ i, grundyValue (G.moveRight i) = o := by
  rw [← grundyValue_neg] at h
  obtain ⟨i, hi⟩ := exists_grundyValue_moveLeft_of_lt h
  use toLeftMovesNeg.symm i
  rwa [← grundyValue_neg, ← moveLeft_neg]

Похожие утверждения