neg_equiv_self

Mathlib.SetTheory.Game.Impartial

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

English

If G is impartial, then G is equivalent to its negation: G ≈ −G.

Русский

Если G непредвзята, то G эквивалентна своему отрицанию: G ≈ −G.

LaTeX

$$$G \approx -G$$$

Lean4

theorem neg_equiv_self (G : PGame) [h : G.Impartial] : G ≈ -G :=
  (impartial_def.1 h).1

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

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

Разделы

Аффилиация

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