Least Fixed-Points of Monotone Functions are Monotone

This post presents a simple lemma related to the Knaster-Tarski fixed-point theorem. I used to think it's obvious, but today I set out to write down the full proof and I was somewhat surprised that I got stuck for awhile. As often is the case, I got unstuck with some help from Rasmus, and his slides in this case.

Definitions. Feel free to skip and refer back only if necessary.

A partial order $\le$ is a binary relation that is reflexive, transitive, and antisymmetric. $$\begin{align} &(1) &&x \le x\\ &(2) &&x \le y \land y \le z \to x \le z\\ &(3) &&x \le y \land y \le x \to x = y \end{align}$$ A greatest lower bound $\inf Y$ of a set $Y$ is a lower bound (smaller than all elements of $Y$) and as big as possible: $$\begin{align} &(4) &&y:Y\to \inf Y \le y\\ &(5) &&(\forall y\; y:Y\to x\le y) \to x\le\inf Y \end{align}$$ Lowest upper bounds are defined symmetrically. A set equipped with a preorder is a complete lattice when all its subsets $Y$ have a greatest lower bound $\inf Y$ and a lowest upper bound $\sup Y$. A function $f$ is monotone when it preserves the order: $$\begin{align} &(6) && x \le y \to f(x) \le f(y) \end{align}$$ A pre-fixed-point of $f$ is an element $x$ that may only decrease by going thru $f$: $$\begin{align} &(7) && f(x) \le x \end{align}$$ Post-fixed-points are defined symmetrically. A fixed-point is an element that is both pre- and post-fixed-point. A least fixed point ${\rm lfp}\,f$ of $f$ is the minimum of fixed points: $$\begin{align} &(8) &&f({\rm lfp}\,f)={\rm lfp}\,f\\ &(9) &&f(x)=x \to {\rm lfp}\,f \le x \end{align}$$ Note that there is no a-priori reason to believe that least fixed-points (or even fixed-points) exist. Let ${\rm pre}\,f=\{x:f(x)\le x\}$ denote the set of $f$'s pre-fixed points.

Lemmas. Suppose from now on that $f$ is a fixed but arbitrary monotone function, on some complete lattice. Here's the first lemma: $$\begin{align} &(10) &&f(y)\le y \to f(\inf{\rm pre}\,f) \le y \end{align}$$ Proof. $$\begin{align} & &&f(y) \le y\\ &\Rightarrow &&\{\text{$(4)$ with $Y:={\rm pre}\,f$}\}\\ & &&\inf{\rm pre}\,f \le y\\ &\Rightarrow &&\{(6)\}\\ & &&f(\inf{\rm pre}\,f)\le f(y)\\ &\Rightarrow &&\text{assumption $f(y)\le y$}\\ & &&f(\inf{\rm pre}\,f)\le y \end{align}$$

Here's the second lemma: $$\begin{align} &(11) &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f \end{align}$$ Proof. Instantiate (5) with $x:=f(\inf{\rm pre}\,f)$, and use (10) to discharge the assumption.

Here's the third lemma: $$\begin{align} &(12) &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f) \end{align}$$ Proof. Be careful here. It's a tricky argument that avoids talking about descending chains and such. $$\begin{align} & &&\{(11)\} \\ & &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f \\ &\Rightarrow &&\{(6)\}\\ & &&f(f(\inf{\rm pre}\,f)) \le f(\inf{\rm pre}\,f) \\ &\Rightarrow &&\{\text{$(4)$ with $y:=f(\inf{\rm pre}\,f)$ and $Y:={\rm pre}\,f$}\} \\ & &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f) \end{align}$$

Here's the fourth lemma: $$\begin{align} &(13) &&{\rm lfp}\,f \le \inf{\rm pre}\,f \end{align}$$ Proof. $$\begin{align} & &&\{\text{$(3)$ with $x:=\inf{\rm pre}\,f$ and $y:=f(\inf{\rm pre}\,f)$}\}\\ & &&(\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f))\land(f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f) \to \inf{\rm pre}\,f=f(\inf{\rm pre}\,f)\\ &\Rightarrow &&\{\text{$(11)$ and $(12)$}\}\\ & &&\inf{\rm pre}\,f=f(\inf{\rm pre}\,f) \\ &\Rightarrow &&\{\text{$(9)$ with $x:=\inf{\rm pre}\,f$}\} \\ & &&{\rm lfp}\,f \le \inf{\rm pre}\,f \end{align}$$

You guessed: Here's the fifth lemma: $$\begin{align} &(14) &&f(y)\le y \to {\rm lfp}\,f \le y \end{align}$$ Proof. $$\begin{align} & &&f(y) \le y \\ &\Rightarrow &&\{(10)\} \\ & &&f(\inf{\rm pre}\,f) \le y \\ &\Rightarrow &&\{\text{$(13)$ and $(2)$}\} \\ & &&{\rm lfp}\,f \le y \end{align}$$

Proposition. Least-fixed points of monotone functions are monotone. Given that both $f$ and $g$ are monotone functions on some complete lattice, we have that $$\begin{align} \bigl(\forall x\; f(x) \le g(x)\bigr) \to {\rm lfp}\,f \le {\rm lfp}\, g \end{align}$$ Proof. $$\begin{align} & &&f(x) \le g(x) \\ &\Rightarrow &&\{\text{instantiate with $x:={\rm lfp}\,g$}\} \\ & &&f({\rm lfp}\,g) \le g({\rm lfp}\,g) \\ &= &&\{\text{$(8)$ with $f:=g$}\} \\ & &&f({\rm lfp}\,g) \le {\rm lfp}\,g \\ &\Rightarrow &&\{\text{$(14)$ with $y:={\rm lfp}\,g$}\} \\ & &&{\rm lfp}\,f \le {\rm lfp}\, g \end{align}$$