diff options
Diffstat (limited to 'library/topology')
| -rw-r--r-- | library/topology/separation.tex | 43 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 26 |
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} |