nim_one_moveLeft — Mathlib

English

For Nim with value 1, every left move leads to Nim 0; i.e., all left options of Nim(1) are Nim(0).

Русский

Для Nim со значением 1 каждый левый ход приводит к Nim 0; то есть все левые варианты Nim(1) равны Nim(0).

LaTeX

$$$ \forall i \in \text{LeftMoves}(\mathrm{nim}(1)),\quad (\mathrm{nim}(1)).moveLeft(i) = \mathrm{nim}(0). $$$

Lean4

theorem nim_one_moveLeft (x) : (nim 1).moveLeft x = nim 0 := by simp

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