grundyValue_eq_iff_equiv_nim — Mathlib

English

Two Nim-sums are equivalent to zero iff their Grundy values are equal; i.e., nim o1 + nim o2 ≈ 0 ⇔ o1 = o2.

Русский

Две суммы Nim эквивалентны нулю тогда и только тогда когда их значения Гранди равны; то есть Nim o1 + Nim o2 ≈ 0 ⇔ o1 = o2.

LaTeX

$$$ (\mathrm{nim}(o_1) + \mathrm{nim}(o_2) \approx 0) \iff o_1 = o_2. $$$

Lean4

theorem grundyValue_eq_iff_equiv_nim {G : PGame} [G.Impartial] {o : Nimber} :
    grundyValue G = o ↔ G ≈ nim (toOrdinal o) :=
  ⟨by rintro rfl; exact equiv_nim_grundyValue G, by intro h; rw [← nim_equiv_iff_eq];
    exact Equiv.trans (Equiv.symm (equiv_nim_grundyValue G)) h⟩

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