English
For Nim with parameter 1, the symmetry map on its left-moves sends every left-move to the same canonical pair (0, β) where β is a witness that 0 < 1 (the left-move set is a singleton, so the image is constant).
Русский
Для Nim с параметром 1 отображение симметрии на левых ходах отправляет каждый левый ход в одну и ту же пару вида (0, β), где β является свидетельством того, что 0 < 1 (множество левых ходов состоит из единственного элемента, поэтому образ постоянен).
LaTeX
$$$ \forall i \in \text{LeftMoves}(\mathrm{nim}(1)),\quad (\mathrm{toLeftMovesNim}(1))^{\mathrm{symm}}(i) = \langle 0, \beta \rangle \text{ with } \beta \in (0,1). $$$
Lean4
@[simp]
theorem toLeftMovesNim_one_symm (i) : (@toLeftMovesNim 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩ := by
simp [eq_iff_true_of_subsingleton]
