grundyValue_add — Mathlib

English

For impartial G and H, the Grundy value of their sum equals the nimber sum of their Grundy values.

Русский

Для непредвзятых G и H значение Гранди их суммы равно Nim-сложению значений Гранди G и H.

LaTeX

$$$\\\\operatorname{grundyValue}(G + H) = \\\\operatorname{grundyValue}(G) + \\\\operatorname{grundyValue}(H).$$$

Lean4

@[simp]
theorem grundyValue_add (G H : PGame) [G.Impartial] [H.Impartial] :
    grundyValue (G + H) = grundyValue G + grundyValue H :=
  by
  rw [← (grundyValue G).toOrdinal_toNimber, ← (grundyValue H).toOrdinal_toNimber, ← grundyValue_nim_add_nim,
    grundyValue_eq_iff_equiv]
  exact add_congr (equiv_nim_grundyValue G) (equiv_nim_grundyValue H)

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