P4_neg_left

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.P4_neg_left

English

P4(x1, x2, y) holds iff P4(-x2, -x1, y) holds.

Русский

P4(x1, x2, y) эквивалентно P4(-x2, -x1, y).

LaTeX

$$$$ \mathrm{P4}(x_1,x_2,y) \iff \mathrm{P4}(-x_2,-x_1,y). $$$$

Lean4

theorem P4_neg_left : P4 x₁ x₂ y ↔ P4 (-x₂) (-x₁) y := by simp_rw [P4, PGame.neg_lt_neg_iff, moveLeft_neg, ← P3_neg]

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

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

Разделы

Аффилиация

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