@MISC{KNASTER.MIZ,
  AUTHOR = {Rudnicki, Piotr and Trybulec, Andrzej},
  TITLE = {Fixpoints in Complete Lattices},
  NOTE = {This work was partially supported by NSERC Grant OGP9207
		  and NATO CRG 951368.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Fixpoints in general},
  SECTION3 = {The lattice of lattice subset},
  SECTION4 = {Complete lattices},
  SECTION5 = {Boolean lattices},
  DAY = {16},
  MONTH = {September},
  YEAR = {1996},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {Warsaw University\\Bia{\l}ystok},
  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. \cite{lns82}.
	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 \cite{lcp95}).  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. \cite{lns82},
	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).}}

