toLeftMovesNeg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Turns a right move for `x` into a left 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 toLeftMovesNeg {x : PGame} : x.RightMoves ≃ (-x).LeftMoves :=
  Equiv.cast (leftMoves_neg x).symm

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