Added measurability in separable metric spaces.

src/measure/index.tex

@@ -4,3 +4,4 @@
 \input{./src/measure/sets/index.tex}
 \input{./src/measure/measure/index.tex}
 \input{./src/measure/measurable-maps/index.tex}
+\input{./src/measure/lebesgue-integral/index.tex}

src/measure/lebesgue-integral/index.tex

@@ -0,0 +1,4 @@
+\chapter{The Lebesgue Integral}
+\label{chap:lebesgue-integral}
+
+%\input{./src/measure/lebesgue-integral/simple.tex}

src/measure/measurable-maps/index.tex

@@ -3,3 +3,6 @@
 
 \input{./src/measure/measurable-maps/measurable-maps.tex}
 \input{./src/measure/measurable-maps/product.tex}
+\input{./src/measure/measurable-maps/real-valued.tex}
+\input{./src/measure/measurable-maps/simple.tex}
+\input{./src/measure/measurable-maps/metric.tex}

src/measure/measurable-maps/measurable-maps.tex

@@ -16,6 +16,15 @@
     Let $X, Y$ be topological spaces and $f: X \to Y$ be continuous, then $f$ is Borel measurable.
 \end{lemma}
 
+\begin{lemma}
+\label{lemma:measurable-function-generating-set}
+    Let $(X, \cm)$ and $(Y, \cn = \sigma(\ce))$ be measurable spaces, and $f: X \to Y$ such that $f^{-1}(\ce) \subset \cm$, then $f$ is $(\cm, \cn)$-measurable.
+\end{lemma}
+\begin{proof}
+    Let $\mathcal{F} = \bracs{E \in \ce| f^{-1}(E) \in \cm}$.
+\end{proof}
+
+
 \begin{definition}[Generated $\sigma$-Algebra]
 \label{definition:generated-sigma-algebra-function}
     Let $X$ be a set, $\bracs{(Y_i, \cn_i)}_{i \in I}$ be measurable spaces, and $\seqi{f}$ with $f_i: X \to Y_i$ for each $i \in I$. The \textbf{$\sigma$-algebra generated by} $\seqi{f}$,

src/measure/measurable-maps/metric.tex

