fix_eq — Mathlib

English

A lemma about equality of recursive definitions in Prod.GameAdd.

Русский

Лемма о равенстве рекурсивных определений в Prod.GameAdd.

LaTeX

$$$\\text{fix\_eq}$$$

Lean4

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

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