Rank in a well-founded relation

For r a well-founded relation, IsWellFounded.rank r a is recursively defined as the least ordinal greater than the ranks of all elements below a.

Rank of an accessible value

noncomputable def Acc.rank {α : Type u} {a : α} {r : α → α → Prop} (h : 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).

theorem Acc.rank_eq {α : Type u} {a : α} {r : α → α → Prop} (h : Acc r a) : h.rank = ⨆ (b : { b : α // r b a }), Order.succ ⋯.rank

theorem Acc.rank_lt_of_rel {α : Type u} {a b : α} {r : α → α → Prop} (hb : Acc r b) (h : r a b) : ⋯.rank < hb.rank

if r a b then the rank of a is less than the rank of b.

theorem Acc.mem_range_rank_of_le {α : Type u} {a : α} {r : α → α → Prop} {o : Ordinal.{u}} (ha : Acc r a) (ho : o ≤ ha.rank) : ∃ (b : α) (hb : Acc r b), hb.rank = o

Rank in a well-founded relation

noncomputable def IsWellFounded.rank {α : Type u} (r : α → α → Prop) [hwf : IsWellFounded α r] (a : α) : 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).

theorem IsWellFounded.rank_eq {α : Type u} (r : α → α → Prop) [hwf : IsWellFounded α r] (a : α) : rank r a = ⨆ (b : { b : α // r b a }), Order.succ (rank r ↑b)

theorem IsWellFounded.rank_lt_of_rel {α : Type u} {a b : α} {r : α → α → Prop} [hwf : IsWellFounded α r] (h : r a b) : rank r a < rank r b

theorem IsWellFounded.mem_range_rank_of_le {α : Type u} {a : α} {r : α → α → Prop} [hwf : IsWellFounded α r] {o : Ordinal.{u}} (h : o ≤ rank r a) : o ∈ Set.range (rank r)

theorem WellFoundedLT.rank_strictMono {α : Type u} [Preorder α] [WellFoundedLT α] : StrictMono (IsWellFounded.rank fun (x1 x2 : α) => x1 < x2)

theorem WellFoundedGT.rank_strictAnti {α : Type u} [Preorder α] [WellFoundedGT α] : StrictAnti (IsWellFounded.rank fun (x1 x2 : α) => x1 > x2)

@[simp]

theorem IsWellFounded.rank_eq_typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : rank r = ⇑(Ordinal.typein r).toRelEmbedding