@@ -0,0 +1,115 @@
+\section{Measurable Functions into Metric Spaces}
+\label{section:measurable-metric}
+
+\begin{proposition}
+\label{proposition:metric-measurable-fibre-product}
+    Let $(X, \cm)$, $(Z, \cn)$ be measurable spaces, $\seqf{Y_j}$ separable metrisable topological spaces, $F: \prod_{j = 1}^n Y_j \to Z$ be a $(\cb_{\prod_{j = 1}^n Y_j}, \cn)$-measurable function. For any $\seqf{f_j}$ where for each $1 \le j \le n$, $f_j: X \to Y_j$ is $(\cm, \cb_{Y_j})$-measurable, the composition
+    \[
+    X \to Z \quad x \mapsto F(f_1(x), \cdots, f_n(x))
+    \]
+    is $(\cm, \cn)$-measurable.
+\end{proposition}
+\begin{proof}
+    By \ref{proposition:product-sigma-algebra-metric}, $\cb_{\prod_{j = 1}^n Y_j} = \bigotimes_{j = 1}^n \cb_{Y_j}$, so
+    \[
+    X \to \prod_{j = 1}^n Y_j \quad x \mapsto (f_1(x), \cdots, f_n(x))
+    \]
+    is $(\cm, \cb_{\prod_{j = 1}^n Y_j})$-measurable. Therefore the composition is $(\cm, \cn)$-measurable.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:metric-measurables}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, $f, g: X \to Y$ be $(\cm, \cb_Y)$-measurable functions, then the following functions are measurable:
+    \begin{enumerate}
+        \item For any metric $d$ on $Y$, $x \mapsto d(f(x), f(y))$.
+        \item If $Y$ is a TVS over $K \in \RC$ and $\lambda \in K$, $\lambda f + g$. In particular, $\bracs{f = g} \in \cm$.
+        \item If $Y \in \RC$, $fg$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    By \ref{proposition:metric-measurable-fibre-product}.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:metric-measurable-compose}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, and $f: X \to Y$ be a function, then the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_Y)$-measurable.
+        \item For each $\phi \in C(X; [0, 1])$, $\phi \circ f$ is $(\cm, \cb_\real)$-measurable.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (2) $\Rightarrow$ (1): For each $U \subset X$ open, the function
+    \[
+    d_{U^c}: X \to [0, 1] \quad x \mapsto d(x, U^c) \wedge 1
+    \]
+    is continuous by \ref{proposition:set-distance-continuous}. By \ref{proposition:fattening-closure}, $\bracsn{d_{U^c} > 0} = U$. Thus $\bracs{f \in U} = \bracsn{d_{U^c} \circ f > 0}$.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:metric-measurable-limit}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, and $\seq{f_n}$ be $(\cm, \cb_Y)$-measurable functions, then:
+    \begin{enumerate}
+        \item If $Y$ is completely metrisable, then $\bracsn{\limv{n}f_n \text{ exists}} \in \cm$.
+        \item If $f = \limv{n}f_n$ exists, then it is $(\cm, \cb_Y)$-measurable.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): Let $d$ be a complete metric on $Y$, then for any $x \in X$, $\limv{n}f_n(x)$ exists if and only if $\seq{f_n(x)}$ is Cauchy. In which case,
+    \[
+    \bracs{\limv{n}f_n \text{ exists}} = \bigcap_{k \in \natp}\bigcup_{N \in \natp}\bigcap_{m \in \natp}\bigcap_{n \in \natp}\bracsn{d(f_m, f_n) < 1/k}
+    \]
+    is measurable by \ref{proposition:metric-measurables}.
+
+    (2): For each $\phi \in C(X; [0, 1])$, $\phi \circ f = \limv{n}\phi \circ f_n$ is $(\cm, \cb_\real)$-measurable by \ref{proposition:limit-measurable}. Thus $f$ is $(\cm, \cb_\real)$-measurable by \ref{proposition:metric-measurable-compose}.
+\end{proof}
+
+
+\begin{proposition}
+\label{proposition:measurable-simple-separable}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, $N: Y \to 2^Y$\footnote{This mapping is typically obtained as slices of the level sets of a continuous function $Y \times Y \to \real$.}, and $f: X \to Y$ such that
+    \begin{enumerate}
+        \item[(a)] For each $y \in Y$, $y \in \ol{N(y)^o}$.
+        \item[(b)] $\bigcap_{y \in Y}N(y) \ne \emptyset$.
+        \item[(c)] For any $y \in Y$, $\bracs{x \in X|y \in N(f(x))} \in \cm$.
+    \end{enumerate}
+    then the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_Y)$-measurable.
+        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
+        \begin{enumerate}
+            \item[(i)] For each $x \in X$ and $n \in \natp$, $f_n(x) \in N(f(x))$.
+            \item[(ii)] $f_n \to f$ pointwise.
+        \end{enumerate}
+        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset of $Y$. Assume without loss of generality that $y_1 \in \bigcap_{y \in Y}N(y)$. For each $N \in \nat$ and $x \in X$, let
+    \[
+    C(N, x) = \bracs{1 \le n \le N|y_n \in N(f(x))}
+    \]
+    By assumption (b), $1 \in C(N, x) \ne \emptyset$. Let
+    \[
+    k(N, x) = \min\bracs{n \in C(N, x) \bigg | d(f(x), y_n) = \min_{m \in C(N, x)}d(f(x), y_m)}
+    \]
+    then for any $k \in \natp$,
+    \[
+    \bracs{x \in X|k(n, x) \le k} = \bigcup_{j = 1}^k\bracs{x \in X \bigg |y_j \in C(n, x), d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)}
+    \]
+    For each $1 \le m \le N$, $y \mapsto d(y, y_m)$ is continuous. Thus $x \mapsto d(f(x), y_m)$ and $x \mapsto \min_{m \in C(N, x)}d(f(x), y_m)$ are $(\cm, \cb_\real)$-measurable by \ref{proposition:limit-measurable} and assumption (c). By \ref{proposition:metric-measurables},
+    \[
+    \bracs{x \in X \bigg | d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)} \in \cm
+    \]
+    for each $1 \le j \le k$. Combining this with assumption (c) shows that $\bracs{x \in X|k(n, x) \le k} \in \cm$.
+
+    Let $f_N(x) = y_{k(N, x)}$, then for each $N \in \natp$, $f_N(x) \subset \bracs{y_n|1 \le n \le N}$, so $f_N(x)$ is finitely valued. Since $x \mapsto k{(N, x)}$ is $(\cm, 2^\nat)$-measurable, $f_N$ is $(\cm, \cb_Y)$-measurable.
+
+    Fix $x \in X$, then
+    \[
+    f(x) \in \ol{N^o(f(x))} = \ol{\bracs{y_n| n \in \natp, y_n \in N^o(f(x))}}
+    \]
+    by assumption (a) and \ref{definition:dense}. Thus for any $\eps > 0$, there exists $N \in \nat$ such that $y_N \in N^o(f(x))$ and $d(f(x), y_N) < \eps$. In which case, $d(f(x), f_n(x)) < \eps$ for all $n \ge N$. Therefore $f_n \to f$ pointwise.
+
+    (3) $\Rightarrow$ (1): By \ref{proposition:metric-measurable-limit}.
+\end{proof}

