Dilworth's theorem

DefinitionChain cover#✓fully proved

Let \(\alpha\) be a partially ordered set. A finite set \(C\) of finite subsets of \(\alpha\) is a chain cover of \(\alpha\) when every member of \(C\) is a chain and every element of \(\alpha\) lies in some member of \(C\).

def IsChainCoverFin {α : Type*} [PartialOrder α] (C : Finset (Finset α)) : Prop :=
  (∀ s ∈ C, IsChain (· ≤ ·) (s : Set α)) ∧ ∀ a : α, ∃ s ∈ C, a ∈ s

Used by 4

Used byDilworth's theorem · The minimum chain cover size is attained · Minimum chain cover size · Chain covers bound the minimum chain cover size

DefinitionMaximum antichain size#✓fully proved

For a finite partially ordered set \(\alpha\), the maximum antichain size of \(\alpha\) (its width) is the largest number of elements of an antichain in \(\alpha\).

noncomputable def maxAntichainSize
    (α : Type*) [Fintype α] [PartialOrder α] : ℕ :=
  ((Finset.univ : Finset α).powerset).sup fun s =>
    if IsAntichain (· ≤ ·) (s : Set α) then s.card else 0

Used by 4

Used byAntichains are no larger than the maximum antichain size · Dilworth's theorem · The maximum antichain size is attained · The minimum chain cover size is attained

DefinitionMinimum chain cover size#✓fully proved

For a finite partially ordered set \(\alpha\), the minimum chain cover size of \(\alpha\) is the smallest number of chains in a chain cover of \(\alpha\), that is, in a finite set of chains of \(\alpha\) whose union is \(\alpha\).

noncomputable def minChainCoverSize
    (α : Type*) [Fintype α] [PartialOrder α] : ℕ :=
  let all : Finset (Finset (Finset α)) := (Finset.univ.powerset).powerset
  let valid := all.filter fun C => IsChainCoverFin (α := α) C
  if h : valid.Nonempty then valid.inf' h fun C => C.card else 0

Uses 1 · Used by 3

Statement usesChain cover

Used byDilworth's theorem · The minimum chain cover size is attained · Chain covers bound the minimum chain cover size

TheoremAntichains are no larger than the maximum antichain size#✓fully proved

Let \(\alpha\) be a finite partially ordered set. Every antichain \(A\) in \(\alpha\) has at most as many elements as the maximum antichain size of \(\alpha\).

theorem card_le_maxAntichainSize {α : Type*} [Fintype α] [PartialOrder α]
    {A : Finset α} (hA : IsAntichain (· ≤ ·) (A : Set α)) : A.card ≤ maxAntichainSize α

Uses 1

Statement usesMaximum antichain size

TheoremChain covers bound the minimum chain cover size#✓fully proved

Let \(\alpha\) be a finite partially ordered set. If \(C\) is a chain cover of \(\alpha\), that is, a finite set of chains of \(\alpha\) whose union is \(\alpha\), then the minimum chain cover size of \(\alpha\) is at most the number of chains in \(C\).

theorem minChainCoverSize_le_card {α : Type*} [Fintype α] [PartialOrder α]
    {C : Finset (Finset α)} (hC : IsChainCoverFin (α := α) C) :
    minChainCoverSize α ≤ C.card

Uses 2 · Used by 2

Statement usesChain cover · Minimum chain cover size

Used byDilworth's theorem · The minimum chain cover size is attained

TheoremDilworth's theorem#✓fully proved

Let \(\alpha\) be a finite partially ordered set. The maximum antichain size of \(\alpha\) equals its minimum chain cover size: the largest number of elements of an antichain in \(\alpha\) equals the smallest number of chains whose union is \(\alpha\).

theorem dilworth_decomposition
    {α : Type*} [Fintype α] [PartialOrder α] :
    maxAntichainSize α = minChainCoverSize α

Sources

• R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51 (1950), 161-166, DOI 10.2307/1969503.

Uses 4 · Used by 1

Statement usesMaximum antichain size · Minimum chain cover size

Proof usesChain cover · Chain covers bound the minimum chain cover size

Used byThe minimum chain cover size is attained

TheoremThe maximum antichain size is attained#✓fully proved

Let \(\alpha\) be a finite partially ordered set. Some antichain in \(\alpha\) has exactly as many elements as the maximum antichain size of \(\alpha\).

theorem exists_isAntichain_card_eq_maxAntichainSize {α : Type*} [Fintype α]
    [PartialOrder α] :
    ∃ A : Finset α, IsAntichain (· ≤ ·) (A : Set α) ∧ A.card = maxAntichainSize α

Uses 1

Statement usesMaximum antichain size

TheoremThe minimum chain cover size is attained#✓fully proved

Let \(\alpha\) be a finite partially ordered set. Some chain cover \(C\) of \(\alpha\), a finite set of chains of \(\alpha\) whose union is \(\alpha\), consists of exactly as many chains as the minimum chain cover size of \(\alpha\).

theorem exists_isChainCoverFin_card_eq_minChainCoverSize {α : Type*} [Fintype α]
    [PartialOrder α] :
    ∃ C : Finset (Finset α), IsChainCoverFin C ∧ C.card = minChainCoverSize α

Uses 5

Statement usesChain cover · Minimum chain cover size

Proof usesDilworth's theorem · Maximum antichain size · Chain covers bound the minimum chain cover size

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.