Theorems · Theorem · order theory

IsWellFounded.fix_eq

∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {motive : α → Sort u_1}
  (ind : (x : α) → ((y : α) → r y x → motive y) → motive x) (x : α),
  IsWellFounded.fix r ind x = ind x fun y x => IsWellFounded.fix r ind y

The value from IsWellFounded.fix is built from the previous ones as specified.

Defined in

Mathlib.Order.RelClasses

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

IsWellFounded