swap

Mathlib.SetTheory.PGame.Order

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

English

If two games x and y are fuzzy, then the order relation is symmetric between them, i.e., x ‖ y implies y ‖ x.

Русский

Если две игры x и y неразборчивы между собой, то отношение между ними симметрично: x ‖ y ⇒ y ‖ x.

LaTeX

$$$x \|\| y \Rightarrow y \|\| x$$$

Lean4

@[symm]
theorem swap {x y : PGame} : x ‖ y → y ‖ x :=
  And.symm

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

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

Разделы

Аффилиация

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