Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Another ZF entry for the AFP

Email Gateway (Dec 28 2020 at 10:54):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce another addition to our tiny collection of entries based on Isabelle/ZF:

Cofinality and the Delta System Lemma, by Pedro Sánchez Terraf

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.

It’s online at https://www.isa-afp.org/entries/Delta_System_Lemma.html

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC