From c4da7b6c439ec8f4f440de4bd3abb770d61200b2 Mon Sep 17 00:00:00 2001
From: Spencer Killen <sjkillen@ualberta.ca>
Date: Mon, 4 Nov 2024 15:42:25 -0700
Subject: [PATCH] .

---
 notation.tex |  4 +++-
 note.tex     | 18 +++++++++++++++++-
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/notation.tex b/notation.tex
index ba93611..9ad9192 100644
--- a/notation.tex
+++ b/notation.tex
@@ -1,4 +1,6 @@
 \newcommand{\fixpointsOf}{\textbf{\textit{fix}}}
 \renewcommand{\L}{\mathcal{L}}
 \newcommand{\lte}{\preceq}
-\newcommand{\image}[1]{[#1]}
\ No newline at end of file
+\newcommand{\image}[1]{[#1]}
+\newcommand{\define}{\coloneqq}
+\newcommand{\union}{\cup}
\ No newline at end of file
diff --git a/note.tex b/note.tex
index 88112ad..6bc17db 100644
--- a/note.tex
+++ b/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}