isEmpty_nim_zero_leftMoves

Mathlib.SetTheory.Game.Nim

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

English

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

Русский

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

LaTeX

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

Lean4

instance isEmpty_nim_zero_leftMoves : IsEmpty (nim 0).LeftMoves :=
  by
  rw [nim]
  exact isEmpty_toType_zero

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

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

Разделы

Аффилиация

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