Formalization of the core ideas extracted from G. Incatasciato's proof of Zorn's Lemma (ZL). It accompanies the paper in collaboration Chain Bounding and the Leanest proof of Zorn's Lemma (arXiv:2404.11638).
All the results are included in the file GreatestGoodChain.lean
, and include
- the existence of a greatest good chain for every operator on the powerset of a poset;
- proof of the new principles of Chain Bounding and the Unbounded Chain Lemma;
- proofs of ZL and the Bourbaki-Witt Fixed Point Theorem using the latter.