Why a function from a product of $\omega$-complete partial order is continuous?

213 Views Asked by At

In “The Formal Semantics of Programming Languages” by Glynn Winskel, there is Lemma 8.10 in “8. Introduction to domain theory/3. Constructions on cpo's/2. Finite products” which is promised to be “very useful”.

Let $f : D_1\times\dots\times D_k\to E$ be a function. Then $f$ is continuous iff $f$ is “continuous in each argument separately”…

($D_i$ is an $\omega$-cpo.) There is a step in its proof

$ \bigsqcup_p (\bigsqcup_q f(x_p, y_q)) = \bigsqcup_n f(x_n, y_n)$

that uses Proposition 8.9 by instantiating $e_{p,q}$ to $f(x_p, y_q)$ in it. ($n\mapsto (x_n, y_n)$ is a $\omega$-chain in $D_1\times D_2$.) But using that proposition requires $p\leq p' \land q\leq q' \to f(x_p, y_q)\leq f(x_{p'}, y_{q'})$. I understand that I can prove it if $f$ is monotone. But how do I know that $f$ is monotone? I see no such assumption in Lemma 8.10. I stuck at the same place trying to prove this theorem for directed complete partial orders (dcpo).

1

There are 1 best solutions below

0
On

If $f$ is continuous in each argument separately, then $f$ is monotone in each argument separately, then $f$ is monotone because the order on $E$ is transitive.