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

• s.subchain = {l : List α | List.IsChain (fun (x1 x2 : α) => x1 < x2) l ∧ ∀ i ∈ l, i ∈ s}

@[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 ∧ ∀ b ∈ l.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

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 = ⨆ l ∈ s.subchain, ↑l.length

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) : ∃ l ∈ s.subchain, l.length = n

theorem Set.le_chainHeight_TFAE {α : Type u_1} [LT α] (s : Set α) (n : ℕ) : [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

theorem Set.le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} {n : ℕ} : ↑n ≤ s.chainHeight ↔ ∃ l ∈ s.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 : ℕ), ∃ l ∈ s.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 α} [IsEmpty α] : s.chainHeight = 0

theorem Set.le_chainHeight_add_nat_iff {α : Type u_1} [LT α] {s : Set α} {n m : ℕ} : ↑n ≤ s.chainHeight + ↑m ↔ ∃ l ∈ s.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 ↔ ∀ l ∈ s.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, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length, ∀ l ∈ s.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 ↔ ∀ l ∈ s.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 ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length

theorem Set.chainHeight_mono {α : Type u_1} [LT α] {s 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 α) [Preorder α] : s.chainHeight = ⨆ i ∈ s, (s ∩ Ici i).chainHeight

theorem Set.chainHeight_eq_iSup_Iic {α : Type u_1} (s : Set α) [Preorder α] : s.chainHeight = ⨆ i ∈ s, (s ∩ Iic i).chainHeight

theorem Set.chainHeight_insert_of_forall_gt {α : Type u_1} {s : Set α} [Preorder α] (a : α) (hx : ∀ b ∈ s, a < b) : (insert a s).chainHeight = s.chainHeight + 1

theorem Set.chainHeight_insert_of_forall_lt {α : Type u_1} {s : Set α} [Preorder α] (a : α) (ha : ∀ b ∈ s, b < a) : (insert a s).chainHeight = s.chainHeight + 1

theorem Set.chainHeight_union_le {α : Type u_1} {s t : Set α} [Preorder α] : (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight

theorem Set.chainHeight_union_eq {α : Type u_1} [Preorder α] (s t : Set α) (H : ∀ a ∈ s, ∀ b ∈ t, a < b) : (s ∪ t).chainHeight = s.chainHeight + t.chainHeight

theorem Set.wellFoundedGT_of_chainHeight_ne_top {α : Type u_1} [Preorder α] (s : Set α) (hs : s.chainHeight ≠ ⊤) : WellFoundedGT ↑s

theorem Set.wellFoundedLT_of_chainHeight_ne_top {α : Type u_1} [Preorder α] (s : Set α) (hs : s.chainHeight ≠ ⊤) : WellFoundedLT ↑s