English
If the set of ordinals below o is contained in the Grundy values of left options, then o ≤ Grundy(G).
Русский
Если множество ordinals ниже o содержится в значениях grundyValue у левых ходов, то o ≤ Grundy(G).
LaTeX
$$$ \text{If } \operatorname{Iio}(o) \subseteq \{ \operatorname{grundyValue}(G.moveLeft(i)) : i \in \text{LeftMoves}(G) \}, \text{ then } o \leq \operatorname{grundyValue}(G). $$$
Lean4
theorem grundyValue_ne_moveLeft {G : PGame} (i : G.LeftMoves) : grundyValue (G.moveLeft i) ≠ grundyValue G :=
by
conv_rhs => rw [grundyValue_eq_sInf_moveLeft]
have :=
csInf_mem
(nonempty_of_not_bddAbove <| Nimber.not_bddAbove_compl_of_small (Set.range fun i => grundyValue (G.moveLeft i)))
rw [Set.mem_compl_iff, Set.mem_range, not_exists] at this
exact this _
