Theorems · Theorem · order theory

Sym2.GameAdd.recursion_eq

∀ {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_3} (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 : α),
  Sym2.GameAdd.recursion hr IH a b = IH a b fun a' b' x => Sym2.GameAdd.recursion hr IH a' b'

Defined in

Mathlib.Order.GameAdd

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound