English
There is an induction principle for Sym2.GameAdd: from WellFounded rα and an inductive step, we obtain C a b for all a,b.
Русский
Существует принцип индукции по Sym2.GameAdd: из WellFounded rα и индуктивного шага следует C(a,b) для всех a,b.
LaTeX
$$$\text{WellFounded } r_\alpha \to (\forall a_1 b_1, (\forall a_2 b_2, \mathrm{Sym2.GameAdd}(r_\alpha) (s(a_2,b_2)) (s(a_1,b_1)) \to C\ a_2 b_2) \to C\ a_1 b_1) \to \forall a b, C\ a b.$$$
Lean4
/-- Induction on the well-founded `Sym2.GameAdd` relation. -/
theorem induction {C : α → α → Prop} :
WellFounded rα → (∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ a b, C a b :=
GameAdd.fix