src/measure/measurable-maps/real-valued.tex

@@ -0,0 +1,50 @@
+\section{Real-Valued Measurable Functions}
+\label{section:real-complex-measurable}
+
+\begin{lemma}
+\label{lemma:extended-real-measurable}
+    Let $(X, \cm)$ be a measurable space and $f: X \to \real$, then the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_{\ol \real})$-measurable.
+        \item $f$ is $(\cm, \cb_{\real})$-measurable.
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1) $\Rightarrow$ (2): $\cb_{\real} \subset \cb_{\ol \real}$.
+
+    (2) $\Rightarrow$ (1): For any $E \subset \ol{\real}$, $f^{-1}(E) = f^{-1}(E \cap \real) \in \cm$.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:limit-measurable}
+    Let $(X, \cm)$ be a measurable space, $\seq{f_n}$ be $(\cm, \cb_{\ol \real})$-measurable functions, then the following functions are $(\cm, \cb_{\ol \real})$-measurable:
+    \begin{enumerate}
+        \item $F = \sup_{n \in \natp}f_n$.
+        \item $f = \inf_{n \in \natp}f_n$.
+        \item $G = \limsup_{n \to \infty}f_n$.
+        \item $g = \limsup_{n \to \infty}f_n$.
+        \item $\limv{n}f_n$ (if it exists).
+    \end{enumerate}
+    In addition, if the above functions are $\real$-valued, then they are $(\cm, \cb_{\real})$-measurable.
+\end{proposition}
+\begin{proof}
+    (1): Let $\alpha \in \real$, then for any $x \in X$, $F(x) > \alpha$ if and only if there exists $n \in \natp$ such that $f_n(x) > \alpha$. Thus
+    \[
+    \bracs{F > \alpha} = \bigcup_{n \in \natp}\bracs{f_n > \alpha}
+    \]
+
+    (2): Let $\alpha \in \real$, then
+    \[
+    \bracs{f < \alpha} = \bigcup_{n \in \natp}\bracs{f_n < \alpha}
+    \]
+
+    By \ref{proposition:borel-sigma-extended-generators} and \ref{lemma:measurable-function-generating-set}, $F$ and $f$ are both $(\cm, \cb_{\ol \real})$-measurable.
+
+    (3): $\limsup_{n \to \infty}f_n = \inf_{n \in \natp}\sup_{k \ge n}f_k$.
+
+    (4): $\liminf_{n \to \infty}f_n = \sup_{n \in \natp}\inf_{k \ge n}f_k$.
+
+    (5): If $\limv{n}f_n$ exists, then it is equal to (3) and (4). In which case, it is measurable.
+
+    Finally, if the above functions are $\real$-valued, then they are $(\cm, \cb_\real)$-measurable by \ref{lemma:extended-real-measurable}.
+\end{proof}

src/measure/measurable-maps/simple.tex

