relabel_moveRight' — Mathlib

English

In the relabelled game, moveRight on j equals the original moveRight on er(j): moveRight (relabel el er) j = x.moveRight (er j).

Русский

В релятабелированной игре moveRight по j равен исходному moveRight по er(j).

LaTeX

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

Lean4

@[simp]
theorem relabel_moveRight' {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (j : xr') :
    moveRight (relabel el er) j = x.moveRight (er j) :=
  rfl

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