relabel_moveRight — Mathlib

English

In the relabelling, for j in x.RightMoves, moveRight( relabel el er ) (er.symm j) equals x.moveRight j. This expresses how the indexing back-maps through er.symm.

Русский

В релятабелировании для j ∈ x.RightMoves: moveRight(relabel(el,er), er.symm(j)) = x.moveRight(j).

LaTeX

$$$ moveRight(\\mathrm{relabel}(el,er), \\mathrm{er}.symm(j)) = x.moveRight(j). $$$

Lean4

theorem relabel_moveRight {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (j : x.RightMoves) :
    moveRight (relabel el er) (er.symm j) = x.moveRight j := by simp

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