@@ -0,0 +1,34 @@
+\section{Simple Functions}
+\label{section:simple-function}
+
+\begin{definition}[Indicator Function]
+\label{definition:indicator-function}
+    Let $(X, \cm)$ be a measurable space and $E \in \cm$, then the function
+    \[
+    \chi_E = \one_E: X \to \bracs{0, 1} \quad x \mapsto \begin{cases}
+    1 &x \in E \\
+    0 &x \not\in E
+    \end{cases}
+    \]
+    is the \textbf{characteristic/indicator function} of $E$.
+\end{definition}
+
+\begin{definition}[Simple Function]
+\label{definition:simple-function}
+    Let $(X, \cm)$ be a measurable space and $Y$ be a set, then a function $\phi: X \to Y$ is \textbf{simple/finitely valued} if:
+    \begin{enumerate}
+        \item $\phi(X)$ is finite.
+        \item For each $y \in \phi(X)$, $\phi^{-1}(y) \in \cm$.
+    \end{enumerate}
+\end{definition}
+
+\begin{definition}[Standard Form]
+\label{definition:simple-function-standard-form}
+    Let $(X, \cm)$ be a measurable space, $V$ be a vector space over $K \in \RC$, and $f: X \to Y$ be a simple function, then
+    \[
+    f = \sum_{y \in f(X)}y\one_Y
+    \]
+    is the \textbf{standard form} of $f$.
+
+    The set $\Sigma(X, \cm, V)$ is the vector space of all simple functions from $X$ to $Y$.
+\end{definition}

src/measure/measure/radon.tex

@@ -5,8 +5,8 @@
 \label{definition:radon-measure}
     Let $X$ be a LCH space and $\mu: \cb_X \to [0, \infty]$ be a Borel measure, then $\mu$ is a \textbf{Radon measure} if:
     \begin{enumerate}
