lf_zero_iff

Mathlib.SetTheory.Game.Impartial

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

English

For impartial G, G ⧏ 0 iff 0 ⧏ G.

Русский

Для непредвзятой G: G ⧏ 0 ⇔ 0 ⧏ G.

LaTeX

$$$G \bowtie 0 \iff 0 \bowtie G$$$

Lean4

theorem lf_zero_iff {G : PGame} [G.Impartial] : G ⧏ 0 ↔ 0 ⧏ G := by
  rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]

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

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

Разделы

Аффилиация

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