Formalizing Results on Directed Sets

Akihisa Yamada 📧 and Jérémy Dubut 📧

May 24, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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