le_grundyValue_of_Iio_subset_moveLeft

English

If o < GrundyValue(G), there exists a left move i such that GrundyValue(G.moveLeft i) = o.

Русский

Если o меньше GrundyValue(G), существует левый ход i, для которого GrundyValue(G.moveLeft i) = o.

LaTeX

$$$ \forall o, \; o < \operatorname{grundyValue}(G) \Rightarrow \exists i, \operatorname{grundyValue}(G.moveLeft(i)) = o. $$$

Lean4

theorem le_grundyValue_of_Iio_subset_moveLeft {G : PGame} {o : Nimber}
    (h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)) : o ≤ grundyValue G :=
  by
  by_contra! ho
  obtain ⟨i, hi⟩ := h ho
  exact grundyValue_ne_moveLeft i hi

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