English
Relabelling moveLeft for a game built from state x factors through the state built by leftMovesOfState.
Русский
Ребаллинговый переход moveLeft для игры, построенной из состояния x, факторизуется через состояние, полученное через leftMovesOfState.
LaTeX
$$$\text{relabellingMoveLeft}(s,t) : \text{Relabelling}(\text{moveLeft}(\text{ofState}(s),t))\; (\text{ofState}((\text{leftMovesOfState}(s).toFun t).val))$$$
Lean4
/-- The relabelling showing `moveLeft` applied to a game constructed using `of`
has itself been constructed using `of`.
-/
def relabellingMoveLeft (s : S) (t : LeftMoves (ofState s)) :
Relabelling (moveLeft (ofState s) t) (ofState ((leftMovesOfState s).toFun t : S)) :=
by
trans
· apply relabellingMoveLeftAux
· apply ofStateAuxRelabelling
