Definition of T3 and regular spaces.

2 files changed, 50 insertions, 19 deletions

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 535a51f..3268bb9 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -145,3 +145,46 @@
         $x\in U$ and $y\in V$ and $U$ is disjoint from $V$.
     \end{subproof}
 \end{proof}
+
+\begin{definition}\label{regular}
+    $X$ is regular iff for all $C,p$ such that $p \in \carrier[X]$ and $p \notin C \in \closeds{X}$ we have there exists $U,C \in \opens[X]$ such that $p \in U$ and $C \subseteq V$ and $U \inter V = \emptyset$.
+\end{definition}
+
+\begin{definition}\label{regular_space}
+    $X$ is a regular space iff $X$ is a topological space and $X$ is regular.
+\end{definition}
+
+
+\begin{definition}\label{teethree}
+    $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ .
+\end{definition}
+
+\begin{definition}\label{teethree_space}
+    $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ .
+\end{definition}
+
+\begin{proposition}\label{teethree_space_is_teetwo_space}
+    Let $X$ be a \teethree-space.
+    Then $X$ is a \teetwo-space.
+\end{proposition}
+\begin{proof}
+    For all $x,y \in \carrier[X]$ such that $x \neq y$ we have $x \notin \{y\}$.
+    It suffices to show that $X$ is hausdorff.
+    It suffices to show that for all $x \in \carrier[X]$ we have for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$.
+    Fix $x \in \carrier[X]$.
+    It suffices to show that for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$.
+    Fix $y \in \carrier[X]$.
+
+    %There exist $U' \in \opens[X]$ such that $x\in U'\not\ni y$ or $x\notin U'\ni y$ by \cref{}.
+    %There exist $C \in \closeds{X}$ such that $y \in C \not\ni X$.
+    We show that there exist $U,V,C$ such that $U,V \in \opens[X]$ and $C\in \closeds{X}$ and $x \in U$ and $y \in C \subseteq V$ and $U$ is disjoint from $V$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    $y \in V$.
+    Follows by assumption.
+\end{proof}
+
+%    for all $x,y\in\carrier[X]$ such that $x\neq y$
+%    there exist $U, V\in\opens[X]$ such that
+%    $x\in U$ and $y\in V$ and $U$ is disjoint from $V$.
\ No newline at end of file
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 7ff588d..c40aba4 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -239,18 +239,12 @@
     Then $A \subseteq \unions{F}$.
 \end{proposition}
 \begin{proof}
-    \begin{byCase}
-        %\caseOf{$F$ is empty.} 
-           %For all $X$ we have $X \notin F$.
-        %If $X \in F$ and $A \in X$ then $A \in F$.
-        %Contradiction by assumption.
-        %Omitted.
-        \caseOf{$F$ is inhabited.}
-        There exist $X \in F$ such that $X \subseteq \unions{F}$.
-        $A \subseteq X \subseteq \unions{F}$.
-    \end{byCase}
+    There exist $X \in F$ such that $X \subseteq \unions{F}$.
+    $A \subseteq X \subseteq \unions{F}$.
 \end{proof}
 
+
+
 \begin{proposition}\label{subseteq_inters_iff_to_left} 
     Let $A,F$ be sets.
     Suppose $F$ is inhabited.    % TODO:Remove!!
@@ -379,10 +373,6 @@
             Then $a \notin \unions{F'}$.
             Therefore $a \in \carrier[X] \setminus (\unions{F'})$.
         \end{subproof}
-
-        
-
-
         We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$.
         \begin{subproof}
             \begin{byCase}
@@ -426,17 +416,15 @@
     \end{byCase}
 \end{proof}
 
-\begin{definition}\label{set_of_closeds}
-    $\closeds[X] = \{ Y \in \pow{\carrier[X]} \mid \text{$Y$ is closed in $X$}\}$.
-\end{definition}
+
 
 \begin{proposition}\label{closure_is_minimal_closed_set}
     Let $X$ be a topological space.
     Suppose $A \subseteq \carrier[X]$.
-    For all $Y \in \closeds[X]$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$.  
+    For all $Y \in \closeds{X}$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$.  
 \end{proposition}
 \begin{proof}
-    Follows by \cref{closure,set_of_closeds,inters_subseteq_elem,closures}.
+    Follows by \cref{closure,closeds,inters_subseteq_elem,closures}.
 \end{proof}
 
 \begin{proposition}\label{complement_interior_eq_closure_complement}