English
A constructor for relabellings swapping the equivalences between left/right moves.
Русский
Конструктор переназначения, меняющий соответствия между левыми и правыми ходами.
LaTeX
$$$ \text{def mk' } (L : y.LeftMoves \simeq x.LeftMoves) (R : y.RightMoves \simeq x.RightMoves) (hL : \forall i, x.moveLeft (L i) \equivr y.moveLeft i) (hR : \forall j, x.moveRight (R j) \equivr y.moveRight j) : x \equivr y$$$
Lean4
/-- A constructor for relabellings swapping the equivalences. -/
def mk' (L : y.LeftMoves ≃ x.LeftMoves) (R : y.RightMoves ≃ x.RightMoves) (hL : ∀ i, x.moveLeft (L i) ≡r y.moveLeft i)
(hR : ∀ j, x.moveRight (R j) ≡r y.moveRight j) : x ≡r y :=
⟨L.symm, R.symm, fun i => by simpa using hL (L.symm i), fun j => by simpa using hR (R.symm j)⟩
