moveLeft_toLeftMovesNim — Mathlib

English

Going left in nim o along the canonical bijection corresponds to nim of the index, i.e., (nim o).moveLeft (toLeftMovesNim i) = nim i.

Русский

При переходе влево в nim o вдоль канонической биекции соответствие даёт nim i.

LaTeX

$$$ \forall {o} \ (\text{toLeftMovesNim}\ i) \,:\ (nim\ o).moveLeft (\text{toLeftMovesNim } i) = nim\ i $$$

Lean4

theorem moveLeft_toLeftMovesNim {o : Ordinal} (i) : (nim o).moveLeft (toLeftMovesNim i) = nim i := by simp

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