English
The recursion operator on Sym2.GameAdd satisfies a fixpoint equation: fix hr IH a b equals IH a b applied to the function a' b' mapped by fix hr IH a' b'.
Русский
Рекурсивный оператор на Sym2.GameAdd удовлетворяет уравнению фикса: fix hr IH a b равно IH a b применённому к функции a' b' соотнесённой через fix hr IH a' b'.
LaTeX
$$$\mathrm{Sym2.GameAdd}.fix\ hr\ IH\ a\ b = IH\ a\ b\ (\lambda a' b' .,\; \mathrm{Sym2.GameAdd}.fix\ hr\ IH\ a' b').$$$
Lean4
/-- Recursion on the well-founded `Sym2.GameAdd` relation. -/
def fix {C : α → α → Sort*} (hr : WellFounded rα)
(IH : ∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α) : C a b :=
@WellFounded.fix (α × α) (fun x => C x.1 x.2) (fun x y ↦ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y)
(by simpa [← Sym2.gameAdd_iff] using hr.sym2_gameAdd.onFun) (fun ⟨x₁, x₂⟩ IH' => IH x₁ x₂ fun a' b' => IH' ⟨a', b'⟩)
(a, b)
