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

@[simp]

theorem Set.nil_mem_subchain {α : Type u_1} [LT α] (s : Set α) : [] ∈ Set.subchain s

theorem Set.cons_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {l : List α} {a : α} : a :: l ∈ Set.subchain s ↔ a ∈ s ∧ l ∈ Set.subchain s ∧ ∀ (b : α), b ∈ List.head? l → a < b

@[simp]

theorem Set.singleton_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {a : α} : [a] ∈ Set.subchain s ↔ a ∈ s

instance Set.instNonemptyElemListSubchain {α : Type u_1} [LT α] {s : Set α} : Nonempty ↑(Set.subchain s)

noncomputable def Set.chainHeight {α : Type u_1} [LT α] (s : Set α) : ℕ∞

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

theorem Set.chainHeight_eq_iSup_subtype {α : Type u_1} [LT α] (s : Set α) : Set.chainHeight s = ⨆ (l : ↑(Set.subchain s)), ↑(List.length ↑l)

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

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

theorem Set.le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} {n : ℕ} : ↑n ≤ Set.chainHeight s ↔ ∃ l, l ∈ Set.subchain s ∧ List.length l = n

theorem Set.length_le_chainHeight_of_mem_subchain {α : Type u_1} [LT α] {s : Set α} {l : List α} (hl : l ∈ Set.subchain s) : ↑(List.length l) ≤ Set.chainHeight s

theorem Set.chainHeight_eq_top_iff {α : Type u_1} [LT α] {s : Set α} : Set.chainHeight s = ⊤ ↔ ∀ (n : ℕ), ∃ l, l ∈ Set.subchain s ∧ List.length l = n

@[simp]

theorem Set.one_le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} : 1 ≤ Set.chainHeight s ↔ Set.Nonempty s

@[simp]

theorem Set.chainHeight_eq_zero_iff {α : Type u_1} [LT α] {s : Set α} : Set.chainHeight s = 0 ↔ s = ∅

@[simp]

theorem Set.chainHeight_empty {α : Type u_1} [LT α] : Set.chainHeight ∅ = 0

@[simp]

theorem Set.chainHeight_of_isEmpty {α : Type u_1} [LT α] {s : Set α} [IsEmpty α] : Set.chainHeight s = 0

theorem Set.le_chainHeight_add_nat_iff {α : Type u_1} [LT α] {s : Set α} {n : ℕ} {m : ℕ} : ↑n ≤ Set.chainHeight s + ↑m ↔ ∃ l, l ∈ Set.subchain s ∧ n ≤ List.length l + m

theorem Set.chainHeight_add_le_chainHeight_add {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) (n : ℕ) (m : ℕ) : Set.chainHeight s + ↑n ≤ Set.chainHeight t + ↑m ↔ ∀ (l : List α), l ∈ Set.subchain s → ∃ l', l' ∈ Set.subchain t ∧ List.length l + n ≤ List.length l' + m

theorem Set.chainHeight_le_chainHeight_TFAE {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) : List.TFAE [Set.chainHeight s ≤ Set.chainHeight t, ∀ (l : List α), l ∈ Set.subchain s → ∃ l', l' ∈ Set.subchain t ∧ List.length l = List.length l', ∀ (l : List α), l ∈ Set.subchain s → ∃ l', l' ∈ Set.subchain t ∧ List.length l ≤ List.length l']

theorem Set.chainHeight_le_chainHeight_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} : Set.chainHeight s ≤ Set.chainHeight t ↔ ∀ (l : List α), l ∈ Set.subchain s → ∃ l', l' ∈ Set.subchain t ∧ List.length l = List.length l'

theorem Set.chainHeight_le_chainHeight_iff_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} : Set.chainHeight s ≤ Set.chainHeight t ↔ ∀ (l : List α), l ∈ Set.subchain s → ∃ l', l' ∈ Set.subchain t ∧ List.length l ≤ List.length l'

theorem Set.chainHeight_mono {α : Type u_1} [LT α] {s : Set α} {t : Set α} (h : s ⊆ t) : Set.chainHeight s ≤ Set.chainHeight t

theorem Set.chainHeight_image {α : Type u_1} {β : Type u_2} [LT α] [LT β] (f : α → β) (hf : ∀ {x y : α}, x < y ↔ f x < f y) (s : Set α) : Set.chainHeight (f '' s) = Set.chainHeight s

@[simp]

theorem Set.chainHeight_dual {α : Type u_1} [LT α] (s : Set α) : Set.chainHeight (↑OrderDual.ofDual ⁻¹' s) = Set.chainHeight s

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

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

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

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

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

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

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

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