neg_lf_iff

Mathlib.SetTheory.PGame.Algebra

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

English

Let x,y be P-Games. The negation preserves the LF relation: -y ⧏ x iff -x ⧏ y.

Русский

Пусть x и y — P-игры. Отрицание сохраняет LF-отношение: -y ⧏ x тогда и только тогда, когда -x ⧏ y.

LaTeX

$$$-y \u29CF x \\iff -x \u29CF y$$$

Lean4

theorem neg_lf_iff {x y : PGame} : -y ⧏ x ↔ -x ⧏ y := by rw [← neg_neg x, neg_lf_neg_iff, neg_neg]

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

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

Разделы

Аффилиация

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