English
Swapping the coordinates in a pair preserves the GameAdd relation under swapped orders.
Русский
Замена координат в паре сохранит отношение GameAdd при смене порядка.
LaTeX
$$$\\text{GameAdd } r_β r_α (a.swap, b.swap) \\Leftrightarrow \\text{GameAdd } r_α r_β (a, b)$$$
Lean4
@[simp]
theorem gameAdd_swap_swap : ∀ a b : α × β, GameAdd rβ rα a.swap b.swap ↔ GameAdd rα rβ a b := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ =>
by rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]