English
If G and H are impartial, then their sum G + H is impartial.
Русский
Если G и H непредвзяты, то их сумма G + H непредвзята.
LaTeX
$$$\operatorname{Impartial}(G) \land \operatorname{Impartial}(H) \Rightarrow \operatorname{Impartial}(G+H)$$$
Lean4
instance impartial_add (G H : PGame) [G.Impartial] [H.Impartial] : (G + H).Impartial :=
by
rw [impartial_def]
refine
⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _)) (Equiv.symm (negAddRelabelling _ _).equiv), fun k =>
?_, fun k => ?_⟩
· apply leftMoves_add_cases k
all_goals
intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
apply impartial_add
· apply rightMoves_add_cases k
all_goals
intro i; simp only [add_moveRight_inl, add_moveRight_inr]
apply impartial_add
termination_by (G, H)
