### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Order

### Related publications

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

### Session Directed_Sets

- Well_Order_Connection
- Directed_Completeness

### Depends on

- Complete Non-Orders and Fixed Points

## Cite

×

Directed_Sets-AFP

    @article{Directed_Sets-AFP,
      author  = {Akihisa Yamada and Jérémy Dubut},
      title   = {Formalizing Results on Directed Sets},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Directed_Sets.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023