English
Let x and y be games and let L and R be equivalences witnessing a relabelling between y and x, with witnesses hL and hR. Then the induced right-moves equivalence of the relabelling is the inverse of R; i.e., the right-moves correspondence is given by R^{-1}.
Русский
Пусть x и y — игры, пусть L : y.LeftMoves ≃ x.LeftMoves и R : y.RightMoves ≃ x.RightMoves являются эквиваленциями, подтверждающими релятабелирование между y и x, при этом существуют доказательства hL и hR. Тогда полученное релятабелированное отображение правых ходов имеет эквивалентность, равную обратному R; то есть соответствие правых ходов задаётся через R^{-1}.
LaTeX
$$$ (\\mathrm{Relabelling.mk'}\\,L\\,R\\,h_L\\,h_R).\\mathrm{rightMovesEquiv} = R^{-1} $$$
Lean4
@[simp]
theorem mk'_rightMovesEquiv {x y L R hL hR} : (@Relabelling.mk' x y L R hL hR).rightMovesEquiv = R.symm :=
rfl
