Email Gateway (Aug 22 2022 at 19:57): Email Gateway (Aug 22 2022 at 19:57):From: Tobias Nipkow <nipkow@in.tum.de>
Complete Non-Orders and Fixed Points
Akihisa Yamada and Jérémy Dubut
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.
https://www.isa-afp.org/entries/Complete_Non_Orders.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC