moveRight_neg

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.moveRight_neg

English

For any x and i, (-x).moveRight(i) equals - x.moveLeft(toRightMovesNeg.symm i).

Русский

Для любых x и i, (-x).moveRight(i) равно - x.moveLeft(toRightMovesNeg.symm(i)).

LaTeX

$$$$ (-x).moveRight(i) = - x.moveLeft( (\mathrm{toRightMovesNeg})^{-1}(i) ). $$$$

Lean4

@[simp]
theorem moveRight_neg {x : PGame} (i) : (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i) :=
  by
  cases x
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru