swap_iff

Mathlib.SetTheory.PGame.Order

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

English

For all x,y, x ‖ y is equivalent to y ‖ x.

Русский

Для любых x,y, x ‖ y эквивалентно y ‖ x.

LaTeX

$$$x \|\| y \iff y \|\| x$$$

Lean4

theorem swap_iff {x y : PGame} : x ‖ y ↔ y ‖ x :=
  ⟨Fuzzy.swap, Fuzzy.swap⟩

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

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

Разделы

Аффилиация

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