2024/04/17 by Guillermo L. Incatasciato, Incatasciato, Guillermo L., Pedro Sánchez Terraf +1
Mathematics · #03-01 #03E25 #06A06 #68V20 #Advanced Differential Equations and Dynamical Systems #Analytic Number Theory Research #F.4.1 #FOS: Mathematics #History and Overview (math.HO) #I.2.3 #Logic (math.LO) #Point processes and geometric inequalities
paper · pdf · doi:10.48550/arxiv.2404.11638
openalex publication_date 2024/04/17 · openalex created_date 2024/04/20 · openalex updated_date 2026/07/28
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 *proofs assistants*. As an illustration, we verify our main results with the Lean proof assistant.