Definition. Complete partial order [dt-001D]

Liam O'Connor

A complete partial order or cpo (more specifically a directed complete partial order or dcpo) is a poset where lubs exist for the empty set and for all directed subsets. That is, a cpo is a poset $A$ such that:

$A$ has a bottom element $\bot \in A$ , that is the lub of the empty set, and
$\bigsqcup X$ exists for all directed $X \subseteq A$ .

$\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$