Formalizing Results on Directed Sets

Akihisa Yamada 📧 and Jérémy Dubut 📧

May 24, 2023


Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL's ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.


BSD License


Related publications

  • A. Yamada and J. Dubut. Formalizing Results on Directed Sets in Isabelle/HOL. ITP 2023. To appear.

Session Directed_Sets