moveLeft_neg

Mathlib.SetTheory.PGame.Algebra

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

English

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

Русский

Для любого x и индекса i, (-x).moveLeft(i) равно - x.moveRight(toLeftMovesNeg.symm(i)).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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