grundyValue_le_of_forall_moveLeft

English

Every impartial game G is equivalent to Nim of its Grundy value, i.e., G ≈ nim(toOrdinal(grundyValue G)).

Русский

Каждая беспристрастная игра G эквивалентна Nim с величиной Гранди, то есть G ≈ nim(toOrdinal(grundyValue G)).

LaTeX

$$$ G \approx nim\bigl(toOrdinal(grundyValue(G))\bigr). $$$

Lean4

theorem grundyValue_le_of_forall_moveLeft {G : PGame} {o : Nimber} (h : ∀ i, grundyValue (G.moveLeft i) ≠ o) :
    G.grundyValue ≤ o := by
  contrapose! h
  exact exists_grundyValue_moveLeft_of_lt h

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