Theorems · Definition · logic and foundations

Acc.rank

{α : Type u} → {a : α} → {r : α → α → Prop} → Acc r a → Ordinal.{u}

The rank of an element a accessible under a 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

4 results in Mathlib

Foundations

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