Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization

Guillermo L. Incatasciato, Pedro Sánchez Terraf

We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results…