toRightMovesNeg — Mathlib

English

There is a canonical equivalence between x.LeftMoves and (-x).RightMoves.

Русский

Существует каноническое биективное соответствие между левыми ходами x и правыми ходами -x.

LaTeX

$$$$ x^{\mathrm{LeftMoves}} \cong (-x)^{\mathrm{RightMoves}}. $$$$

Lean4

/-- Turns a left move for `x` into a right move for `-x` and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert
between them. -/
def toRightMovesNeg {x : PGame} : x.LeftMoves ≃ (-x).RightMoves :=
  Equiv.cast (rightMoves_neg x).symm

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