Fixpoints in Complete Lattices

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

Fixpoints in Complete Lattices

Piotr Rudnicki: University of Alberta, Edmonton
Andrzej Trybulec: Warsaw University, Bialystok

Summary.

Theorem (5) states that if an iterate of a function has a unique fixpoint then it is also the fixpoint of the function. It has been included here in response to P. Andrews claim that such a proof in set theory takes thousands of lines when one starts with the axioms. While probably true, such a claim is misleading about the usefulness of proof-checking systems based on set theory.\par Next, we prove the existence of the least and the greatest fixpoints for $\subseteq$-monotone functions from a powerset to a powerset of a set. Scheme {\it Knaster} is the Knaster theorem about the existence of fixpoints, cf. [13]. Theorem (11) is the Banach decomposition theorem which is then used to prove the Schr\"{o}der-Bernstein theorem (12) (we followed Paulson's development of these theorems in Isabelle [15]). It is interesting to note that the last theorem when stated in Mizar in terms of cardinals becomes trivial to prove as in the Mizar development of cardinals the $\leq$ relation is synonymous with $\subseteq$.\par Section 3 introduces the notion of the lattice of a lattice subset provided the subset has lubs and glbs.\par The main theorem of Section 4 is the Tarski theorem (43) that every monotone function $f$ over a complete lattice $L$ has a complete lattice of fixpoints. As the consequence of this theorem we get the existence of the least fixpoint equal to $f^\beta(\bot_L)$ for some ordinal $\beta$ with cardinality not bigger than the cardinality of the carrier of $L$, cf. [13], and analogously the existence of the greatest fixpoint equal to $f^\beta(\top_L)$.\par Section 5 connects the fixpoint properties of monotone functions over complete lattices with the fixpoints of $\subseteq$-monotone functions over the lattice of subsets of a set (Boolean lattice).

This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

MML Identifier: KNASTER

The terminology and notation used in this paper have been introduced in the following articles [17] [11] [19] [20] [22] [21] [8] [10] [9] [16] [14] [12] [2] [3] [1] [6] [23] [4] [5] [18] [7]