moveRight_neg_toRightMovesNeg

Mathlib.SetTheory.PGame.Algebra

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

English

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

Русский

Для любых x и i, (-x).moveRight(toRightMovesNeg(i)) = - x.moveLeft(i).

LaTeX

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

Lean4

theorem moveRight_neg_toRightMovesNeg {x : PGame} (i) : (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i := by simp

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

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

Разделы

Аффилиация

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