Introduced scaffold to localisable measure spaces.

src/measure/measure/localisable.tex

@@ -105,7 +105,7 @@
 
 \begin{lemma}
 \label{lemma:gluing-measurable-sets}
-    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $\bracs{(E_A, F_A)}_{A \in \cf}$ such that:
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} localisable measure space and $\bracs{(E_A, F_A)}_{A \in \cf}$ be pairs of measurable sets such that:
     \begin{enumerate}[label=(\alph*)]
         \item For each $A \in \cf$, $E_A, F_A \in \cm$, $E_A, F_A \subset A$, and $E_A \cap F_A = \emptyset$. 
         \item For each $A, B \in \cf$, $\mu((E_A \cap B) \Delta (E_B \cap A)) = 0$ and $\mu((F_A \cap B) \Delta (F_B \cap A)) = 0$.
@@ -132,7 +132,7 @@
 
 \begin{lemma}[Gluing Lemma for Measurable Functions]
 \label{lemma:gluing-measurable}
-    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $Y$ be a Polish space, and $\bracsn{f_A: A \to Y|A \in \cf}$ such that:
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} localisable measure space, $Y$ be a Polish space, and $\bracsn{f_A: A \to Y|A \in \cf}$ such that:
     \begin{enumerate}[label=(\alph*)]
         \item For each $A \in \cf$, $f_A \in \mathcal{L}^0(A; Y)$. 
         \item For each $A, B \in \cf$, $f_A|_{A \cap B} = f_B|_{A \cap B}$ almost everywhere.  
@@ -160,7 +160,7 @@
         \end{align*}
         
         so $f|_A = f_A$ almost everywhere on $A$. 
-        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ almost everywhere. 
+        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\cf$ is a scaffold for $\mu$, $f = g$ almost everywhere. 
     \end{enumerate}
     
     Therefore $f$ is the desired function. 
@@ -191,11 +191,11 @@
         \mu\paren{\bracs{\limv{n}f_n \text{ does not exist}} \cap A} &= 0
     \end{align*}
 
-    As $\mu$ is semifinite, $\mu\bracsn{\limv{n}f_n \text{ does not exist}} = 0$. By (1) and \autoref{proposition:metric-measurable-limit}, there exists $f \in \mathcal{L}^0(X; Y)$ such that $f = \limv{n}f_n$ almost everywhere. In which case, 
+    As $\cf$ is a scaffold for $\mu$, $\mu\bracsn{\limv{n}f_n \text{ does not exist}} = 0$. By (1) and \autoref{proposition:metric-measurable-limit}, there exists $f \in \mathcal{L}^0(X; Y)$ such that $f = \limv{n}f_n$ almost everywhere. In which case, 
     \begin{enumerate}
         \item $f \in \mathcal{L}^0(X; Y)$. 
         \item For each $A \in \cf$, $f|_A = \limv{n}f_n|_A = \limv{n}f_{A, n} = f_A$ almost everywhere. 
-        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ almost everywhere. 
+        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\cf$ is a scaffold for $\mu$, $f = g$ almost everywhere. 
     \end{enumerate}
 \end{proof}