fixpoint-theory-nov24/betastable/sections/sketchjan20.tex

\begin{definitionOf}{chain}
    Given a \Poset $\langle \LL, \lte \rangle$, a {\em chain} is a (possibly empty) set $C \subseteq \LL$ that is totally ordered, that is, 
    for all $x, y \in C$ either $x \lte y$ or $y \lte x$.
\end{definitionOf}

\begin{definitionOf}{setordering}
    Given a preorder, $\langle \LL, \lte \rangle$
    We define a set ordering $\langle \powersetO(\LL), \lte \rangle$
    s.t. for any $X, Y \subseteq \LL$
    \begin{align*}
        X \lte Y \textrm{ iff } (X \upclosure) \supseteq Y
    \end{align*}
\end{definitionOf}

\begin{definitionOf}{chaincompleteposet}
    We call \Poset $\langle \LL, \lte \rangle$ {\em chain-complete} if $\lub \LL$ is unique and in $\LL$ and for ever chain $C \subseteq \LL$
    \begin{enumerate}
        \item $\lub \LL$ is unique and in $\LL$, and
        \item for every chain $C \subseteq \LL$, we have $\lub C \in \LL$
    \end{enumerate}
\end{definitionOf}

\begin{definitionOf}{antisymmequiv}
    Given a set $\powersetO(\LL)^2$, define $\antisymmequiv{\powersetO(\LL)^2}$ to be the set obtained by removing any elements $x \in \powersetO(\LL)^2$ s.t. $x \not= x \upprecision$.
\end{definitionOf}

\begin{remark}
    The \Preorder $\langle \powersetO(\LL)^2, \lteSetLPrecision \rangle$ lacks \Antisymmetry, thus it is not a \Poset.
    We can construct and equivalence relation $\equiv$ based on the \Antisymmetry condition:
        $x \equiv x' \textrm{ iff } x \lteSetLPrecision x' \textrm{ and } x' \lteSetLPrecision x$.
    Each equivalence class $[x]$ can be uniquely represented by $x \upprecision$. Thus, another way of viewing 
    $\langle \antisymmequiv{\powersetO(\LL)^2}, \lteSetLPrecision \rangle$
    is as the quotient under the above equivalence relation.
\end{remark}

\begin{lemma}
    Given $\langle \antisymmequiv{\powersetO(\LL)^2}, \lteSetLPrecision \rangle$, and $x, y \in  \powersetO(\LL)^2$
    \begin{enumerate}
        \item $x \lteSetRPrecision y$. 
        \item if $x \lteSetLPrecision y$ then $x \lteSetLRPrecision y$. 
    \end{enumerate}
\end{lemma}
\begin{proof}
    (1) We have $\top_{\ltePrecision} \in y$. (2) Follows from (1).
\end{proof}


\begin{propositionOf}{chaincompletepreserve}
    Let $\langle \LL, \lte \rangle$ be a \CompleteLattice and $o: \LL^2 \rightarrow \powersetO(\LL)$ \AnNdao.
    The structure $\langle \antisymmequiv{o\image{R}}, \lteSetL \rangle$ is a \ChainCompletePoset where $R$ is one of the following:
    \begin{enumerate}
        \item\label{chaincompletepreserve:enum:a} $\LL^2$,
        \item\label{chaincompletepreserve:enum:b} $\LLc$
        \item\label{chaincompletepreserve:enum:c} $\postfixpointsOf(o)$
        \item\label{chaincompletepreserve:enum:d} $\prefixpointsOf(S(o))$
    \end{enumerate}
\end{propositionOf}
\begin{proof}
    This should be simpler, the incoming is chain complete poset so should inject one ?


\end{proof}