toRightMovesNim_one_symm — Mathlib

English

For Nim with parameter 1, the symmetry map on its right-moves sends every right-move to the same canonical pair (0, β) where β witness that 0 < 1 (the right-move set is a singleton, so the image is constant).

Русский

Для Nim с параметром 1 отображение симметрии на правых ходах отправляет каждый правый ход в одну и ту же пару вида (0, β), где β свидетельствует о 0 < 1 (множество правых ходов — синглтон).

LaTeX

$$$ \forall i \in \text{RightMoves}(\mathrm{nim}(1)),\quad (\mathrm{toRightMovesNim}(1))^{\mathrm{symm}}(i) = \langle 0, \beta \rangle \text{ with } \beta \in (0,1). $$$

Lean4

@[simp]
theorem toRightMovesNim_one_symm (i) : (@toRightMovesNim 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩ := by
  simp [eq_iff_true_of_subsingleton]

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