nim_equiv_iff_eq

Mathlib.SetTheory.Game.Nim

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

← MathLib Explorer

English

Two nimbers Nim(o1) and Nim(o2) are equivalent iff o1 = o2.

Русский

Два нибера Nim(o1) и Nim(o2) эквивалентны тогда и только тогда, когда o1 = o2.

LaTeX

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

Lean4

@[simp]
theorem nim_equiv_iff_eq {o₁ o₂ : Ordinal} : (nim o₁ ≈ nim o₂) ↔ o₁ = o₂ := by
  rw [Impartial.equiv_iff_add_equiv_zero, nim_add_equiv_zero_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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