diff --git a/cpo.tex b/cpo.tex index 834141a0a85fdc56a417e769b209b48029309e15..7b3bfa917d35b99d9827d123534e3c9a18ebc8df 100644 --- a/cpo.tex +++ b/cpo.tex @@ -21,9 +21,10 @@ A map on \defn{cpo}{CPOs} \(\phi : \map{(X, \sqsubseteq)}{(X', \sqsubseteq')}\) is \emph{(Scott-)continuous} if is \de{monotone} and it preserves - \des{join}, \[ x_0 \sqsubseteq \dots \sqsubseteq \bigsqcup_{i = - 0}^\infty x_i \implies \phi(x_0) \sqsubseteq' \dots \sqsubseteq' \phi\left(\bigsqcup_{i = - 0}^\infty x_i\right) \] + \des{join} for all chains + \(\forall \left(x_i\right)_{i \in \mathbb{N}}\): + \[ {\bigsqcup_{i = 0}^\infty}' \phi(x_i) = \phi\left(\bigsqcup_{i = + 0}^\infty x_i\right) \] \end{definition} \begin{theorem}[Kleene]\label{thm:kleene}