fix_eq — Mathlib

English

The fix function on Sym2.GameAdd is well-defined by WellFounded.fix with the given parameters.

Русский

Функция fix для Sym2.GameAdd задаётся корректно через WellFounded.fix с заданными параметрами.

LaTeX

$$$\mathrm{GameAdd}.fix\ hr\ IH\ a\ b = \text{WellFounded}.fix\ (\text{...})\ a b.$$$

Lean4

theorem fix_eq {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 : α) :
    GameAdd.fix hr IH a b = IH a b fun a' b' _ => GameAdd.fix hr IH a' b' :=
  WellFounded.fix_eq ..

Похожие утверждения