<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml">The following theorem is due to Dilworth [8]: Let <italic>P</italic> be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of <italic>P</italic> is <italic>k</italic>, then <italic>P</italic> is the union of <italic>k</italic> chains (cliques).In this article we formalize an elegant proof of the above theorem for finite posets by Perles [13]. The result is then used in proving the case of infinite posets following the original proof of Dilworth [8].A dual of Dilworth's theorem also holds: a poset with maximum clique <italic>m</italic> is a union of <italic>m</italic> independent sets. The proof of this dual fact is considerably easier; we follow the proof by Mirsky [11]. Mirsky states also a corollary that a poset of <italic>r</italic> x <italic>s</italic> + 1 elements possesses a clique of size <italic>r</italic> + 1 or an independent set of size <italic>s</italic> + 1, or both. This corollary is then used to prove the result of Erdős and Szekeres [9].Instead of using posets, we drop reflexivity and state the facts about anti-symmetric and transitive relations.</abstract>

The following theorem is due to Dilworth [8]: Let P be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of P is k, then P is the union of k chains (cliques).In this article we formalize an elegant proof of the above theorem for finite posets by Perles [13]. The result is then used in proving the case of infinite posets following the original proof of Dilworth [8].A dual of Dilworth's theorem also holds: a poset with maximum clique m is a union of m independent sets. The proof of this dual fact is considerably easier; we follow the proof by Mirsky [11]. Mirsky states also a corollary that a poset of r x s + 1 elements possesses a clique of size r + 1 or an independent set of size s + 1, or both. This corollary is then used to prove the result of Erdős and Szekeres [9].Instead of using posets, we drop reflexivity and state the facts about anti-symmetric and transitive relations.

Dilworth's Decomposition Theorem for Posets

Formalized Mathematics

{"article-title":"Dilworth's Decomposition Theorem for Posets"}

The following theorem is due to Dilworth [8]: Let P be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of P is...

Dilworth's Decomposition Theorem for Posets

Published Online: Jul 08, 2010

Page range: 223 - 232

DOI: https://doi.org/10.2478/v10037-009-0028-4

This content is open access.