-        \item For any $K \subset X$ compact, $\mu(K) < \infty$.
+        \item[(R1)] For any $K \subset X$ compact, $\mu(K) < \infty$.
-        \item $\mu$ is outer regular on all Borel sets.
+        \item[(R2)] $\mu$ is outer regular on all Borel sets.
-        \item $\mu$ is inner regular on all open sets.
+        \item[(R3')] $\mu$ is inner regular on all open sets.
     \end{enumerate}
 \end{definition}

src/measure/sets/algebra.tex

@@ -72,7 +72,87 @@
     Let $X$ be a set and $\ce \subset 2^X$, then the $\sigma$-algebra $\sigma(\ce)$ \textbf{generated by} $\ce$ is the smallest $\sigma$-algebra on $X$ containing $\ce$.
 \end{definition}
 
+
 \begin{definition}[Borel $\sigma$-Algebra]
 \label{definition:borel-sigma-algebra}
     Let $(X, \topo)$ be a topological space, then the \textbf{Borel $\sigma$-algebra} $\cb_X$ on $X$ is the $\sigma$-algebra generated by $\topo$.
 \end{definition}
+
+
+\begin{definition}[Borel $\sigma$-Algebra on $\ol{\real}$]
+\label{definition:borel-sigma-algebra-extended}
+    The family
+    \[
+    \cb_{\ol{\real}} = \bracsn{E \subset \ol \real| E \cap \real \in \cb_\real}
+    \]
+    is the \textbf{Borel $\sigma$-algebra} on $\ol{\real}$.
+\end{definition}
+
+
+\begin{proposition}
+\label{proposition:borel-sigma-real-generators}
+    The following families of sets generate the Borel $\sigma$-algebra on $\real$:
+    \begin{enumerate}
+        \item $\bracs{(-\infty, a]| a \in \real}$.
+        \item $\bracs{(a, \infty)|a \in \real}$.
+        \item $\bracs{[a, \infty)| a \in \real}$.
+        \item $\bracs{(-\infty, a)| a \in \real}$.
+        \item $\bracs{[a, b)| -\infty < a < b < \infty}$.
+        \item $\bracs{[a, b]| -\infty < a < b < \infty}$.
+        \item $\bracs{(a, b]| -\infty < a < b < \infty}$.
+        \item $\bracs{(a, b)| -\infty < a < b < \infty}$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    It is sufficient to show that the $\sigma$-algebra generated by any of the above two families coincide, and that the resulting $\sigma$-algebra is the Borel $\sigma$-algebra on $\real$.
+
+    (1) $\to$ (2): For any $a \in \real$, $(a, \infty) = (-\infty, a)^c$.
+
+    (2) $\to$ (3): For any $a \in \real$, $[a, \infty) = \bigcap_{n \in \natp}(a - 1/n, \infty)$.
+
+    (3) $\to$ (4): For any $a \in \real$, $(-\infty, a) = [a, \infty)^c$.
+
+    (4) $\to$ (5): For any $a, b \in \real$, $[a, b) = (-\infty, b) \cap (-\infty, a)^c$.
+
+    (5) $\to$ (6): For any $a, b \in \real$, $[a, b]= \bigcap_{n \in \natp}(a - 1/n, b]$.
+
+    (6) $\to$ (7): For any $a, b \in \real$, $(a, b] = \bigcup_{n \in \natp}[a + 1/n, b]$.
+
+    (7) $\to$ (8): For any $a, b \in \real$, $(a, b) = \bigcup_{n \in \natp}(a, b - 1/n]$.
+
+    (8) $\to$ (1): For any $a \in \real$, $(-\infty, a] = \bigcup_{n \in \natp}\bigcap_{k \in \natp}(-n, a + 1/k]$.
+
+    For any $U \subset X$ open and $q \in U \cap \rational$, there exists $r_q > 0$ such that $(q - r_q, q + r_q) \subset U$. In which case,
+    \[
+    U = \bigcup_{q \in U \cap \rational}(q - r_q, q + r_q)
+    \]
+    so (8) generates all open sets in $\real$. Conversely, every element of (8) is open, so the $\sigma$-algebra generated by (8) is the Borel $\sigma$-algebra on $\real$.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:borel-sigma-extended-generators}
+    The following families of sets generate the Borel $\sigma$-algebra on $\ol \real$:
+    \begin{enumerate}
+        \item $\bracs{[-\infty, a]| a \in \real}$.
+        \item $\bracs{(a, \infty]|a \in \real}$.
+        \item $\bracs{[a, \infty]| a \in \real}$.
+        \item $\bracs{[-\infty, a)| a \in \real}$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1) $\to$ (2): For any $a \in \real$, $(a, \infty] = [-\infty, a]^c$.
+
+    (2) $\to$ (3): For any $a \in \real$, $[a, \infty] = \bigcap_{n \in \natp}(a - 1/n, \infty]$.
+
+    (3) $\to$ (4): For any $a \in \real$, $[-\infty, a) = [a, \infty]^c$.
+
+    (4) $\to$ (1): For any $a \in \real$, $[-\infty, a] = \bigcap_{n \in \natp}[-\infty, a + 1/n)$.
+
+    By definition, all elements of (1), (2), (3), and (4) belong to $\cb_{\ol{\real}}$. Let $\cm$ be the $\sigma$-algebra generated by (1), (2), (3), and (4), then
+    \[
+    \bracs{\infty} = \bigcap_{n \in \nat}[n, \infty] \quad \bracs{-\infty} = \bigcap_{n \in \nat}[-\infty, n]
+    \]
+    are elements of $\cm$. For any $a \in \real$, $(a, \infty) = (a, \infty] \setminus \bracs{\infty}$, so $\cm \supset \cb_\real$ by \ref{proposition:borel-sigma-real-generators}.
+
+    In addition, for any $E \in \cb_{\ol{\real}}$, $E = (E \cap \real) \cup (E \setminus \real)$, where $E \cap \real \in \cb_\real$. Since $\bracs{\infty}, \bracs{-\infty} \in \cm$ and $\cb_\real \subset \cm$, $E \in \cm$ and $\cm = \cb_{\ol \real}$.
+\end{proof}

src/topology/index.tex

@@ -4,3 +4,4 @@
 \input{./src/topology/main/index.tex}
 \input{./src/topology/uniform/index.tex}
 \input{./src/topology/functions/index.tex}
+\input{./src/topology/metric/index.tex}

src/topology/main/interiorclosureboundary.tex

@@ -63,7 +63,7 @@
 
 \begin{definition}[Dense]
 \label{definition:dense}
-    Let $X$ be a topologicial space and $A \subset X$, then the following are equivalent:
+    Let $X$ be a topological space and $A \subset X$, then the following are equivalent:
     \begin{enumerate}
         \item $\ol{A} = X$.
         \item For every $\emptyset \ne U \subset X$ open, $A \cap U \ne \emptyset$.

src/topology/metric/index.tex

@@ -0,0 +1,5 @@
+\chapter{Metric Spaces}
+\label{chap:metric-space}
+
+\input{./src/topology/metric/metric.tex}
+\input{./src/topology/metric/set-distance.tex}

src/topology/metric/metric.tex

