English
Define a recursive fix-point operator for a well-founded Prod.GameAdd relation, generalizing lexicographic recursion.
Русский
Определим рекурсивную операцию фикса для хорошо основанной связи Prod.GameAdd, обобщающую лексикографную рекурсию.
LaTeX
$$$\\text{Fix}_{Prod.GameAdd} : (IH) \\Rightarrow \\text{C}$$$
Lean4
/-- Recursion on the well-founded `Prod.GameAdd` relation.
Note that it's strictly more general to recurse on the lexicographic order instead. -/
def fix {C : α → β → Sort*} (hα : WellFounded rα) (hβ : WellFounded rβ)
(IH : ∀ a₁ b₁, (∀ a₂ b₂, GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α) (b : β) : C a b :=
@WellFounded.fix (α × β) (fun x => C x.1 x.2) _ (hα.prod_gameAdd hβ)
(fun ⟨x₁, x₂⟩ IH' => IH x₁ x₂ fun a' b' => IH' ⟨a', b'⟩) ⟨a, b⟩
