Email Gateway (Mar 25 2025 at 13:17): Email Gateway (Mar 25 2025 at 13:17):From: Tobias Nipkow <nipkow@in.tum.de>
Formal Proof of Dilworth's Theorem
Vivek Soorya Maadoori, Syed Mohammad Meesum, Shiv Pillai, T.V.H. Prathamesh and
Aditya Swami
A chain is defined as a totally ordered subset of a partially ordered set. A
chain cover refers to a collection of chains of a partially ordered set whose
union equals the entire set. A chain decomposition is a chain cover consisting
of pairwise disjoint sets. An antichain is a subset of elements of a partially
ordered set in which no two elements are comparable.
In 1950, Dilworth proved that in any finite partially ordered set, the
cardinality of a largest antichain equals the cardinality of a smallest chain
decomposition.
In this paper, we formalise a proof of the theorem above, also known as
Dilworth's theorem, based on a proof by Perles (1963). We draw on the
formalisation of Dilworth's theorem in Coq by Abhishek Kr. Singh, and depend on
the AFP entry containing formalisation of minimal and maximal elements in a set
by Martin Desharnais.
https://www.isa-afp.org/entries/Dilworth.html
Enjoy!
Last updated: Apr 18 2025 at 01:39 UTC