From 65a2b4cef4c5e49fbf90050b47524da6991500b6 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Mon, 29 Jun 2026 12:37:13 -0400
Subject: [PATCH] FIxed up lattices.

---
 src/fa/order/lattice.tex | 82 +++++++++++++++++++++++++++++-----------
 1 file changed, 60 insertions(+), 22 deletions(-)

diff --git a/src/fa/order/lattice.tex b/src/fa/order/lattice.tex
index 9996c96..8a11b6e 100644
--- a/src/fa/order/lattice.tex
+++ b/src/fa/order/lattice.tex
@@ -87,41 +87,79 @@
     Let $(E, \le)$ be a vector lattice and $x, y \in E$, then $x$ and $y$ are \textbf{disjoint}, denoted $x \perp y$, if $|x| \wedge |y| = 0$.
 \end{definition}
 
+\begin{lemma}
+\label{lemma:lattice-gymnastics}
+    Let $E$ be a vector lattice and $a, b, c, d \in E$, then
+    \begin{enumerate}
+        \item $a + b = a \vee b + a \wedge b$.
+        \item $b \le a + |b - a|$.
+        \item If $c \ge 0$, then $(a + c) \vee b \le a \vee b + c$.
+        \item $|a \vee c - b \vee c| \le |a - b|$.
+        \item $|a \vee c - b \vee d| \le |a - b| \vee |c- d|$
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1): By translation invariance, 
+    \begin{align*}
+        x \vee y + x \wedge y - x - y &= 0 \vee (y - x) + (x - y) \wedge 0 \\
+        &= 0 \vee (y - x) - 0 \vee (x - y) = 0
+    \end{align*}
 
-\begin{proposition}[{{\cite[V.1.1]{SchaeferWolff}}}]
+    (2): $b = a + b - a \le a + |b - a|$.
+
+    (3): Since $c \ge 0$, 
+    \[
+    (a + c) \vee b = (a + c) \vee (b - c + c) = a \vee (b - c) + c \le a \vee b + c
+    \]
+
+    (4): By (2) and then (3), 
+    \begin{align*}
+        a \vee c - b \vee c &\le (b + |a - b|) \vee c - b \vee c \\
+        &\le b \vee c + |a - b| - b \vee c \le |a - b|
+    \end{align*}
+    
+    Similarly, $b \vee c - a \vee c \le |b - a| = |a - b|$.
+
+    (5): Finally, 
+    \begin{align*}
+        a \vee c - b \vee d &\le (b + |a - b|) \vee (d + |c- d|) - b \vee d \\
+        &\le (b + |a - b| \vee |c- d|) \vee (d + |a - b| \vee |c- d|) - b \vee d \\
+        &= b \vee d + |a - b| \vee |c- d| - b \vee d \\
+        &\le |a - b| \vee |c- d| 
+    \end{align*}
+
+    Similarly, 
+    \[
+    b \vee d - a \vee c \le  |b - a| \vee |d - c| = |a - b| \vee |c- d|  
+    \]
+    
+\end{proof}
+
+
+
+\begin{proposition}
 \label{proposition:lattice-properties}
     Let $(E, \le)$ be a vector lattice, then:
     \begin{enumerate}
-        \item For any $x, y \in E$,
-        \[
-        x + y = x \vee y + x \wedge y
-        \]
-
         \item Let $x \in E$, $x^+ = x \vee 0 \ge 0$, and $x^- = -(x \wedge 0) \ge 0$, then $x = x^+ - x^-$ and $|x| = x^+ + x^-$. Moreover, $(x^+, x^-)$ are the unique disjoint non-negative elements of $E$ such that $x = x^+ - x^-$.
     \end{enumerate}
 
     For any $x, y \in E$ and $\lambda \in \real$, 
-    \begin{enumerate}
-        \item[(3)] $|\lambda x| = |\lambda| \cdot |x|$
-        \item[(4)] $|x + y| \le |x| + |y|$.
+    \begin{enumerate}[start=1]
+        \item $|\lambda x| = |\lambda| \cdot |x|$
+        \item $|x + y| \le |x| + |y|$.
     \end{enumerate}
 
     
     Finally, for any $x, y \in E$ with $x, y \ge 0$, 
-    \begin{enumerate}
-        \item[(5)] $[0, x] + [0, y] = [0, x + y]$.
+    \begin{enumerate}[start=3]
+        \item $[0, x] + [0, y] = [0, x + y]$.
     \end{enumerate}
 
     
 \end{proposition}
-\begin{proof}
-    (1): By \autoref{proposition:ordered-vector-space-properties},
-    \begin{align*}
-        x \vee y + x \wedge y - x - y &= 0 \vee (y - x) + (x - y) \wedge 0 \\
-        &= 0 \vee (y - x) - 0 \vee (y - x) = 0
-    \end{align*}
-    
-    (2): By (1),
+\begin{proof}[Proof, {{\cite[V.1.1]{SchaeferWolff}}}. ]
+    (1): By \autoref{lemma:lattice-gymnastics},
     \[
     x  = x + 0 = x \vee 0 + x \wedge 0 = x^+ - x^-
     \]
@@ -150,12 +188,12 @@
 
     and $x^- \le z$. If $y \perp z$, then $y - x^+ \perp z - x^-$. Since $y - x^+ = z - x^-$, $y - x^+ = z - x^- = 0$, so $y = x^+$ and $z = x^-$. 
 
-    (3): For any $\lambda > 0$, by (LO2),
+    (2): For any $\lambda > 0$, by (LO2),
     \[
     |\lambda x| = (\lambda x) \vee (-\lambda x) = \lambda (x \vee -x) = \lambda |x|
     \]
 
-    (4): For any $x, y \in E$, by \autoref{proposition:ordered-vector-space-properties},
+    (3): For any $x, y \in E$, by \autoref{proposition:ordered-vector-space-properties},
     \begin{align*}
     x^+ + y^+ &= (x \vee 0) + (y \vee 0) = x \vee y \vee (x + y) \vee 0 \\
     &\ge (x + y) \vee 0 = (x + y)^+
@@ -166,7 +204,7 @@
     |x+y| = (x+y)^+ + (x + y)^- \le x^+ + y^+ + x^- + y^- = |x| + |y|
     \]
 
-    (5): Let $x, y \in E$ with $x, y \ge 0$, then $[0, x] + [0, y] \subset [0, x + y]$. For any $z \in [0, x + y]$, let $u = z \wedge x$ and $v = z - u$, then
+    (4): Let $x, y \in E$ with $x, y \ge 0$, then $[0, x] + [0, y] \subset [0, x + y]$. For any $z \in [0, x + y]$, let $u = z \wedge x$ and $v = z - u$, then
     \[
         v = z - z \wedge x = z + (-z \vee -x) = (0 \vee z - x) \le z - x \le y
     \]