Theorem. Nothing suddenly invented at infinity [dt-0045]

Let D and E be algebraic cpos. Then a function f : D \rightarrow E is continuous iff, for all x \in D: f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} In other words, in an algebraic cpo, continuous functions are completely defined by their behaviour for compact arguments.

This makes precise our earlier slogan in Definition [dt-001J], that continuous functions don't suddenly behave differently for infinite (i.e. non-compact) elements.

Proof.

First, assuming f is continuous, we show that f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}: \begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ \end {array} It remains to show that if f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}, then f is continuous. Using the alternative definition, we shall first show that f is monotone. Let a \sqsubseteq b for a,b \in D. Then \mathop {\downarrow }(a) \subseteq \mathop {\downarrow }(b) and thus \{f(x) \mid x \in \mathop {\downarrow }(a)\} \subseteq \{f(x) \mid x \in \mathop {\downarrow }(b)\}, therefore: \begin {array}{lclr} f(a) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(a) \} & \text {(assumption)}\\ & \sqsubseteq &\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(b) \} & \text {(from above)}\\ & = & f(b) & \text {(assumption)}\\ \end {array} Next, let X \subseteq D be directed. \begin {array}{lclr} f(\bigsqcup X) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(\bigsqcup X) \} & \text {(assumption)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in \mathsf {K}(X) \land x \sqsubseteq \bigsqcup X \} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathsf {K}(X) \land x \sqsubseteq y \} & \text {(compactness)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathop {\downarrow }(y)\} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in X\} & \text {(algebraicity)}\\ \end {array}