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]

#### Contents (PDF format)

1. Preliminaries
2. Fixpoints in general
3. The lattice of lattice subset
4. Complete lattices
5. Boolean lattices

#### Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Complete lattices. Journal of Formalized Mathematics, 4, 1992.
[5] Grzegorz Bancerek. Quantales. Journal of Formalized Mathematics, 6, 1994.
[6] Grzegorz Bancerek. Continuous, stable, and linear maps of coherence spaces. Journal of Formalized Mathematics, 7, 1995.
[7] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.
[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[10] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[12] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[13] J.-L. Lassez, V. L. Nguyen, and E. A Sonenberg. Fixed point theorems and semantics: a folk tale. \em Information Processing Letters, 14(3):112--116, 1982.
[14] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[15] Lawrence C. Paulson. Set theory for verification: II, induction and recursion. \em Journal of Automated Reasoning, 15(2):167--215, 1995.
[16] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[18] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[19] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[20] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[21] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[22] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.
[23] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.