English
If a and b are accessible, then (a,b) is accessible under Prod.GameAdd.
Русский
Если a и b доступны по Acc, то (a,b) доступен по Prod.GameAdd.
LaTeX
$$$\\text{Acc }(a) \\land \\text{Acc }(b) \\Rightarrow \\text{Acc}_{Prod.GameAdd}(a,b)$$$
Lean4
/-- If `a` is accessible under `rα` and `b` is accessible under `rβ`, then `(a, b)` is
accessible under `Prod.GameAdd rα rβ`. Notice that `Prod.lexAccessible` requires the
stronger condition `∀ b, Acc rβ b`. -/
theorem prod_gameAdd (ha : Acc rα a) (hb : Acc rβ b) : Acc (Prod.GameAdd rα rβ) (a, b) :=
by
induction ha generalizing b with
| _ a _ iha
induction hb with
| _ b hb ihb
refine Acc.intro _ fun h => ?_
rintro (⟨ra⟩ | ⟨rb⟩)
exacts [iha _ ra (Acc.intro b hb), ihb _ rb]
