neg_insertRight_neg

Mathlib.SetTheory.PGame.Algebra

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

← MathLib Explorer

English

(-x).insertRight(-x') = -x.insertLeft x'.

Русский

(-x).insertRight(-x') = -x.insertLeft x'.

LaTeX

$$$ (-x).insertRight(-x') = -x.insertLeft x' $$$

Lean4

theorem neg_insertRight_neg (x x' : PGame.{u}) : (-x).insertRight (-x') = -x.insertLeft x' :=
  by
  cases x
  cases x'
  dsimp [insertRight, insertLeft]
  congr! with (i | j)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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