English
If Prod.GameAdd holds for (a1,b1) and (a2,b2), then the Sym2 lifting satisfies GameAdd for s(a1,b1) and s(a2,b2).
Русский
Если Prod.GameAdd выполняется для (a1,b1) и (a2,b2), тогда переход к Sym2 удовлетворяет GameAdd для s(a1,b1) и s(a2,b2).
LaTeX
$$$\forall a_1,a_2,b_1,b_2:\; \mathrm{Prod.GameAdd}(r_\alpha,r_\alpha)((a_1,b_1),(a_2,b_2)) \Rightarrow \mathrm{Sym2.GameAdd}(r_\alpha,\mathrm{Sym2.mk}(a_1,b_1),\mathrm{Sym2.mk}(a_2,b_2)).$$$
Lean4
theorem _root_.Prod.GameAdd.to_sym2 {a₁ a₂ b₁ b₂ : α} (h : Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) :
Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂) :=
gameAdd_mk'_iff.2 <| Or.inl <| h
