Added uniform structures for completely regular spaces. Added calculus lemma.

src/topology/uniform/definition.tex

@@ -270,19 +270,16 @@ V = (\bracs{x} \times V)(x) = (U \cup (\bracs{x} \times V))(x) = W(x) \in \cn(x)
         \item $X$ is T1.
         \item $X$ is Hausdorff.
         \item $X$ is regular.
+        \item $X$ is completely regular. 
         \item $\Delta = \bigcap_{U \in \fU}U$.
     \end{enumerate}
 
     If the above holds, then $X$ is \textbf{separated}.
 \end{definition}
 \begin{proof}
-    $(1) \Rightarrow (5)$: Let $x, y \in X$ with $x \ne y$. Assume without loss of generality that there exists $U(x) \in \cn(x)$ such that $y \not\in U$. In which case, $(x, y) \not\in U$ and $\Delta \supset \bigcap_{U \in \fU}U$.
+    (1) $\Rightarrow$ (6): Let $x, y \in X$ with $x \ne y$. Assume without loss of generality that there exists $U(x) \in \cn(x)$ such that $y \not\in U$. In which case, $(x, y) \not\in U$ and $\Delta \supset \bigcap_{U \in \fU}U$.
 
-    $(5) \Rightarrow (2)$: By \autoref{proposition:goodentourages}, $\ol \Delta \subset \bigcap_{U \in \fU}\ol U = \Delta$, so $\ol \Delta$ is closed. By (6) of \autoref{definition:hausdorff}, $X$ is Hausdorff.
-
-    $(1) \Rightarrow (4)$: $X$ is T1 and satisfies (2) of \autoref{definition:regular} by \autoref{proposition:uniform-neighbourhoods}, so $X$ is regular.
-
-    $(4) \Rightarrow (3) \Rightarrow (2) \Rightarrow (1)$:  (T3) $\Rightarrow $ (T2) $\Rightarrow$ (T1) $\Rightarrow$ (T0).
+    (6) $\Rightarrow$ (5): Let $E \subset X$ be closed and $x \in X \setminus E$. Since $\Delta = \bigcap_{U \in \fU}U$, there exists $U \in \fU$ such that $U(x) \subset E^c$. By \autoref{theorem:uniform-pseudometric}, there exists a pseudometric $d: X \times X \to [0, \infty)$ such that $d(x, E) > 0$. Thus the function $y \mapsto d(x, y)$ is a continuous function that separates $x$ and $E$. 
 \end{proof}