Theorems · Definition · logic and foundations

IsWellFounded.rank

{α : Type u} → (r : α → α → Prop) → [hwf : IsWellFounded α r] → α → Ordinal.{u}

The rank of an element a under a well-founded relation r is defined recursively as the smallest ordinal greater than the ranks of all elements below it (i.e. elements b such that r b a).

Defined in

Mathlib.SetTheory.Ordinal.Rank

Cited by

9 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

IsWellFounded