neg_insertLeft_neg

Mathlib.SetTheory.PGame.Algebra

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem neg_insertLeft_neg (x x' : PGame.{u}) : (-x).insertLeft (-x') = -x.insertRight x' := by
  rw [← neg_eq_iff_eq_neg, ← neg_insertRight_neg, neg_neg, neg_neg]

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

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

Разделы

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

Аффилиация

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