relabel_moveLeft' — Mathlib

English

A simplification lemma: in the relabelled game, moving left on i equals moving left on the original game after applying the leftMovesEquiv. In symbols, moveLeft (relabel el er) i = x.moveLeft (el i).

Русский

Упрощение: в релятабелированной игре движение слева по i равно движению слева в исходной игре после применения leftMovesEquiv. Формально: moveLeft (relabel el er) i = x.moveLeft (el i).

LaTeX

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

Lean4

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

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