This commit is contained in:
parent
e8f348f060
commit
c4da7b6c43
|
@ -1,4 +1,6 @@
|
|||
\newcommand{\fixpointsOf}{\textbf{\textit{fix}}}
|
||||
\renewcommand{\L}{\mathcal{L}}
|
||||
\newcommand{\lte}{\preceq}
|
||||
\newcommand{\image}[1]{[#1]}
|
||||
\newcommand{\image}[1]{[#1]}
|
||||
\newcommand{\define}{\coloneqq}
|
||||
\newcommand{\union}{\cup}
|
18
note.tex
18
note.tex
|
@ -5,6 +5,8 @@
|
|||
\usepackage{bm}
|
||||
\usepackage[english]{babel}
|
||||
\usepackage{amsthm}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{mathtools}
|
||||
\newcommand{\jh}[1]{{\leavevmode\color{blue!50!red}#1}}
|
||||
|
||||
\input{notation.tex}
|
||||
|
@ -36,7 +38,21 @@ $$\fixpointsOf(S)$$
|
|||
For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle o\imageNoLink{\L}, \lte \rangle$ is a \CompleteLattice.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
foo
|
||||
Consider $\langle \L', \lte' \rangle$ where
|
||||
\begin{align*}
|
||||
\L' \define \{ x' ~|~ x \in \L \} \\
|
||||
x' \lte' y' \iff x \lte y \textrm{ where } x, y \in \L
|
||||
\end{align*}
|
||||
Clearly, $\langle \L', \lte' \rangle$ is a \CompleteLattice.
|
||||
Combining $\L$ and $\L'$
|
||||
\begin{align*}
|
||||
\L^* \define \{ \top^*, \bot^* \} \union \L \union \L' \\
|
||||
\forall x^*, y^* \in \L^*, x^* \lte y^* \iff \begin{cases}
|
||||
(x^* = \bot^*) \lor (y^* = \top^*) \\
|
||||
two \\
|
||||
three
|
||||
\end{cases}
|
||||
\end{align*}
|
||||
\end{proof}
|
||||
|
||||
\bibliographystyle{plain}
|
||||
|
|
Loading…
Reference in New Issue