LARA

Comparing Fixpoints of Sequences

Lemma: Let $(L,\sqsubseteq)$ be a lattice and let $x_i, y_i \in L$ and for $i \ge 0$ be sequences such that for each $i$ there exists $j$ such that $x_i \sqsubseteq y_j$. Suppose that there exist $x_*$ and $y_*$ (e.g. if $L$ is a complete lattice) such that

\begin{equation*} x_* = \bigsqcup_{i \ge 0} x_i \end{equation*}

\begin{equation*} y_* = \bigsqcup_{j \ge 0} y_j \end{equation*}

Then $x_* \sqsubseteq y_*$.

Proof: Take any $x_i$. Then there is $y_j$ such

\begin{equation*} x_i \sqsubseteq y_j \sqsubseteq y_* \end{equation*}

Thus, $y_*$ is an upper bound on the set $\{ x_i \mid i \ge 0\}$. Because $x_*$ is the least upper bound, $x_* \sqsubseteq y_*$. End of Proof.