Added existence of the Haar measure.

src/topology/main/lch.tex

@@ -40,7 +40,7 @@
 \label{lemma:lch-urysohn}
     Let $X$ be a LCH space, $K \subset X$ be compact, and $U \in \cn(K)$, then there exists $f \in C_c(X; [0, 1])$ such that $\supp{f} \subset U$.
 \end{lemma}
-\begin{proof}[Proof {{\cite[Lemma 4.32]{Folland}}}. ]
+\begin{proof}[Proof, {{\cite[Lemma 4.32]{Folland}}}. ]
     By \autoref{lemma:lch-compact-neighbour}, there exists $V, W \in \cn^o(K)$ precompact such that
     \[
     K \subset V \subset \ol{V} \subset W \subset \ol{W} \subset U
@@ -106,7 +106,7 @@
 
 
 
-\begin{proposition}[{{\cite[Proposition 4.39]{Folland}}}]
+\begin{proposition}
 \label{proposition:lch-sigma-compact}
     Let $X$ be a LCH space, then the following are equivalent:
     \begin{enumerate}
@@ -114,7 +114,7 @@
         \item There exists an exhaustion of $X$ by compact sets.
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Proposition 4.39]{Folland}}}. ]
     (1) $\Rightarrow$ (2): Let $\seq{K_n} \subset 2^X$ be compact such that $\bigcup_{n \in \natp}K_n = X$, and $U_0 = \emptyset$.
 
     Assume inductively that $\bracs{U_j}_0^n$ has been constructed such that:
@@ -132,11 +132,11 @@
     Thus $\bracs{U_j}_0^{n+1}$ satisfies (a), (b), and (c), and $\seq{U_n}$ is an exhaustion of $X$ by compact sets.
 \end{proof}
 
-\begin{proposition}[{{\cite[Proposition 4.41]{Folland}}}]
+\begin{proposition}
 \label{proposition:lch-partition-of-unity}
     Let $X$ be a LCH space, $K \subset X$ be compact, and $\seqi{U}$ be an open cover of $K$, then there exists a $C_c$ partition of unity on $K$ subordinate to $\seqi{U}$.
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Proposition 4.41]{Folland}}}. ]
     Since $K$ is compact, assume without loss of generality that $\seqi{U} = \seqf{U_j}$.
 
     For every $x \in K$, there exists $1 \le j \le n$ and $N_x \in \cn(x)$ compact such that $x \in N_x \subset U_j$. By compactness of $K$, there exists $\seqf[m]{x_j} \subset K$ such that $K = \bigcup_{j = 1}^m N_{x_j}$.
@@ -260,6 +260,14 @@
     (6) $\Rightarrow$ (2): Let $\seqi{f} \subset C_c(X; [0, 1])$ be a partition of unity. For each $i \in I$, let $V_i = \bracs{f_i > 0}$, then $\seqi{V}$ is a locally finite precompact open cover of $\mathcal{U}$.
 \end{proof}
 
+\begin{proposition}
+\label{proposition:paracompact-lch-normal}
+    Let $X$ be a paracompact LCH space, then $X$ is normal. 
+\end{proposition}
+\begin{proof}
+    Let $A, B \subset X$ be disjoint closed sets. By \autoref{proposition:lch-paracompact}, there exists a partition of unity $\seqi{f}$ subordinate to $\bracs{A^c, B^c}$. Let $I = I_A \sqcup I_B$ such that for each $i \in I_A$, $\supp{f_i} \subset B^c$, and for each $i \in I_B$, $\supp{f_i} \subset A^c$. Take $f = \sum_{i \in I_A}f_i$ and $g = \sum_{i \in I_B}f_i$, then since $f|_B = 0$ and $g|_A = 0$, $\bracs{f \ge 2/3} \in \cn_X(A)$ and $\bracs{f \le 1/3} \in \cn_X(B)$. 
+\end{proof}
+
 \begin{proposition}
 \label{proposition:lch-sigma-paracompact}
     Let $X$ be a $\sigma$-compact LCH space, then $X$ is paracompact.
@@ -270,4 +278,3 @@
     Let $x \in X$, then there exists $n \in \natp$ such that $x \in U_n \setminus U_{n-1}$. In which case, if $n > 1$, then $x \in U_{n} \setminus \ol{U_{n - 2}} = V_{n-1}$. If $n = 1$, then $x \in U_{2} = V_1$. Thus $\seq{V_n}$ is an open cover of $X$. In addition, for any $m, n \in \natp$ with $m \le n$, $V_m \cap V_n \ne \emptyset$ implies that $n - m < 2$, so $\seq{V_n}$ is locally finite. By (2) of \autoref{proposition:lch-paracompact}, $X$ is paracompact.
 \end{proof}
 
-

src/topology/main/support.tex

@@ -8,9 +8,20 @@
 
 \begin{definition}[Compactly Supported]
 \label{definition:compactly-supported}
-    Let $X$ be a topological space, $E$ be a TVS over $K \in \RC$, and $f \in C(X; E)$, then $f$ is \textbf{compactly supported} if $\supp{f}$ is compact. The set $C_c(X; E)$ is the vector space of all $E$-valued compactly supported functions on $X$.
+    Let $X$ be a topological space, $E$ be a TVS over $K \in \RC$, and $f \in C(X; E)$, then $f$ is \textbf{compactly supported} if $\supp{f}$ is compact. The set $C_c(X; E)$ is the space of $E$-valued compactly supported continuous functions on $X$.
 \end{definition}
 
+\begin{definition}[Non-negative Compactly Supported Functions]
+\label{definition:non-negative-compactly-supported}
+    Let $X$ be a topological space, then
+    \[
+    C_c^+(X) = \bracs{f \in C_c(X)|f \ge 0}
+    \]
+
+    is the space of \textbf{non-negative compactly supported continuous functions} on $X$. 
+\end{definition}
+
+
 \begin{definition}
 \label{definition:compactly-supported-01}
     Let $X$ be a topological space, $f \in C_c(X; [0, 1])$ and $U \subset X$ be open, then $f \prec U$ if $\supp{f} \subset U$.