Cofinality and the Delta System Lemma

Pedro Sánchez Terraf 🌐

December 27, 2020


We formalize the basic results on cofinality of linearly ordered sets and ordinals and Šanin’s Lemma for uncountable families of finite sets. This last result is used to prove the countable chain condition for Cohen posets. We work in the set theory framework of Isabelle/ZF, using the Axiom of Choice as needed.


BSD License


Session Delta_System_Lemma