Dilworth's Decomposition Theorem for Posets

Piotr Rudnicki

Formalized Mathematics (2009)

  • Volume: 17, Issue: 4, page 223-232
  • ISSN: 1426-2630

Abstract

top
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.

How to cite

top

Piotr Rudnicki. "Dilworth's Decomposition Theorem for Posets." Formalized Mathematics 17.4 (2009): 223-232. <http://eudml.org/doc/266978>.

@article{PiotrRudnicki2009,
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.},
author = {Piotr Rudnicki},
journal = {Formalized Mathematics},
language = {eng},
number = {4},
pages = {223-232},
title = {Dilworth's Decomposition Theorem for Posets},
url = {http://eudml.org/doc/266978},
volume = {17},
year = {2009},
}

TY - JOUR
AU - Piotr Rudnicki
TI - Dilworth's Decomposition Theorem for Posets
JO - Formalized Mathematics
PY - 2009
VL - 17
IS - 4
SP - 223
EP - 232
AB - 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.
LA - eng
UR - http://eudml.org/doc/266978
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  4. [4] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81-91, 1997. 
  5. [5] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93-107, 1997. 
  6. [6] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  7. [7] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  8. [8] R. P. Dilworth. A Decomposition Theorem for Partially Ordered Sets. Annals of Mathematics, 51(1):161-166, 1950.[Crossref] Zbl0038.02003
  9. [9] P. Erdős and G. Szekeres. A combinatorial problem in geometry. Compositio Mathematica, 2:463-470, 1935. Zbl0012.27010
  10. [10] Adam Grabowski. Auxiliary and approximating relations. Formalized Mathematics, 6(2):179-188, 1997. 
  11. [11] L. Mirsky. A Dual of Dilworth's Decomposition Theorem. The American Mathematical Monthly, 78(8). Zbl0263.06002
  12. [12] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  13. [13] M. A. Perles. A Proof of Dilworth's Decomposition Theorem for Partially Ordered Sets. Israel Journal of Mathematics, 1:105-107, 1963. Zbl0115.01702
  14. [14] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441-444, 1990. 
  15. [15] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990. 
  16. [16] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990. 
  17. [17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.