Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-31
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Mirsky's theorem: the minimum number of antichains covering a finite poset equals its height

Statement

Let P be a nonempty finite poset of height h(P). Then P can be covered by h(P) antichains, and no cover by fewer antichains exists. Thus the minimum number of antichains in an antichain cover of P equals h(P).

Facts & Assumptions

Given: A nonempty finite poset P with height h:=h(P).

[F1]

A chain is a subset of pairwise comparable elements; an antichain is a subset of pairwise incomparable elements; and an antichain cover has union P (Chain in a poset, Antichains, chain covers, and antichain covers of a poset).

[F2]

The height h(P) is the maximum cardinality of a chain in P (Height and width of a nonempty finite poset).

[L1]

Every nonempty subset of N has a least element (The well-ordering principle); equivalently, every nonempty finite bounded collection of natural numbers has a greatest element.

Proof

technique · direct
1.1

For each x∈P, let r(x) be the greatest cardinality of a chain whose largest element is x. Such a chain exists, since {x} is one, and the greatest cardinality exists because the possible values form a nonempty finite subset of {1,…,∣P∣}.

givenF1L1
1.2

Let C be a chain of cardinality h, which exists by [F2]. Every antichain contains at most one element of C, so any antichain cover of P needs at least h members to cover the h elements of C.

F1F2
2.1

If x<y, then appending y to a chain of cardinality r(x) ending at x gives a chain ending at y, so r(y)≥r(x)+1.

step 1.1F1
3.1

For i∈{1,…,h} put Ai:={x∈P:r(x)=i}. Each Ai is an antichain, since comparable distinct elements have different r-values by step 2.1.

step 2.1F1
4.1

Every x∈P belongs to exactly one Ai, and 1≤r(x)≤h by the definition of height, so A1,…,Ah cover P.

step 1.1step 3.1F2
5.1

Step 4.1 gives an antichain cover with h members and step 1.2 rules out every smaller one. Hence the minimum antichain-cover number is h(P).

step 4.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources