gameAdd_swap_swap — Mathlib

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]

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