Add Me!Close Menu Navigation

Limit Preserving Functions in CPOs

Very short proof that limit preserving functions (continuous functions) on complete partial orders are necessarily monotone.

A complete partial order (hereon cpo) is a partial order (D, \sqsubseteq) such that all monotone chains

    \[x_0 \sqsubseteq x_1 \sqsubseteq \cdots\]

has a least upper bound

    \[\bigsqcup_{k \in \omega} x_k \in D\]

A continuous function f: D \to E between two cpos D and E is one that preserves the limit/least upper bound on all monotone chains:

    \[f\left(\bigsqcup_{k\in \omega} x_k\right) = \bigsqcup_{k \in \omega} f(x_k)\]

Theorem (Monotonicity)

All continuous functions are monotone in the sense that x \sqsubseteq y => f(x) \sqsubseteq f(y).

Proof: For the sake of deriving a contradiction, suppose that there exists some non-monotone continuous function f: D \to E for some pairs of cpos D and E. Then it must be the case that for some pair of elements x, y \in D, x \sqsubseteq y but f(x) \not\sqsubseteq f(y). Now, consider an \omega-chain

    \[(s_k)_{k \in \omega} = x \sqsubseteq y \sqsubseteq y \sqsubseteq y \sqsubseteq \cdots\]

that is y-terminal and monotone. Obviously, its least upper bound \bigsqcup s_k = y, but

    \[\bigsqcup f(s_k) = f(x) \sqcup f(y) \sqcup f(y) \sqcup \cdots = f(x) \sqcup f(y)\]

where

    \[f(x) \sqcup f(y) \ne f(y)\]

because otherwise f(x) \subseteq f(y). Hence, we can show that

    \begin{align*} f\left(\bigsqcup s_k\right) &= f(y) \\ &\ne \bigsqcup f(s_k) \\ &= f(x) \sqcup f(y) \end{align*}

and hence f cannot be continuous; a contradiction! Therefore, all continuous functions are monotone. \square

Posted By Lee

Woosh