Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Teichmuller-Tukey Lemma

Email Gateway (Sep 23 2026 at 10:30):

From: Tobias Nipkow <nipkow@in.tum.de>

The Teichmüller-Tukey Lemma
Vithor Lindermann Kraisch and Luiz Gustavo Cordeiro

This entry formalizes the Teichmüller-Tukey lemma in Isabelle/HOL: every
nonempty family of sets of finite character contains a member that is maximal
under inclusion. The development follows the direct choice-function construction
of Sun and Yu, originally presented in Morse-Kelley set theory and verified in Coq.

https://isa-afp.org/entries/Teichmuller_Tukey_Lemma.html

Enjoy!

smime.p7s

Last updated: Oct 08 2026 at 21:07 UTC