论文标题
固定点定理非传播关系
Fixed Points Theorems for Non-Transitive Relations
论文作者
论文摘要
在本文中，我们开发了一个订单理论固定点定理的isabelle/hol库。我们将形式化尽可能笼统地保持：我们根据完全具有反对称性或诱人的命令来否定几个众所周知的结果，这是由反对称或传递性暗示的轻度条件。特别是，我们概括了各种定理，以确保在完全关系上存在单调图的准固定点，并证明（Quasi-）固定点本身是完整的。该结果概括并增强了担为塔尔斯基，布尔巴基·韦特，克莱恩，马尔科夫斯基，帕塔拉亚，马什本，巴塔·乔治和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.
