Maximal length of chains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.chain_height: 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_chain_height: For each n : ℕ such that n ≤ s.chain_height, there exists s.subchain of length n.
set.chain_height_mono: If s ⊆ t then s.chain_height ≤ t.chain_height.
set.chain_height_image: If f is an order embedding, then (f '' s).chain_height = s.chain_height.
set.chain_height_insert_of_forall_lt: If ∀ y ∈ s, y < x, then (insert x s).chain_height = s.chain_height + 1.
set.chain_height_insert_of_lt_forall: If ∀ y ∈ s, x < y, then (insert x s).chain_height = s.chain_height + 1.
set.chain_height_union_eq: If ∀ x ∈ s, ∀ y ∈ t, s ≤ t, then (s ∪ t).chain_height = s.chain_height + t.chain_height.
set.well_founded_gt_of_chain_height_ne_top: If s has finite height, then > is well-founded on s.
set.well_founded_lt_of_chain_height_ne_top: If s has finite height, then < is well-founded on s.

source

def set.subchain {α : Type u_1} [has_lt α] (s : set α) :

set (list α)

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

Equations

s.subchain = {l : list α | list.chain' has_lt.lt l ∧ ∀ (i : α), i ∈ l → i ∈ s}

Instances for ↥set.subchain

set.subchain.nonempty

source

theorem set.nil_mem_subchain {α : Type u_1} [has_lt α] (s : set α) :

list.nil ∈ s.subchain

source

theorem set.cons_mem_subchain_iff {α : Type u_1} [has_lt α] {s : set α} {l : list α} {a : α} :

a :: l ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ (b : α), b ∈ l.head' → a < b

source

@[protected, instance]

def set.subchain.nonempty {α : Type u_1} [has_lt α] {s : set α} :

nonempty ↥(s.subchain)

source

noncomputable def set.chain_height {α : Type u_1} [has_lt α] (s : set α) :

ℕ∞

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

Equations

s.chain_height = ⨆ (l : list α) (H : l ∈ s.subchain), ↑(l.length)

source

theorem set.chain_height_eq_supr_subtype {α : Type u_1} [has_lt α] (s : set α) :

s.chain_height = ⨆ (l : ↥(s.subchain)), ↑(l.val.length)

source

theorem set.exists_chain_of_le_chain_height {α : Type u_1} [has_lt α] (s : set α) {n : ℕ} (hn : ↑n ≤ s.chain_height) :

∃ (l : list α) (H : l ∈ s.subchain), l.length = n

source

theorem set.le_chain_height_tfae {α : Type u_1} [has_lt α] (s : set α) (n : ℕ) :

[↑n ≤ s.chain_height, ∃ (l : list α) (H : l ∈ s.subchain), l.length = n, ∃ (l : list α) (H : l ∈ s.subchain), n ≤ l.length].tfae

source

theorem set.le_chain_height_iff {α : Type u_1} [has_lt α] {s : set α} {n : ℕ} :

↑n ≤ s.chain_height ↔ ∃ (l : list α) (H : l ∈ s.subchain), l.length = n

source

theorem set.length_le_chain_height_of_mem_subchain {α : Type u_1} [has_lt α] {s : set α} {l : list α} (hl : l ∈ s.subchain) :

↑(l.length) ≤ s.chain_height

source

theorem set.chain_height_eq_top_iff {α : Type u_1} [has_lt α] {s : set α} :

s.chain_height = ⊤ ↔ ∀ (n : ℕ), ∃ (l : list α) (H : l ∈ s.subchain), l.length = n

source

@[simp]

theorem set.one_le_chain_height_iff {α : Type u_1} [has_lt α] {s : set α} :

1 ≤ s.chain_height ↔ s.nonempty

source

@[simp]

theorem set.chain_height_eq_zero_iff {α : Type u_1} [has_lt α] {s : set α} :

s.chain_height = 0 ↔ s = ∅

source

@[simp]

theorem set.chain_height_empty {α : Type u_1} [has_lt α] :

∅.chain_height = 0

source

@[simp]

theorem set.chain_height_of_is_empty {α : Type u_1} [has_lt α] {s : set α} [is_empty α] :

s.chain_height = 0

source

theorem set.le_chain_height_add_nat_iff {α : Type u_1} [has_lt α] {s : set α} {n m : ℕ} :

↑n ≤ s.chain_height + ↑m ↔ ∃ (l : list α) (H : l ∈ s.subchain), n ≤ l.length + m

source

theorem set.chain_height_add_le_chain_height_add {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (s : set α) (t : set β) (n m : ℕ) :

s.chain_height + ↑n ≤ t.chain_height + ↑m ↔ ∀ (l : list α), l ∈ s.subchain → (∃ (l' : list β) (H : l' ∈ t.subchain), l.length + n ≤ l'.length + m)

source

theorem set.chain_height_le_chain_height_tfae {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (s : set α) (t : set β) :

[s.chain_height ≤ t.chain_height, ∀ (l : list α), l ∈ s.subchain → (∃ (l' : list β) (H : l' ∈ t.subchain), l.length = l'.length), ∀ (l : list α), l ∈ s.subchain → (∃ (l' : list β) (H : l' ∈ t.subchain), l.length ≤ l'.length)].tfae

source

theorem set.chain_height_le_chain_height_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {s : set α} {t : set β} :

s.chain_height ≤ t.chain_height ↔ ∀ (l : list α), l ∈ s.subchain → (∃ (l' : list β) (H : l' ∈ t.subchain), l.length = l'.length)

source

theorem set.chain_height_le_chain_height_iff_le {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {s : set α} {t : set β} :

s.chain_height ≤ t.chain_height ↔ ∀ (l : list α), l ∈ s.subchain → (∃ (l' : list β) (H : l' ∈ t.subchain), l.length ≤ l'.length)

source

theorem set.chain_height_mono {α : Type u_1} [has_lt α] {s t : set α} (h : s ⊆ t) :

s.chain_height ≤ t.chain_height

source

theorem set.chain_height_image {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (f : α → β) (hf : ∀ {x y : α}, x < y ↔ f x < f y) (s : set α) :

(f '' s).chain_height = s.chain_height

source

@[simp]

theorem set.chain_height_dual {α : Type u_1} [has_lt α] (s : set α) :

(⇑order_dual.of_dual ⁻¹' s).chain_height = s.chain_height

source

theorem set.chain_height_eq_supr_Ici {α : Type u_1} (s : set α) [preorder α] :

s.chain_height = ⨆ (i : α) (H : i ∈ s), (s ∩ set.Ici i).chain_height

source

theorem set.chain_height_eq_supr_Iic {α : Type u_1} (s : set α) [preorder α] :

s.chain_height = ⨆ (i : α) (H : i ∈ s), (s ∩ set.Iic i).chain_height

source

theorem set.chain_height_insert_of_forall_gt {α : Type u_1} {s : set α} [preorder α] (a : α) (hx : ∀ (b : α), b ∈ s → a < b) :

(has_insert.insert a s).chain_height = s.chain_height + 1

source

theorem set.chain_height_insert_of_forall_lt {α : Type u_1} {s : set α} [preorder α] (a : α) (ha : ∀ (b : α), b ∈ s → b < a) :

(has_insert.insert a s).chain_height = s.chain_height + 1

source

theorem set.chain_height_union_le {α : Type u_1} {s t : set α} [preorder α] :

(s ∪ t).chain_height ≤ s.chain_height + t.chain_height

source

theorem set.chain_height_union_eq {α : Type u_1} [preorder α] (s t : set α) (H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b) :

(s ∪ t).chain_height = s.chain_height + t.chain_height

source

theorem set.well_founded_gt_of_chain_height_ne_top {α : Type u_1} [preorder α] (s : set α) (hs : s.chain_height ≠ ⊤) :

well_founded_gt ↥s

source

theorem set.well_founded_lt_of_chain_height_ne_top {α : Type u_1} [preorder α] (s : set α) (hs : s.chain_height ≠ ⊤) :

well_founded_lt ↥s