English
A left move of x corresponds, under a relabelling between x and y, to a relabelled left move of y. Formally, if r is a relabelling between x and y, then for every i in x.LeftMoves, x.moveLeft i is Relabelling-equivalent to y.moveLeft (r.leftMovesEquiv i).
Русский
Левый ход x соответствует через релятабелирование между x и y левому ходу y; для любого r, являющегося релятабелированием, и любого i из x.LeftMoves, x.moveLeft i эквивалентно через релятабелирование y.moveLeft (r.leftMovesEquiv i).
LaTeX
$$$ \\forall r : x \\equiv_r y, \\forall i : x.LeftMoves,\\ x.moveLeft\\ i \\equiv_r y.moveLeft (r.leftMovesEquiv i). $$$
Lean4
/-- A left move of `x` is a relabelling of a left move of `y`. -/
def moveLeft : ∀ (r : x ≡r y) (i : x.LeftMoves), x.moveLeft i ≡r y.moveLeft (r.leftMovesEquiv i)
| ⟨_, _, hL, _⟩ => hL
