relabel_moveLeft — Mathlib

English

Under relabelling, for i in x.LeftMoves, moveLeft( relabel(el,er), el.symm(i) ) equals x.moveLeft i. This shows how the indexing maps back through the equivalence.

Русский

При релятабелировании для i ∈ x.LeftMoves: moveLeft(relabel(el,er), el.symm(i)) = x.moveLeft(i).

LaTeX

$$$ moveLeft(\\mathrm{relabel}(el,er), \\mathrm{el}.^{\\mathrm{symm}}(i)) = x.moveLeft(i). $$$

Lean4

theorem relabel_moveLeft {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (i : x.LeftMoves) :
    moveLeft (relabel el er) (el.symm i) = x.moveLeft i := by simp

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