# Maximal length of chains #

This file contains lemmas to work with the maximal length of strictly descending finite sequences (chains) in a partial order.

## Main definition #

• Set.subchain: The set of strictly ascending lists of α contained in a Set α.
• Set.chainHeight: The maximal length of a strictly ascending sequence in a partial order. This is defined as the maximum of the lengths of Set.subchains, valued in ℕ∞.

## Main results #

• Set.exists_chain_of_le_chainHeight: For each n : ℕ such that n ≤ s.chainHeight, there exists s.subchain of length n.
• Set.chainHeight_mono: If s ⊆ t then s.chainHeight ≤ t.chainHeight.
• Set.chainHeight_image: If f is an order embedding, then (f '' s).chainHeight = s.chainHeight.
• Set.chainHeight_insert_of_forall_lt: If ∀ y ∈ s, y < x, then (insert x s).chainHeight = s.chainHeight + 1.
• Set.chainHeight_insert_of_forall_gt: If ∀ y ∈ s, x < y, then (insert x s).chainHeight = s.chainHeight + 1.
• Set.chainHeight_union_eq: If ∀ x ∈ s, ∀ y ∈ t, s ≤ t, then (s ∪ t).chainHeight = s.chainHeight + t.chainHeight.
• Set.wellFoundedGT_of_chainHeight_ne_top: If s has finite height, then > is well-founded on s.
• Set.wellFoundedLT_of_chainHeight_ne_top: If s has finite height, then < is well-founded on s.
def Set.subchain {α : Type u_1} [LT α] (s : Set α) :
Set (List α)

The set of strictly ascending lists of α contained in a Set α.

Equations
Instances For
@[simp]
theorem Set.nil_mem_subchain {α : Type u_1} [LT α] (s : Set α) :
[] s.subchain
theorem Set.cons_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {l : List α} {a : α} :
a :: l s.subchain a s l s.subchain bl.head?, a < b
@[simp]
theorem Set.singleton_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {a : α} :
[a] s.subchain a s
instance Set.instNonemptyElemListSubchain {α : Type u_1} [LT α] {s : Set α} :
Nonempty s.subchain
Equations
• =
noncomputable def Set.chainHeight {α : Type u_1} [LT α] (s : Set α) :

The maximal length of a strictly ascending sequence in a partial order.

Equations
• s.chainHeight = ls.subchain, l.length
Instances For
theorem Set.chainHeight_eq_iSup_subtype {α : Type u_1} [LT α] (s : Set α) :
s.chainHeight = ⨆ (l : s.subchain), (l).length
theorem Set.exists_chain_of_le_chainHeight {α : Type u_1} [LT α] (s : Set α) {n : } (hn : n s.chainHeight) :
ls.subchain, l.length = n
theorem Set.le_chainHeight_TFAE {α : Type u_1} [LT α] (s : Set α) (n : ) :
[n s.chainHeight, ls.subchain, l.length = n, ls.subchain, n l.length].TFAE
theorem Set.le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} {n : } :
n s.chainHeight ls.subchain, l.length = n
theorem Set.length_le_chainHeight_of_mem_subchain {α : Type u_1} [LT α] {s : Set α} {l : List α} (hl : l s.subchain) :
l.length s.chainHeight
theorem Set.chainHeight_eq_top_iff {α : Type u_1} [LT α] {s : Set α} :
s.chainHeight = ∀ (n : ), ls.subchain, l.length = n
@[simp]
theorem Set.one_le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} :
1 s.chainHeight s.Nonempty
@[simp]
theorem Set.chainHeight_eq_zero_iff {α : Type u_1} [LT α] {s : Set α} :
s.chainHeight = 0 s =
@[simp]
theorem Set.chainHeight_empty {α : Type u_1} [LT α] :
.chainHeight = 0
@[simp]
theorem Set.chainHeight_of_isEmpty {α : Type u_1} [LT α] {s : Set α} [] :
s.chainHeight = 0
theorem Set.le_chainHeight_add_nat_iff {α : Type u_1} [LT α] {s : Set α} {n : } {m : } :
n s.chainHeight + m ls.subchain, n l.length + m
theorem Set.chainHeight_add_le_chainHeight_add {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) (n : ) (m : ) :
s.chainHeight + n t.chainHeight + m ls.subchain, l't.subchain, l.length + n l'.length + m
theorem Set.chainHeight_le_chainHeight_TFAE {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) :
[s.chainHeight t.chainHeight, ls.subchain, l't.subchain, l.length = l'.length, ls.subchain, l't.subchain, l.length l'.length].TFAE
theorem Set.chainHeight_le_chainHeight_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
s.chainHeight t.chainHeight ls.subchain, l't.subchain, l.length = l'.length
theorem Set.chainHeight_le_chainHeight_iff_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
s.chainHeight t.chainHeight ls.subchain, l't.subchain, l.length l'.length
theorem Set.chainHeight_mono {α : Type u_1} [LT α] {s : Set α} {t : Set α} (h : s t) :
s.chainHeight t.chainHeight
theorem Set.chainHeight_image {α : Type u_1} {β : Type u_2} [LT α] [LT β] (f : αβ) (hf : ∀ {x y : α}, x < y f x < f y) (s : Set α) :
(f '' s).chainHeight = s.chainHeight
@[simp]
theorem Set.chainHeight_dual {α : Type u_1} [LT α] (s : Set α) :
(OrderDual.ofDual ⁻¹' s).chainHeight = s.chainHeight
theorem Set.chainHeight_eq_iSup_Ici {α : Type u_1} (s : Set α) [] :
s.chainHeight = is, (s ).chainHeight
theorem Set.chainHeight_eq_iSup_Iic {α : Type u_1} (s : Set α) [] :
s.chainHeight = is, (s ).chainHeight
theorem Set.chainHeight_insert_of_forall_gt {α : Type u_1} {s : Set α} [] (a : α) (hx : bs, a < b) :
(insert a s).chainHeight = s.chainHeight + 1
theorem Set.chainHeight_insert_of_forall_lt {α : Type u_1} {s : Set α} [] (a : α) (ha : bs, b < a) :
(insert a s).chainHeight = s.chainHeight + 1
theorem Set.chainHeight_union_le {α : Type u_1} {s : Set α} {t : Set α} [] :
(s t).chainHeight s.chainHeight + t.chainHeight
theorem Set.chainHeight_union_eq {α : Type u_1} [] (s : Set α) (t : Set α) (H : as, bt, a < b) :
(s t).chainHeight = s.chainHeight + t.chainHeight
theorem Set.wellFoundedGT_of_chainHeight_ne_top {α : Type u_1} [] (s : Set α) (hs : s.chainHeight ) :
theorem Set.wellFoundedLT_of_chainHeight_ne_top {α : Type u_1} [] (s : Set α) (hs : s.chainHeight ) :