Construction. Product of cpos [dt-0021]

Liam O'Connor

Given cpos $A$ and $B$ , the product $A \times B$ is itself a cpo, ordered by $(x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y'$ with bottom value $\bot _{X \times Y}$ being $(\bot _A, \bot _B)$ . Least upper bounds are found by taking the lubs of each component:

\bigsqcup X \; = \; \left (\bigsqcup \{ \pi _0(x) \mid x \in X \}, \bigsqcup \{ \pi _1(x) \mid x \in X \}\right )

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$