diff options
Diffstat (limited to 'library/topology/separation.tex')
| -rw-r--r-- | library/topology/separation.tex | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/library/topology/separation.tex b/library/topology/separation.tex index ad8cad1..5806216 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -32,11 +32,13 @@ $x\in A\not\ni y$ or $x\notin A\ni y$. \end{proposition} \begin{proof} - Take $U\in\opens[X]$ such that $x\in U\not\ni y$ or $x\notin U\ni y$ + Take $U$ such that + $U\in\opens[X]\land ((x\in U\land y\notin U)\lor(x\notin U\land y\in U))$ by \cref{is_kolmogorov}. Then $\carrier[X]\setminus U\in\closeds{X}$ by \cref{complement_of_open_elem_closeds}. Now $x\in (\carrier[X]\setminus U)\not\ni y$ or $x\notin (\carrier[X]\setminus U)\ni y$ by \cref{setminus}. + Follows by assumption. \end{proof} \begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov} @@ -138,15 +140,7 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - 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} + Follows by \cref{is_hausdorff,teeone,disjoint}. \end{proof} \begin{definition}\label{is_regular} @@ -168,7 +162,7 @@ \begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Suppose $X$ is \teethree\ . For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} @@ -193,7 +187,7 @@ \begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. \end{proposition} \begin{proof} @@ -207,12 +201,13 @@ \begin{subproof} Omitted. \end{subproof} + Follows by assumption. \end{proof} \begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} \begin{proof} @@ -223,7 +218,7 @@ \begin{proposition}\label{teethree_space_is_teetwo_space} Let $X$ be a \teethree-space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Then $X$ is a \teetwo-space. \end{proposition} \begin{proof} |