Documentation

Mathlib.Order.Height

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 #

Main results #

def Set.subchain {α : Type u_1} [LT α] (s : Set α) :
Set (List α)

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

Instances For
    @[simp]
    theorem Set.nil_mem_subchain {α : Type u_1} [LT α] (s : Set α) :
    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? la < b
    @[simp]
    theorem Set.singleton_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {a : α} :
    instance Set.instNonemptyElemListSubchain {α : Type u_1} [LT α] {s : Set α} :
    noncomputable def Set.chainHeight {α : Type u_1} [LT α] (s : Set α) :

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

    Instances For
      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) :
      theorem Set.le_chainHeight_TFAE {α : Type u_1} [LT α] (s : Set α) (n : ) :
      theorem Set.le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} {n : } :
      theorem Set.length_le_chainHeight_of_mem_subchain {α : Type u_1} [LT α] {s : Set α} {l : List α} (hl : l Set.subchain 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 α} :
      @[simp]
      theorem Set.chainHeight_eq_zero_iff {α : Type u_1} [LT α] {s : Set α} :
      @[simp]
      theorem Set.chainHeight_empty {α : Type u_1} [LT α] :
      @[simp]
      theorem Set.chainHeight_of_isEmpty {α : Type u_1} [LT α] {s : Set α} [IsEmpty α] :
      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 sl', 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 β) :
      theorem Set.chainHeight_le_chainHeight_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
      theorem Set.chainHeight_le_chainHeight_iff_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
      theorem Set.chainHeight_mono {α : Type u_1} [LT α] {s : Set α} {t : Set α} (h : s 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 α) :
      @[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 sa < b) :
      theorem Set.chainHeight_insert_of_forall_lt {α : Type u_1} {s : Set α} [Preorder α] (a : α) (ha : ∀ (b : α), b sb < a) :
      theorem Set.chainHeight_union_eq {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) (H : ∀ (a : α), a s∀ (b : α), b ta < b) :