Chain Bounding, the Leanest Proof of Zorn's Lemma, and an Illustration of Computerized Proof Formalization

Abstract

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 through the use of Chain Bounding are amongst the simplest ones that we are aware of. As a by-product, we show that for every poset P and function f from the powerset of P into P, there exists a maximal well-ordered chain whose family of initial segments is appropriately closed under f. We also provide an introduction to the process of “computer formalization” of mathematical proofs by using proof assistants. As an illustration, we verify our main results with the Lean proof assistant.