Theorem 1 (LATTICE-THEORETICAL FIXPOINT <</A>85#>THEOREM)   Lethttp://planetmath.org/encyclopedia/ETAC2.html]

(i)

$\mathfrak{A}=(A,\ \leq)$ be a complete lattice,

(ii)

$f$ be an increasing function on $A$ to $A,$

(iii)

$P$ the set of all fixpoints of $f.$

Then the set $P$ is not empty and the system $(P,\ \leq)$ is a complete lattice; in particular we have $$ \cup P=\cup E_{x}[f(x)\geq x]\in P $$ and $$ \cap P=\cap E_{x}[f(x)\leq x]\in P. $$

Definition 1   A poset (partially ordered set) $\mathfrak{A}=(A,\ \leq)$ consists of a nonempty set $A$ and a relation $$ \leq:\ A\times A\longrightarrow\{\text{False},\ \text{True}\} $$ that is reflexive ($a\leq a$ $\forall a\in A$ ), antisymmetric ($\forall \ a,\ b\in A,$ if $a\leq b$ and $b\leq a,$ then $a=b$ ). and transitive ($\forall\ a,\ b,\ c\in A,$ if $a\leq b$ and $b\leq c,$ then $a\leq c$ ).

Definition 2   If $\mathfrak{A}=(A,\ \leq)$ is a poset and $B$ is a nonempty subset of $A,$ then $\sup(B)$ is an element of $A,$ if it exists, with these properties:

1. $\forall\ b\in B,~b\leq\sup(B)$ , (in shorthand, $B\leq\sup(B)$ ).
2. If $a\in A$ and $B\leq a,$ then $\sup(B)\leq a.$

Similarly $\inf(B)$ is an element of $A,$ if it exists, with these properties:

(3)

$\inf(B)\leq B,$

(4)

If $a\in A$ and $a\leq B,$ then $a\leq\inf(B).$

Theorem 2   If $\sup(B)$ exists, then it is unique; if $\inf(B)$ exists, it is unique.

Definition 3   Let $\mathfrak{A}=(A,\ \leq)$ be a poset. Then $\mathfrak{A}$ is a lattice if $\forall\ a,\ b\in A,$ the set $\{a,\ b\}$ has a $\sup$ and an $\inf.$ We write $$ a\cup b=\sup(\{a,\ b\})\quad\text{and}\quad a\cap b=\inf(\{a,\ b\}). $$

Theorem 3   Let $\mathfrak{A}=(A,\ \leq)$ be a lattice. Then

1. $a\cup b=b\cup a,\qquad a\cap b=b\cap a$
2. $(a\cup b)\cup c=a\cup(b\cup c),\qquad(a\cap b)\cap c=a\cap(b\cap c)$
3. $a\cup(b\cap c)\leq(a\cup b)\cap(a\cup c).\qquad(a\cap b)\cup(a\cap c)\leq a\cap(b\cup c).$

Definition 4   A poset $\mathfrak{A}=(A,\ \leq)$ is a complete lattice if for each nonempty $B\subseteq A,$ both $\sup(B)$ and $\inf(B)$ exist.

Theorem 4 (LATTICE-THEORETICAL FIXPOINT THEOREM)   Let

(i)

$\mathfrak{A}=(A,\ \leq)$ be a complete lattice,

(ii)

$f$ be an increasing function on $A$ to $A,$

(iii)

$P$ the set of all fixpoints of $f.$

Then the set $P$ is not empty and the system $(P,\ \leq)$ is a complete lattice; in particular we have $$ \cup P=\cup E_{x}[f(x)\geq x]\in P $$ and $$ \cap P=\cap E_{x}[f(x)\leq x]\in P. $$

Theorem 5   Let $\mathfrak{A}=(A,\ \leq)$ be a complete lattice. Let $f$ be an increasing function on $A$ to $A,$ that is, whenever $a\leq b,$ then $f(a)\leq f(b).$ Let $P$ be the set of all fixed points of $f:$ $$ P=\{\ a\in A\ |\ f(a)=a\ \}. $$ Then

1. $P\neq\emptyset$ .
2. The system $\mathfrak{P}=(P,$ $\leq)$ is a complete lattice.
3. Set $B=\{\ b\in A\ |\ b\leq f(b)\ \}$ . Then $B\neq\emptyset$ and $\sup(B)=\sup(P)\in P.$
4. Set $C=\{\ c\in A\ |\ f(c)\leq c\ \}$ . Then $C\neq\emptyset\ $ and $\inf(C)=\inf(P)\in P.$

Lemma 1   Let $\mathfrak{A}=(A,\ \leq)$ be a complete lattice and $\emptyset\neq A_{0}\subseteq A.$ Let $$ D=\{d\in A\ |\ d\leq A_{0}\},\qquad E=\{e\in A\ |\ A_{0}\leq e\}. $$ ($d\leq A_{o}$ means $d\leq a_{0}$ $\forall a_{0}\in A_{0}.$ ) Then both $B$ and $C$ are complete lattices, with $\leq$ inherited from that of $A.$

Proof. [Proof (of Lemma)]We'll do the case of $D;$ that for $E$ is similar (dual). First, $D\neq\emptyset$ because $\inf(A)\in D.$ Suppose $\emptyset\neq G\subseteq D.$ Obviously $$ \inf(G)\leq g\leq A_{0} $$ for any $g\in G,$ so $\inf(G)\in D.$ As $g\leq A_{0}$ for all $g\in G,$ we have $\sup(G)\leq A_{0}$ by (2) in the definition of $\sup.$ So $\sup(G)\in D.$ As $G$ was any nonempty subset of $D,$ these statements say that $D$ is a complete lattice.

Proof. [Proof (of Theorem)]$B\neq\emptyset$ because $\inf(A)\in B.$ Hence $b_{1} =\sup(B)$ exists. If $b\in B,$ then $b\leq b_{1},$ which implies $$ f(b)\leq f(b_{1}). $$ because $f$ is increasing., so $$ b\leq f(b)\leq f(b_{1}). $$ This is true $\forall$ $b\in B.$ Hence $$ b_{1}=\sup(B)\leq f(b_{1}). $$ Therefore $b_{1}\in B.$ Because $f$ is increasing, this implies $$ f(b_{1})\leq f(f(b_{1})), $$ from which $f(b_{1})\in B.$ Hence $f(b_{1})\leq\sup(B)=b_{1}.$ From $$ b_{1}\leq f(b_{1})\leq b_{1} $$ we have $f(b_{1})=b_{1},$ that is, $b_{1}\in P.$ This settles (1): $P\neq \emptyset,$ and incidentally proves $\sup(B)\in P.\smallskip$

From this, $\sup(B)\leq\sup(P).$ But obviously $P\subseteq B,$ so $\sup(P)\leq\sup(B).$ Therefore $\sup(P)=\sup(B),$ completing the proof of (3). Statement (4) is proved similarly (or dually).$\smallskip$

Next we prove (2). Let $\emptyset\neq P_{0}\subseteq P.$ Set $$ Q=\{\ q\in A\ |\ q\leq P_{0}\ \}. $$ By the Lemma, $Q$ is a complete lattice. If $q\in Q,$ then $\forall\ p_{0}\in P_{0},$ we have $q\leq p_{0},$ hence $$ f(q)\leq f(p_{0})=p_{0}\ , $$ that is, $f(q)\in Q.$ In other words, $$ f:\ Q\longrightarrow Q. $$ By what we have already proved for $A,$ applied to $Q,$ we have $\sup(Q)\in Q,$ and $\sup(Q)$ is a fixed point of $f.$ That is, $\sup(Q)\in P.$ But obviously $\sup(Q)=\inf(P_{0}),$ so $\inf(P_{0})\in P$ Similarly $\sup (P_{0})\in P,$ completing the proof of (2): $P$ is a complete lattice.