非传递关系的定点定理
Fixed Points Theorems for Non-Transitive Relations
AI总结：
本文构建Isabelle/HOL库，在弱化条件下推广完全关系上单调映射的定点定理，并证明定点集合的完备性，强化多个经典结果。
摘要：
本文中，我们开发了一个关于序理论定点定理的Isabelle/HOL库。我们尽可能保持形式化的一般性：我们重新证明了关于完全序的几个众所周知的结果，通常仅依赖于反对称性或吸引性，这是一种由反对称性或传递性蕴含的温和条件。特别是，我们推广了多个确保完全关系上单调映射拟定点存在的定理，并证明了（拟）定点集合本身是完全的。这一结果推广并强化了Knaster-Tarski、Bourbaki-Witt、Kleene、Markowsky、Pataraia、Mashburn、Bhatta-George和Stouti-Maaden的定理。
英文摘要：
In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
