### Abstract

We develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any properties of ordering, thus complete non-orders. In particular, we generalize the Knaster–Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition—attractivity—which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.

### License

BSD License

### Topics

- Mathematics/Order

### Session Complete_Non_Orders

- Binary_Relations
- Well_Relations
- Directedness
- Complete_Relations
- Fixed_Points
- Continuity
- Kleene_Fixed_Point

### Used by

- Formalizing Results on Directed Sets

## Cite

×

Complete_Non_Orders-AFP

    @article{Complete_Non_Orders-AFP,
      author  = {Akihisa Yamada and Jérémy Dubut},
      title   = {Complete Non-Orders and Fixed Points},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Complete_Non_Orders.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 28, 2019 : Isabelle2019