Mirsky's theorem

DefinitionFinite antichain covers#✓fully proved

Let \(\alpha\) be a partially ordered set. A finite family \(C\) of finite subsets of \(\alpha\) is a finite antichain cover of \(\alpha\) when every member of \(C\) is an antichain and every element of \(\alpha\) belongs to some member of \(C\).

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

Used by 2

Used byMinimum antichain cover size · Dual of Dilworth's theorem

DefinitionMaximum chain size#✓fully proved

For a finite partially ordered set \(\alpha\), the maximum chain size of \(\alpha\) is the largest cardinality of a chain in \(\alpha\), that is, of a set of pairwise comparable elements.

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

Used by 2

Used byMirsky's theorem · Dual of Dilworth's theorem

DefinitionMinimum antichain cover size#✓fully proved

For a finite partially ordered set \(\alpha\), the minimum antichain cover size of \(\alpha\) is the smallest number of antichains in \(\alpha\) whose union is all of \(\alpha\).

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

Uses 1 · Used by 2

Statement usesFinite antichain covers

Used byMirsky's theorem · Dual of Dilworth's theorem

TheoremDual of Dilworth's theorem#✓fully proved

For every finite partially ordered set \(\alpha\), the maximum chain size of \(\alpha\) equals its minimum antichain cover size: the largest cardinality of a chain in \(\alpha\) equals the smallest number of antichains whose union is \(\alpha\).

theorem mirsky_dual_general {α : Type*} [Fintype α] [PartialOrder α] :
    maxChainSize α = minAntichainCoverSize α

Uses 3 · Used by 1

Statement usesMaximum chain size · Minimum antichain cover size

Proof usesFinite antichain covers

Used byMirsky's theorem

TheoremMirsky's theorem#✓fully proved

For every finite partially ordered set \(\alpha\), the maximum chain size of \(\alpha\) equals its minimum antichain cover size: the largest cardinality of a chain in \(\alpha\) equals the smallest number of antichains whose union is \(\alpha\).

@[nolint unusedArguments]
theorem mirsky_dual {α : Type*} [Fintype α] [DecidableEq α] [PartialOrder α] :
    maxChainSize α = minAntichainCoverSize α

Sources

• L. Mirsky, Amer. Math. Monthly 78 (1971), 876-877, DOI 10.2307/2316481. It follows from mirsky_dual_general; the instance [DecidableEq α] is unused and keeps the Wanted entry's shape.

Uses 3

Statement usesMaximum chain size · Minimum antichain cover size

Proof usesDual of Dilworth's theorem

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.