diff options
Diffstat (limited to 'library/topology/separation.tex')
| -rw-r--r-- | library/topology/separation.tex | 80 |
1 files changed, 73 insertions, 7 deletions
diff --git a/library/topology/separation.tex b/library/topology/separation.tex index f70cb50..3268bb9 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -73,14 +73,29 @@ \begin{proposition}\label{teeone_implies_singletons_closed} Let $X$ be a \teeone-space. - Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. + Assume $x \in \carrier[X]$. + Then $\{x\}$ is closed in $X$. \end{proposition} \begin{proof} - Omitted. - % TODO - % Choose for every y distinct from x and open subset U_y containing y but not x. - % The union U of all the U_y is open. - % {x} is the complement of U in \carrier[X]. + Let $V = \{ U \in \opens[X] \mid x \notin U\}$. + For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$. + For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. + + $\unions{V} \in \opens[X]$. + For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$. + We show that $\carrier[X] \setminus \{x\} = \unions{V}$. + \begin{subproof} + We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$. + \begin{subproof} + Fix $y \in \carrier[X] \setminus \{x\}$. + $y \neq x$. + $y \in \carrier[X]$. + $y \in \unions{V}$. + \end{subproof} + For all $y \in \unions{V}$ we have $y \notin \{x\}$. + For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. + Follows by set extensionality. + \end{subproof} \end{proof} % % Conversely, if \{x\} is open, then for any y distinct from x we can use @@ -120,5 +135,56 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - Omitted. % TODO + We show that for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $U\ni x\notin V$ and $V\ni y\notin U$. + \begin{subproof} + $X$ is hausdorff. + 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$. + \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 |