le_grundyValue_of_Iio_subset_moveRight

English

If o is a nimber and every nimber less than o occurs as the Grundy value of some right move of G, then o ≤ Grundy(G).

Русский

Если o — nimber, и каждый nimber, меньший o, встречается как значение Гранди для некоторого правого хода G, тогда o ≤ Grundy(G).

LaTeX

$$$\\\\operatorname{Iio}(o) \\\\subseteq \\\\operatorname{range}(\\\\operatorname{grundyValue} \\\\\\circ G.moveRight) \\\\Rightarrow o \\\\le \\\\operatorname{grundyValue}(G).$$$

Lean4

theorem le_grundyValue_of_Iio_subset_moveRight {G : PGame} [G.Impartial] {o : Nimber}
    (h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)) : o ≤ grundyValue G :=
  by
  by_contra! ho
  obtain ⟨i, hi⟩ := h ho
  exact grundyValue_ne_moveRight i hi

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