moveLeftSymm — Mathlib

English

If r is a relabelling between x and y, then for any i in y.LeftMoves, x.moveLeft (r.leftMovesEquiv.symm i) is Relabelling-equivalent to y.moveLeft i. This expresses the symmetry of the left-move relabelling.

Русский

Если r — релятабелирование между x и y, то для любого i из y.LeftMoves, x.moveLeft (r.leftMovesEquiv.symm i) эквивалентно через релятабелирование y.moveLeft i.

LaTeX

$$$ \\forall r : x \\equiv_r y, \\forall i : y.LeftMoves,\\ x.moveLeft (r.leftMovesEquiv.symm i) \\equiv_r y.moveLeft i. $$$

Lean4

/-- A left move of `y` is a relabelling of a left move of `x`. -/
def moveLeftSymm : ∀ (r : x ≡r y) (i : y.LeftMoves), x.moveLeft (r.leftMovesEquiv.symm i) ≡r y.moveLeft i
  | ⟨L, R, hL, hR⟩, i => by simpa using hL (L.symm i)

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