mathlib3 documentation

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 #

Main results #

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 : ) :
[n s.chain_height, (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 : } :
n s.chain_height (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 α} :
s.chain_height = (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 α} :
@[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 s.chain_height + m (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 : ) :
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)
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
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)
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)
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 α) :
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) :