isEmpty_nim_zero_rightMoves

Mathlib.SetTheory.Game.Nim

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

English

The right moves of nim 0 are empty, i.e., nim 0 has no right options.

Русский

Правые ходы nim 0 пусты, то есть у nim 0 нет правых вариантов.

LaTeX

$$$ (nim\ 0).RightMoves = \varnothing $$$

Lean4

instance isEmpty_nim_zero_rightMoves : IsEmpty (nim 0).RightMoves :=
  by
  rw [nim]
  exact isEmpty_toType_zero

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

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

Разделы

Аффилиация

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