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

Equations
Instances For
    @[simp]
    theorem Set.nil_mem_subchain {α : Type u_1} [LT α] (s : Set α) :
    [] s.subchain
    theorem Set.cons_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {l : List α} {a : α} :
    a :: l s.subchain a s l s.subchain bl.head?, a < b
    @[simp]
    theorem Set.singleton_mem_subchain_iff {α : Type u_1} [LT α] {s : Set α} {a : α} :
    [a] s.subchain a s
    instance Set.instNonemptyElemListSubchain {α : Type u_1} [LT α] {s : Set α} :
    Nonempty s.subchain
    Equations
    • =
    noncomputable def Set.chainHeight {α : Type u_1} [LT α] (s : Set α) :

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

    Equations
    • s.chainHeight = ls.subchain, l.length
    Instances For
      theorem Set.chainHeight_eq_iSup_subtype {α : Type u_1} [LT α] (s : Set α) :
      s.chainHeight = ⨆ (l : s.subchain), (l).length
      theorem Set.exists_chain_of_le_chainHeight {α : Type u_1} [LT α] (s : Set α) {n : } (hn : n s.chainHeight) :
      ls.subchain, l.length = n
      theorem Set.le_chainHeight_TFAE {α : Type u_1} [LT α] (s : Set α) (n : ) :
      [n s.chainHeight, ls.subchain, l.length = n, ls.subchain, n l.length].TFAE
      theorem Set.le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} {n : } :
      n s.chainHeight ls.subchain, l.length = n
      theorem Set.length_le_chainHeight_of_mem_subchain {α : Type u_1} [LT α] {s : Set α} {l : List α} (hl : l s.subchain) :
      l.length s.chainHeight
      theorem Set.chainHeight_eq_top_iff {α : Type u_1} [LT α] {s : Set α} :
      s.chainHeight = ∀ (n : ), ls.subchain, l.length = n
      @[simp]
      theorem Set.one_le_chainHeight_iff {α : Type u_1} [LT α] {s : Set α} :
      1 s.chainHeight s.Nonempty
      @[simp]
      theorem Set.chainHeight_eq_zero_iff {α : Type u_1} [LT α] {s : Set α} :
      s.chainHeight = 0 s =
      @[simp]
      theorem Set.chainHeight_empty {α : Type u_1} [LT α] :
      .chainHeight = 0
      @[simp]
      theorem Set.chainHeight_of_isEmpty {α : Type u_1} [LT α] {s : Set α} [IsEmpty α] :
      s.chainHeight = 0
      theorem Set.le_chainHeight_add_nat_iff {α : Type u_1} [LT α] {s : Set α} {n : } {m : } :
      n s.chainHeight + m ls.subchain, n l.length + m
      theorem Set.chainHeight_add_le_chainHeight_add {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) (n : ) (m : ) :
      s.chainHeight + n t.chainHeight + m ls.subchain, l't.subchain, l.length + n l'.length + m
      theorem Set.chainHeight_le_chainHeight_TFAE {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : Set α) (t : Set β) :
      [s.chainHeight t.chainHeight, ls.subchain, l't.subchain, l.length = l'.length, ls.subchain, l't.subchain, l.length l'.length].TFAE
      theorem Set.chainHeight_le_chainHeight_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
      s.chainHeight t.chainHeight ls.subchain, l't.subchain, l.length = l'.length
      theorem Set.chainHeight_le_chainHeight_iff_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] {s : Set α} {t : Set β} :
      s.chainHeight t.chainHeight ls.subchain, l't.subchain, l.length l'.length
      theorem Set.chainHeight_mono {α : Type u_1} [LT α] {s : Set α} {t : Set α} (h : s t) :
      s.chainHeight t.chainHeight
      theorem Set.chainHeight_image {α : Type u_1} {β : Type u_2} [LT α] [LT β] (f : αβ) (hf : ∀ {x y : α}, x < y f x < f y) (s : Set α) :
      (f '' s).chainHeight = s.chainHeight
      @[simp]
      theorem Set.chainHeight_dual {α : Type u_1} [LT α] (s : Set α) :
      (OrderDual.ofDual ⁻¹' s).chainHeight = s.chainHeight
      theorem Set.chainHeight_eq_iSup_Ici {α : Type u_1} (s : Set α) [Preorder α] :
      s.chainHeight = is, (s Set.Ici i).chainHeight
      theorem Set.chainHeight_eq_iSup_Iic {α : Type u_1} (s : Set α) [Preorder α] :
      s.chainHeight = is, (s Set.Iic i).chainHeight
      theorem Set.chainHeight_insert_of_forall_gt {α : Type u_1} {s : Set α} [Preorder α] (a : α) (hx : bs, a < b) :
      (insert a s).chainHeight = s.chainHeight + 1
      theorem Set.chainHeight_insert_of_forall_lt {α : Type u_1} {s : Set α} [Preorder α] (a : α) (ha : bs, b < a) :
      (insert a s).chainHeight = s.chainHeight + 1
      theorem Set.chainHeight_union_le {α : Type u_1} {s : Set α} {t : Set α} [Preorder α] :
      (s t).chainHeight s.chainHeight + t.chainHeight
      theorem Set.chainHeight_union_eq {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) (H : as, bt, a < b) :
      (s t).chainHeight = s.chainHeight + t.chainHeight
      theorem Set.wellFoundedGT_of_chainHeight_ne_top {α : Type u_1} [Preorder α] (s : Set α) (hs : s.chainHeight ) :
      theorem Set.wellFoundedLT_of_chainHeight_ne_top {α : Type u_1} [Preorder α] (s : Set α) (hs : s.chainHeight ) :