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).

Equations

• h.rank = Acc.recOn h fun (a : α) (_h : ∀ (y : α), r y a → Acc r y) (ih : (y : α) → r y a → Ordinal.{?u.43}) => ⨆ (b : { b : α // r b a }), Order.succ (ih ↑b ⋯)

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).

Equations

• IsWellFounded.rank r a = ⋯.rank

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

@[deprecated IsWellFounded.rank (since := "2024-09-07")]

noncomputable def WellFounded.rank {α : Type u} {r : α → α → Prop} (hwf : WellFounded r) (a : α) : Ordinal.{u}

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

Equations

• hwf.rank a = ⋯.rank

@[deprecated IsWellFounded.rank_eq (since := "2024-09-07")]

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

@[deprecated IsWellFounded.rank_lt_of_rel (since := "2024-09-07")]

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

@[deprecated WellFoundedLT.rank_strictMono (since := "2024-09-07")]

theorem WellFounded.rank_strictMono {α : Type u} [Preorder α] [WellFoundedLT α] : StrictMono ⋯.rank

@[deprecated WellFoundedGT.rank_strictAnti (since := "2024-09-07")]

theorem WellFounded.rank_strictAnti {α : Type u} [Preorder α] [WellFoundedGT α] : StrictAnti ⋯.rank