Order theory · formal theorem
Every finite poset in which each antichain has at most k elements admits a cover of all elements by k chains.
Scope: For every finite partially ordered type, width at most k implies that k chains cover all elements.
Exact formal proposition
theorem dilworthTheorem : DilworthTheoremStatementProof route
The checked proof inducts on the finite poset. A maximum antichain either splits the order into proper lower and upper closures whose recursive chain covers can be joined through common anchors, or forces a fallback that removes a comparable minimal–maximal pair and lowers the width.
These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.
|A| = width(P) ≤ k
Finiteness supplies a maximum antichain A. Its cardinality records the poset width and is at most k, so A can index the chains that will be assembled recursively.
exists_max_card_antichain_of_widthAtMostWidthAtMostwidthAtMost_max_card_antichain
P = ↓A ∪ ↑A
A concrete width-four poset is shown as the disjoint union of four finite chains. Its lower closure contains the lower three vertices of each chain plus the shared anchor, and its upper closure contains the upper three vertices plus that same anchor. Each closure is a proper subset, their intersection is exactly the four-element maximum antichain, and their union is the whole displayed poset.
lowerClosureupperClosurewidthAtMost_lowerClosure_of_max_card_antichainwidthAtMost_upperClosure_of_max_card_antichain
Cₐ = Cₐ⁻ ∪ Cₐ⁺
The exact four anchor identities, twenty-four non-anchor vertices, and within-chain incidences from the preceding closure stage are preserved. Each gold anchor belongs to one lower and one upper recursive chain; their union becomes one seven-vertex chain. The four resulting chains cover all twenty-eight displayed vertices, with no cross-anchor or cross-chain incidence.
exists_anchorIndexed_split_coverIsChain.union_of_lower_upper_anchorexists_strongCoversByChains_card_of_split
x minimal, y maximal, x ≤ y
The failed split yields a minimal element x and a maximal element y with x ≤ y. Removing the pair leaves a smaller poset whose antichains are strictly smaller than the original maximum.
exists_minimal_le_maximalwidthAtMost_erase_pair_of_no_proper_max_antichain
(k−1)-cover of P∖{x,y} + chain {x,y}
The width drop gives a cover of the remaining elements by k−1 chains. Since x≤y, the removed pair is itself a chain; adjoining it and padding empty chains when necessary completes the k-chain cover.
exists_strongCoversByChains_of_widthAtMostisChain_pair_of_leStrongCoversByChains.extenddilworthTheoremThe theorem at a glance
Accessible transcript
antichain size ≤ k ⇒ k-chain cover
The proof uses a maximum antichain to split and rejoin recursive chain covers when possible. In the remaining case it removes a comparable minimal–maximal pair, lowers the width, recurses, and adds the pair as one chain.
ORDER THEORY · FINITE POSETS
DILWORTH’S THEOREM
EVERY ANTICHAIN HAS AT MOST k ELEMENTS
THE POSET IS COVERED BY k CHAINS
CHAIN · every pair is comparable
ANTICHAIN · distinct pairs are incomparable
HOW THE PROOF MOVES
1 CHOOSE A MAXIMUM ANTICHAIN
Its size is at most k.
2 SPLIT INTO LOWER AND UPPER CLOSURES
When both are proper, recurse on each side.
3 JOIN CHAINS THROUGH COMMON ANCHORS
Corresponding lower and upper chains meet at the antichain.
4 USE THE NO-SPLIT FALLBACK
Remove a comparable minimal–maximal pair, lower the width, then add one chain.
EXACT SCOPE
Finite posets and a cover by k chains. The checked statement does not assert a disjoint partition, uniqueness, an algorithm, or an infinite-poset extension.
Theorem schematic
width(P) ≤ k ⇒ P is covered by k chains
The width bound limits every pairwise-incomparable family to k elements. Dilworth’s theorem converts that obstruction into a cover of the whole finite poset by k chains.
Result boundary
For every finite partially ordered type, width at most k implies that k chains cover all elements.
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Review record
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
The formal declaration was accepted against the named theorem and its exact variant.
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
The first-party source link is pinned to the checked package commit and exact Lean file.
A validated accepted-result record binds the four reviews to the checked formalization.