Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

**Piotr Rudnicki**- University of Alberta, Edmonton
**Andrzej Trybulec**- Warsaw University, Bialystok

- 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.

- Preliminaries
- Fixpoints in general
- The lattice of lattice subset
- Complete lattices
- Boolean lattices

- [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.

[ Download a postscript version, MML identifier index, Mizar home page]