From 5f5a6681d96f448b5b98652bd34d67c053843f91 Mon Sep 17 00:00:00 2001
From: Philip Kaludercic <philip.kaludercic@fau.de>
Date: Mon, 8 Apr 2024 14:57:08 +0200
Subject: [PATCH] Define continuity of maps between CPO properly
---
cpo.tex | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/cpo.tex b/cpo.tex
index 834141a..7b3bfa9 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}
--
GitLab