order.height

# 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.
def set.subchain {α : Type u_1} [has_lt α] (s : set α) :
set (list α)

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

Equations
Instances for ↥set.subchain
theorem set.nil_mem_subchain {α : Type u_1} [has_lt α] (s : set α) :
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
@[protected, instance]
def set.subchain.nonempty {α : Type u_1} [has_lt α] {s : set α} :
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
theorem set.chain_height_eq_supr_subtype {α : Type u_1} [has_lt α] (s : set α) :
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
theorem set.le_chain_height_tfae {α : Type u_1} [has_lt α] (s : set α) (n : ) :
[, (l : list α) (H : l s.subchain), l.length = n, (l : list α) (H : l s.subchain), n l.length].tfae
theorem set.le_chain_height_iff {α : Type u_1} [has_lt α] {s : set α} {n : } :
(l : list α) (H : l s.subchain), l.length = n
theorem set.length_le_chain_height_of_mem_subchain {α : Type u_1} [has_lt α] {s : set α} {l : list α} (hl : l s.subchain) :
theorem set.chain_height_eq_top_iff {α : Type u_1} [has_lt α] {s : set α} :
(n : ), (l : list α) (H : l s.subchain), l.length = n
@[simp]
theorem set.one_le_chain_height_iff {α : Type u_1} [has_lt α] {s : set α} :
@[simp]
theorem set.chain_height_eq_zero_iff {α : Type u_1} [has_lt α] {s : set α} :
s =
@[simp]
theorem set.chain_height_empty {α : Type u_1} [has_lt α] :
@[simp]
theorem set.chain_height_of_is_empty {α : Type u_1} [has_lt α] {s : set α} [is_empty α] :
theorem set.le_chain_height_add_nat_iff {α : Type u_1} [has_lt α] {s : set α} {n m : } :
n (l : list α) (H : l s.subchain), n l.length + m
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 : ) :
(l : list α), l s.subchain ( (l' : list β) (H : l' t.subchain), l.length + n l'.length + m)
theorem set.chain_height_le_chain_height_tfae {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (s : set α) (t : set β) :
[, (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
theorem set.chain_height_le_chain_height_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {s : set α} {t : set β} :
(l : list α), l s.subchain ( (l' : list β) (H : l' t.subchain), l.length = l'.length)
theorem set.chain_height_le_chain_height_iff_le {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {s : set α} {t : set β} :
(l : list α), l s.subchain ( (l' : list β) (H : l' t.subchain), l.length l'.length)
theorem set.chain_height_mono {α : Type u_1} [has_lt α] {s t : set α} (h : s t) :
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 α) :
@[simp]
theorem set.chain_height_dual {α : Type u_1} [has_lt α] (s : set α) :
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
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
theorem set.chain_height_insert_of_forall_gt {α : Type u_1} {s : set α} [preorder α] (a : α) (hx : (b : α), b s a < b) :
=
theorem set.chain_height_insert_of_forall_lt {α : Type u_1} {s : set α} [preorder α] (a : α) (ha : (b : α), b s b < a) :
=
theorem set.chain_height_union_le {α : Type u_1} {s t : set α} [preorder α] :
theorem set.chain_height_union_eq {α : Type u_1} [preorder α] (s t : set α) (H : (a : α), a s (b : α), b t a < b) :
theorem set.well_founded_gt_of_chain_height_ne_top {α : Type u_1} [preorder α] (s : set α) (hs : s.chain_height ) :
theorem set.well_founded_lt_of_chain_height_ne_top {α : Type u_1} [preorder α] (s : set α) (hs : s.chain_height ) :