default_nim_one_leftMoves_eq — Mathlib

English

The default left moves of nim 1 correspond to the canonical left-move bijection; in particular, nim 1 has a single left move nim 0.

Русский

У Nim 1 левый ход по умолчанию соответствует канонической биекции левых ходов; Nim 1 имеет ровно один левый ход nim 0.

LaTeX

$$$ (nim\ 1).LeftMoves = \{ nim\ 0 \}$$$

Lean4

@[simp]
theorem default_nim_one_leftMoves_eq :
    (default : (nim 1).LeftMoves) = @toLeftMovesNim 1 ⟨0, Set.mem_Iio.mpr zero_lt_one⟩ :=
  rfl

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