The pair is called a partial order, when is a partial order on D, that is, a reflexive, antisymmetric and transitive relation. Let . We say that d is a lower bound of X if, for all , . d is the greatest lower bound (glb) of X, if d is a lower bound, and, for every e such that e is a lower bound of X, we have . An analogue definition holds for upper bounds and the least upper bound (lub). We say that is a minimal (or bottom) element of D, if is a lower bound for D.
The set of continuous functions from the cpo D to the cpo E will be denoted by .
Example 139. ()
Every set ordered by the identity function is a discrete cpo. Any function from discrete cpo’s to discrete cpo’s are continuous.
Let be the cpo consisting of elements and such that .
Let X be a set. Let . Then is a complete lattice.
Let . Then F is a cpo.
Let be the partial order . Then is a cpo. Let be such that
Then is continuous for every , but is not continuous.
A fixpoint of f is both a prefixpoint and a postfixpoint. d is called the least fixpoint (lfp) of f , if d is a fixpoint, and, for every , .
Without proof we state the following theorem.
is the least fixpoint of f , where , , and . Moreover, is the least prefixpoint of f , that is, if , then .
Below, we consider a straightforward application of the Knaster-Tarski theorem. Let X be a set, and be a relation over X. As before, let
and let . We assert the following lemma.
Proof. First of all, observe that is continuous. For, let be a chain in . Then
This means, Theorem 142 is applicable. Let , and for . Thus,
By this, the lemma is proved.
As a consequence, we prove that indeed defines the reflexive, transitive closure of R.
Proof. By the Knaster–Tarski theorem it is enough to verify that Q is a prefixpoint of . By the reflexivity of Q, we have , moreover, by assumption, , which, together with transitivity, yields .