Dilworth's Theorem: in any partial ordering, the size of the largest possible antichain is equal to the smallest possible number of chains in a partition of the items into chains.

If you already know, in a bipartite graph with \( n \) vertices, maximum matching \( M \), and maximum independent set \( I \), that \( n=|M|+|I| \), then a proof is easy: form a bipartite graph with \( 2n \) vertices, one copy of each item of the ordering in each side and an edge from the smaller to the larger of each pair of comparable items. Find a matching \( M \) and maximum independent set \( I \). The edges of \( M \) decompose the items into \( n-|M| \) chains, and the items that have both of their copies belonging to \( I \) form an antichain of at least \( n-|M| \) items. The antichain must have exactly \( n-|M| \) items, for it can have at most one item from each chain.

Anyway, I've now implemented all this in PADS. It's in a new module PartialOrder.py, which also contains everything that used to be in TopologicalOrder.py. Along with the new MaximumAntichain and MinimumChainDecomposition functions, I included a TransitiveClosure function, as it was needed when the input order is given by a sparser DAG.