nim_grundyValue

Mathlib.SetTheory.Game.Nim

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.nim_grundyValue

English

The addition nim o1 + nim o2 is fuzzy with 0 iff o1 ≠ o2.

Русский

Сложение Nim o1 + Nim o2 неразрешимо с 0 тогда и только тогда, когда o1 ≠ o2.

LaTeX

$$$ (\mathrm{nim}(o_1) + \mathrm{nim}(o_2)) \;\|\!\!\|\; 0 \iff o_1 \neq o_2. $$$

Lean4

@[simp]
theorem nim_grundyValue (o : Ordinal.{u}) : grundyValue (nim o) = ∗o :=
  grundyValue_eq_iff_equiv_nim.2 PGame.equiv_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru