Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: Dilworth's Decomposition Theorem for Posets
Autorzy: Rudnicki, Piotr
Data wydania: 2009
Data dodania: 2-gru-2015
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 17, Issue 4, 2009, Pages 223-232
Abstrakt: 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.
Afiliacja: University of Alberta, Edmonton, Canada
DOI: 10.2478/v10037-009-0028-4
ISSN: 1426-2630
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2009, Volume 17, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
v10037-009-0028-4.pdf254,28 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons