isOption_neg_neg

Mathlib.SetTheory.PGame.Algebra

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

English

IsOption(-x) (-y) holds exactly when IsOption x y holds.

Русский

IsOption(-x) (-y) эквивалентно IsOption x y.

LaTeX

$$$$ \mathrm{IsOption}(-x,-y) \iff \mathrm{IsOption}(x,y). $$$$

Lean4

@[simp]
theorem isOption_neg_neg {x y : PGame} : IsOption (-x) (-y) ↔ IsOption x y := by rw [isOption_neg, neg_neg]

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

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

Разделы

Аффилиация

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