Added some linfty.

src/measure/measure/localisable.tex

@@ -198,43 +198,3 @@
         \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}
-
-\begin{corollary}
-\label{corollary:l-infty-dedekind-complete}
-    Let $(X, \cm, \mu)$ be a localisable measure space, then $L^\infty(X; \real)$ is order complete. 
-\end{corollary}
-\begin{proof}
-    Let $\seqi{f} \subset L^\infty(X; \real)$ and $M \in \real$ such that $f_i \le M$ almost everywhere for all $i \in I$. 
-
-    Fix $A \in \cm$ with $\mu(A) < \infty$, and let
-    \[
-    \mathcal{S}_A = \bracs{g \in L^\infty(A; \real)| f_i|_A \le g \text{ almost everywhere }\forall i \in I}
-    \]
-
-    then since $f_i \le M$ almost everywhere for all $i \in I$, $\mathcal{S}_A \ne \emptyset$, and $m_A = \inf_{g \in \mathcal{S}_A}\int g d\mu \in \real$.
-    
-    Let $\seq{g_{A, n}} \subset \mathcal{S}_A$ such that $\seq{g_{A, n}}$ is decreasing pointwise and $\limv{n}\int_A g_{A, n} d\mu \downto m_A$. Take $g_A = \limv{n}g_{A, n}$, then by the \hyperref[Dominated Convergence Theorem]{theorem:dct}, $\int g_A d\mu = m_A$. 
-
-    For each $i \in I$, since $g_{A, n} \ge f_i|_A$ almost everywhere for all $n \in \natp$, $g_A \ge f_i|_A$ almost everywhere as well. Thus $g_A \in \mathcal{S}_A$. For any $h \in \mathcal{S}_A$, $g_A \wedge h \in \mathcal{S}_A$ with
-    \[
-    m_A \le \int_A g_A \wedge h d\mu \le \int_A g_A d\mu = m_A 
-    \]
-
-    Thus $g_A \wedge h = g_A$ almost everywhere, so $g_A \le h$ almost everywhere, and $g_A$ is an essential supremum of $\bracsn{f_i|_A}_{i \in I}$. 
-
-    Now, let $A, B \in \cm$ with $\mu(A), \mu(B) < \infty$, then $\one_{A \cap B} g_B + \one_{A \setminus B}M \in \mathcal{S}_A$, and
-    \[
-    m_A \le \int_A g_A \wedge (\one_{A \cap B} g_B + \one_{A \setminus B}M)d\mu \le \int_A g_A d\mu = m_A
-    \]
-
-    Thus $g_A \wedge (\one_{A \cap B} g_B + \one_{A \setminus B}M) = g_A$ almost everywhere, so $g_A|_{A \cap B} \le g_B|_{A \cap B}$ almost everywhere. As the argument is symmetric, $g_A|_{A \cap B} = g_B|_{A \cap B}$ almost everywhere. 
-
-    By the \hyperref[gluing lemma for measurable functions]{lemma:gluing-measurable}, there exists a measurable function $g:X \to \real$ such that $g|_A = g_A$ for all $A \in \cm$ with $\mu(A) < \infty$. 
-
-    Let $h \in L^\infty(X; \real)$ with $h \ge f_i$ almost everywhere for all $i \in I$, then for any $A \in \cm$ with $\mu(A) < \infty$, 
-    \[
-    \mu(\bracs{h < g} \cap A) \le \mu(\bracs{h|_A < g_A} \cup \bracs{g|_A \ne g_A}) = 0
-    \]
-    
-    As $\mu$ is semifinite, $\mu(\bracs{h < g}) = 0$. Finally, since $g_A \le M$ almost everywhere for all $A \in \cm$ with $\mu(A) < \infty$, $g \le M$ almost everywhere. Therefore $g \in L^\infty(X; \real)$ is indeed the essential supremum of $\seqi{f}$. 
-\end{proof}