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