Commit 2021-12-15 19:58 9525f5e0
View on Github →feat(order/zorn): Added some results about chains (#10658)
Added chain_empty, chain_subsingleton, and chain.max_chain_of_chain.
The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle.