grundyValue_ne_moveRight — Mathlib

English

For any right move i of an impartial P-Game G, the Grundy value of the resulting game G.moveRight i is different from the Grundy value of G.

Русский

Для любого правого хода i в непредвзятой игре G значение Гранди получившейся игры G.moveRight i отличается от значения Гранди самой G.

LaTeX

$$$\\\\forall i: G.\\\\RightMoves, \\\\operatorname{grundyValue}(G.moveRight(i)) \\\\neq \\\\operatorname{grundyValue}(G).$$$$

Lean4

theorem grundyValue_ne_moveRight {G : PGame} [G.Impartial] (i : G.RightMoves) :
    grundyValue (G.moveRight i) ≠ grundyValue G := by
  convert grundyValue_ne_moveLeft (toLeftMovesNeg i) using 1 <;> simp

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