Added Hausdorff characterisation for uniform spaces.

src/topology/uniform/definition.tex

@@ -208,7 +208,7 @@ V = (\bracs{x} \times V)(x) = (U \cup (\bracs{x} \times V))(x) = W(x) \in \cn(x)
 
 \begin{proposition}[{{\cite[Corollary 2.1.2]{Bourbaki}}}]
 \label{proposition:goodentourages}
-    Let $(X, \fU)$ be a uniform space, then the following famillies of sets form fundamental systems of entourages for $\fU$:
+    Let $(X, \fU)$ be a uniform space, then the following families of sets form fundamental systems of entourages for $\fU$:
     \begin{enumerate}
         \item $\mathfrak{O} = \bracs{U^o| U \in \fU}$
         \item $\mathfrak{K} = \bracsn{\overline{U}| U \in \fU}$.
@@ -245,9 +245,8 @@ V = (\bracs{x} \times V)(x) = (U \cup (\bracs{x} \times V))(x) = W(x) \in \cn(x)
     By \ref{proposition:goodentourages} and \ref{lemma:openentourageneighbourhoods}, the closed neighbourhoods form a fundamental system of neighbourhoods.
 \end{proof}
 
-
-\begin{proposition}
-\label{proposition:uniform-regular}
+\begin{definition}[Separated]
+\label{definition:uniform-separated}
     Let $(X, \fU)$ be a uniform space, then the following are equivalent:
     \begin{enumerate}
         \item $X$ is T0.
@@ -256,7 +255,8 @@ V = (\bracs{x} \times V)(x) = (U \cup (\bracs{x} \times V))(x) = W(x) \in \cn(x)
         \item $X$ is regular.
         \item $\Delta = \bigcap_{U \in \fU}U$.
     \end{enumerate}
-\end{proposition}
+    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$.