The Teichmüller-Tukey Lemma

Vithor Lindermann Kraisch 📧 and Luiz Gustavo Cordeiro 📧

September 21, 2026

Abstract

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.

License

BSD License

Note

Grammar check in texts and abstract; Help to compile and prepare the submission. Not used in the proofs.

Topics

Related publications

  • Sun, T., & Yu, W. (2019). Formalization of the Axiom of Choice and its Equivalent Theorems (Version 1). arXiv. https://doi.org/10.48550/ARXIV.1906.03930

Session Teichmuller_Tukey_Lemma

Cite

× 
@article{Teichmuller_Tukey_Lemma-AFP,
  author  = {Vithor Lindermann Kraisch and Luiz Gustavo Cordeiro},
  title   = {The Teichmüller-Tukey Lemma},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Teichmuller_Tukey_Lemma.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download