# Completeness of the quotient of the power set lattice of a partial order induced by the Hoare pre-order

Let $(P,\le)$ be a partially ordered set and $\preceq$ the Hoare pre-order on its subsets, i.e. for $X,Y\subseteq P$, $X\preceq Y$ iff $\forall x\in X:\exists y\in Y:x\le y$.

Let $\sim$ be the equivalence on the power set $2^P$ generated by $\preceq$, i.e. $X\sim Y$ iff $X\preceq Y$ and $Y\preceq X$. Let $M=2^P/\mathord\sim$ be the quotient, then $\preceq$ passes to a partial order, also denoted $\preceq$, on $M$.

Is $(M,\preceq)$ a complete lattice?

• As far as I can see, a union of a family of sets is its lub in $\preceq$, or am I missing something? – Emil Jeřábek supports Monica May 5 '15 at 13:58
• In fact, $(M,\preceq)$ is apparently (isomorphic to) the complete lattice of downsets in $P$, as $X\preceq Y$ iff $X{\downarrow}\subseteq Y{\downarrow}$. This is an upside-down complete Heyting algebra. – Emil Jeřábek supports Monica May 5 '15 at 14:03
• Thank you Emil, this looks right to me. But (next question) is it well-known? I'm not familiar with the old papers on domain theory, but it seems like something which should be in there. – Uli Fahrenberg May 20 '15 at 12:46