English
Let a1,a2,b1,b2 ∈ α. Then GameAdd rα s(a1,b1) s(a2,b2) holds exactly when either Prod.GameAdd holds for (a1,b1) and (a2,b2) or for (b1,a1) and (a2,b2).
Русский
Пусть a1,a2,b1,b2 ∈ α. Тогда GameAdd rα s(a1,b1) s(a2,b2) выполняется тогда и только тогда, когда либо Prod.GameAdd для (a1,b1) и (a2,b2), либо Prod.GameAdd для (b1,a1) и (a2,b2).
LaTeX
$$$\forall a_1,a_2,b_1,b_2 \in \alpha,\; \mathrm{GameAdd}(r_\alpha,\mathrm{Sym2.mk}(a_1,b_1),\mathrm{Sym2.mk}(a_2,b_2)) \iff \mathrm{Prod.GameAdd}(r_\alpha,r_\alpha)((a_1,b_1),(a_2,b_2)) \lor \mathrm{Prod.GameAdd}(r_\alpha,r_\alpha)((b_1,a_1),(a_2,b_2)).$$$
Lean4
theorem gameAdd_mk'_iff {a₁ a₂ b₁ b₂ : α} :
GameAdd rα s(a₁, b₁) s(a₂, b₂) ↔ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) :=
Iff.rfl
