\import{topology/topological-space.tex}


% T0 separation
\begin{definition}\label{is_kolmogorov}
    $X$ is Kolmogorov iff
    for all $x,y\in\carrier[X]$ such that $x\neq y$
    there exist $U\in\opens[X]$ such that
    $x\in U\not\ni y$ or $x\notin U\ni y$.
\end{definition}

\begin{abbreviation}\label{kolmogorov_space}
    $X$ is a Kolmogorov space iff $X$ is a topological space and
    $X$ is Kolmogorov.
\end{abbreviation}

\begin{abbreviation}\label{teezero}
    $X$ is \teezero\ iff $X$ is Kolmogorov.
\end{abbreviation}

\begin{abbreviation}\label{teezero_space}
    $X$ is a \teezero-space iff $X$ is a Kolmogorov space.
\end{abbreviation}

\begin{proposition}\label{kolmogorov_implies_kolmogorov_for_closeds}
    Suppose $X$ is a Kolmogorov space.
    Let $x,y\in\carrier[X]$.
    Suppose $x\neq y$.
    Then there exist $A\in\closeds{X}$ such that
    $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$
        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}.
\end{proof}

\begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov}
    Suppose for all $x,y\in\carrier[X]$ such that $x\neq y$
        there exist $U\in\closeds{X}$ such that
        $x\in U\not\ni y$ or $x\notin U\ni y$.
    Then $X$ is Kolmogorov.
\end{proposition}
\begin{proof}
    Follows by \cref{closeds,is_closed_in,is_kolmogorov,setminus}.
\end{proof}

\begin{proposition}\label{kolmogorov_iff_kolmogorov_for_closeds}
    Let $X$ be a topological space.
    $X$ is Kolmogorov iff
    for all $x,y\in\carrier[X]$ such that $x\neq y$
    there exist $U\in\closeds{X}$ such that
    $x\in U\not\ni y$ or $x\notin U\ni y$.
\end{proposition}
\begin{proof}
    Follows by \cref{kolmogorov_implies_kolmogorov_for_closeds,kolmogorov_for_closeds_implies_kolmogorov}.
\end{proof}

% T1 separation (Fréchet topology)
\begin{definition}\label{teeone}
    $X$ is \teeone\ iff
    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$.
\end{definition}

\begin{abbreviation}\label{teeone_space}
    $X$ is a \teeone-space iff $X$ is a topological space and
    $X$ is \teeone.
\end{abbreviation}

\begin{proposition}\label{teeone_implies_singletons_closed}
    Let $X$ be a \teeone-space.
    Assume $x \in \carrier[X]$.
    Then $\{x\}$ is closed in $X$.
    %Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. Ambigus Phrase. if Omitted is ereased.
\end{proposition}
\begin{proof}
    %Omitted.
    %Fix $x \in 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}




    % Let $U_{y} \in \opens[X]$ such that $x \neq y \in X$.          Error: unexpected '{' expecting digit
    %For all $y$ there exists $U$ such that $x \neq y$ and $y \in U$ and $U \in \opens[X]$.

    % 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].
\end{proof}
%
% Conversely, if \{x\} is open, then for any y distinct from x we can use
% X\setminus\{x\} as the open neighbourhood of y.

% T2 separation
\begin{definition}\label{is_hausdorff}
    $X$ is Hausdorff iff
    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{definition}

\begin{abbreviation}\label{hausdorff_space}
    $X$ is a Hausdorff space iff $X$ is a topological space and
    $X$ is Hausdorff.
\end{abbreviation}

\begin{abbreviation}\label{teetwo}
    $X$ is \teetwo\ iff $X$ is Hausdorff.
\end{abbreviation}

\begin{abbreviation}\label{teetwo_space}
    $X$ is a \teetwo-space iff $X$ is a Hausdorff space.
\end{abbreviation}

\begin{proposition}\label{teeone_space_is_teezero_space}
    Let $X$ be a \teeone-space.
    Then $X$ is a \teezero-space.
\end{proposition}
\begin{proof}
    Follows by \cref{is_kolmogorov,teeone}.
\end{proof}

\begin{proposition}\label{teetwo_space_is_teeone_space}
    Let $X$ be a \teetwo-space.
    Then $X$ is a \teeone-space.
\end{proposition}
\begin{proof}
    Omitted. % TODO
\end{proof}