moveLeft_neg_toLeftMovesNeg

Mathlib.SetTheory.PGame.Algebra

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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