exists_grundyValue_moveLeft_of_lt

English

If for all left moves, GrundyValue(G.moveLeft i) ≠ o, then GrundyValue(G) ≤ o.

Русский

Если для всех левый ходов GrundyValue(G.moveLeft i) ≠ o, тогда GrundyValue(G) ≤ o.

LaTeX

$$$ \forall i, \operatorname{grundyValue}(G.moveLeft(i)) \neq o \;\Longrightarrow\; \operatorname{grundyValue}(G) \le o. $$$

Lean4

theorem exists_grundyValue_moveLeft_of_lt {G : PGame} {o : Nimber} (h : o < grundyValue G) :
    ∃ i, grundyValue (G.moveLeft i) = o :=
  by
  rw [grundyValue_eq_sInf_moveLeft] at h
  by_contra ha
  exact h.not_ge (csInf_le' ha)

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