@@ -0,0 +1,14 @@
+\section{Metrics}
+\label{section:metric}
+
+\begin{definition}[Metric Space]
+\label{definition:metric}
+    Let $X$ be a set and $d: X \times X$, then $d$ is a \textbf{metric} if:
+    \begin{enumerate}
+        \item[(PM1)] For any $x \in X$, $d(x, x) = 0$.
+        \item[(M)] For any $x, y \in X$ with $x \ne y$, $d(x, y) > 0$.
+        \item[(PM2)] For any $x, y \in X$, $d(x, y) = d(y, x)$.
+        \item[(PM3)] For any $x, y, z \in X$, $d(x, z) \le d(x, y) + d(y, z)$.
+    \end{enumerate}
+    The pair $(X, d)$ is a \textbf{metric space}, which comes with the metric uniformity induced by $d$, and the corresponding topology.
+\end{definition}

src/topology/metric/set-distance.tex

@@ -0,0 +1,55 @@
+\section{Distance Between Sets}
+\label{section:distance-between-sets}
+
+\begin{definition}[Distance Between Sets]
+\label{definition:distance-betwene-sets}
+    Let $X$ be a set, $d: X \times X \to [0, \infty)$ be a pseudometric, and $A, B \subset X$, then
+    \[
+    d(A, B) = \inf_{\substack{a \in A \\ b \in B}}d(a, b)
+    \]
+    is the \textbf{distance} between $A$ and $B$.
+\end{definition}
+
+\begin{proposition}
+\label{proposition:set-distance-continuous}
+    Let $(X, d)$ be a pseudometric space, $A \subset X$, and
+    \[
+    d_A: X \to [0, \infty) \quad x \mapsto d(x, A)
+    \]
+    then $d_A \in UC(X; [0, \infty))$, where for any $x, y \in X$, $|d_A(x) - d_A(y)| \le d(x, y)$.
+\end{proposition}
+\begin{proof}
+    Let $x, y \in X$, then
+    \[
+    d(y, A) = \inf_{a \in A}d(y, a) \le d(x, y) + \inf_{a \in A}d(x, a) = d(x, y) + d(x, A)
+    \]
+    As the argument is symmetric, $|d_A(x) - d_A(y)| \le d(x, y)$.
+\end{proof}
+
+\begin{definition}[Fattening]
+\label{definition:fattening}
+    Let $X$ be a set, $d: X \times X \to [0, \infty)$ be a pseudometric, $A \subset X$, and $\eps > 0$, then
+    \[
+    B(A, \eps) = \bracs{x \in X|d(x, A) < \eps} = \bigcup_{a \in A}B(a, \eps)
+    \]
+    is the \textbf{$\eps$-fattening} of $A$ with respect to $d$.
+\end{definition}
+
+\begin{proposition}
+\label{proposition:fattening-closure}
+    Let $(X, d)$ be a metric space and $A \subset X$, then
+    \[
+    \ol{A} = \bigcap_{\eps > 0}B(A, \eps)
+    \]
+\end{proposition}
+\begin{proof}
+    By \ref{proposition:uniformclosure}.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:distance-compact}
+    Let $(X, d)$ be a metric space, $C \subset X$ be closed, and $K \subset X$ be compact. If $C \cap K = \emptyset$, then $d(K, C) > 0$.
+\end{proposition}
+\begin{proof}
+    Suppose that $d(K, C) = 0$, then there exists $\seq{(x_n, y_n)} \subset K \times C$ such that $d(x_n, y_n) \to 0$ as $n \to \infty$. By \ref{definition:compact}, there exists a subsequence $\seq{n_k}$ and $x \in K$ such that $x_{n_k} \to x$ as $k \to \infty$. In which case, $d(x, C) = 0$, and $x \in \ol{K}$ by \ref{proposition:fattening-closure}, so $K \cap C \ne \emptyset$.
+\end{proof}

src/topology/uniform/metric.tex

@@ -13,7 +13,7 @@ The axioms of uniform spaces strongly resembles working in a metric space. In fa
     \end{enumerate}
     If $d$ satisfies the above and
     \begin{enumerate}
-        \item[(M)] For any $x, y \in X$ with $x \ne y$, $d(x, y)$
+        \item[(M)] For any $x, y \in X$ with $x \ne y$, $d(x, y) > 0$.
     \end{enumerate}
     then $d$ is a \textbf{metric}.
 \end{definition}