= Solution
A <complete lattice> has every <join>, hence every directed and finite join. Conversely, if a <partially ordered set> is <directed-complete> and has finite joins including the empty join, then for any subset $A$ the set of joins of its finite subsets is nonempty and <directed>. Its <least upper bound> is $\bigvee A$. Including the empty join supplies a bottom element and handles $A=\varnothing$.
For a <directed set> of <partial functions> from $A$ to $B$, their union is a function: any two functions have a common extension, so they agree wherever their domains overlap. This union is exactly their <least upper bound> in the extension order, proving directed completeness.
Write $C_x$ for the intersection of all sets containing $x$ and closed under $f$ and directed joins. Then $x\mathrel R y$ means $y\in C_x$. Reflexivity is immediate, and transitivity follows because any closed set containing $x$ must contain $y$ and then every $z$ with $y\mathrel R z$. The upper set $[x,\infty)$ is closed: $f$ is <inflationary>, and a directed join of elements above $x$ is above $x$. Thus $x\mathrel R y$ implies $x\le y$, proving antisymmetry.
If $h,k\in H$, then $x\mathrel R k(x)\mathrel R h(k(x))$, so $h\circ k\in H$. Moreover $h(k(x))\ge h(x)$ by <monotonicity>, and $h(k(x))\ge k(x)$ by inflationarity. This proves that $H x$ is <directed>. Define $h_0(x)=\bigvee H x$. Pointwise monotonicity of every $h$ implies monotonicity of $h_0$. Since $H x\subseteq C_x$ and $C_x$ is closed under directed joins, $x\mathrel R h_0(x)$; hence $h_0\in H$.
The original map $f$ belongs to $H$ by the definition of closedness, so $f\circ h_0\in H$ and $f(h_0(x))\le h_0(x)$ by the definition of the join. Inflationarity gives the reverse inequality. Finally, if $p=f(p)$ and $p\ge x$, the lower set $(-\infty,p]$ is closed by monotonicity of $f$ and the join property. Thus every $h(x)$ is at most $p$, and so is $h_0(x)$. This proves the <least fixed point from a directed family of maps>: $h_0(x)$ is the least <fixed point> above $x$.
Back to article page
