grundyValue_le_of_forall_moveRight

English

If for all right moves i, Grundy(G.moveRight i) ≠ o, then Grundy(G) ≤ o.

Русский

Если для всех правых ходов i выполняется Grundy(G.moveRight i) ≠ o, тогда Grundy(G) ≤ o.

LaTeX

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

Lean4

theorem grundyValue_le_of_forall_moveRight {G : PGame} [G.Impartial] {o : Nimber}
    (h : ∀ i, grundyValue (G.moveRight i) ≠ o) : G.grundyValue ≤ o :=
  by
  contrapose! h
  exact exists_grundyValue_moveRight_of_lt h

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