Least fixed point from a directed family of maps (source code)

= Least fixed point from a directed family of maps

Let $f$ be <order-preserving> and <inflationary> on a <directed-complete partial order>. Define $x\mathrel R y$ when every set containing $x$ and closed under $f$ and directed <joins> contains $y$. This is a <partial order> refining $\le$. The <order-preserving> maps $h$ satisfying $x\mathrel R h(x)$ form a composition-closed family $H$. The values $H x$ are <directed>, since $h(k(x))$ bounds $h(x)$ and $k(x)$. Their <least upper bound> $h_0(x)$ lies in every such closed set containing $x$, so $h_0\in H$. Then $f\circ h_0\in H$ gives $f(h_0(x))\le h_0(x)$, while inflationarity gives the reverse inequality. If $p=f(p)$ and $x\le p$, the lower set $\{y:y\le p\}$ is closed, proving $h_0(x)\le p$. Thus $h_0(x)$ is the least <fixed point> of $f$ above $x$.