\import{topology/topological-space.tex}
\import{set.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$.
\end{proposition}
\begin{proof}
    Omitted.
    %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$ by \cref{carrier_open,teeone}.
    %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
% 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}
    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{is_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{abbreviation}\label{regular_space}
    $X$ is a regular space iff $X$ is a topological space and $X$ is regular.
\end{abbreviation}


\begin{abbreviation}\label{teethree}
    $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ .
\end{abbreviation}

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

\begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open}
    Let $X$ be a topological space.
    Suppose $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}
\begin{proof}
    Omitted.
    %%Suppose $X$ is regular and kolmogorov.
    %Fix $U \in \opens[X]$.
    %Fix $x \in U$.
    %Let $C = \carrier[X] \setminus U$.
    %Then $C \in \closeds{X}$.
    %$x \notin C$.
    %$x \in \carrier[X]$.
    %We show that there exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$.     
    %We show that $B \subseteq (\carrier[X] \setminus A)$.
    %$(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$.
    %$(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$.
    %$x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$.
    %Let $N = (\carrier[X] \setminus A)$.
    %Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$.
    %$N \in \neighbourhoods{x}{X}$.
\end{proof}

\begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods}
    Let $X$ be a topological space.
    Suppose $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}
    We show that if $X$ is \teethree\ then for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$.
    \begin{subproof}
        %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$.
        Omitted.
    \end{subproof}

    We show that if for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$ then $X$ is \teethree\ .
    \begin{subproof}
        Omitted.
    \end{subproof}
\end{proof}


\begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open}
    Let $X$ be a topological space.
    Suppose $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}
    Omitted.
    %Follows by \cref{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods,teethree_implies_closed_neighbourhood_in_open}.
\end{proof}


\begin{proposition}\label{teethree_space_is_teetwo_space}
    Let $X$ be a \teethree-space.
    Suppose $X$ is inhabited.
    Then $X$ is a \teetwo-space.
\end{proposition}
\begin{proof}
    Omitted.
\end{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]$.


    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}
        There exist $C' \in \closeds{X}$ such that $x \in \carrier[X]$ and $x \notin C' \in \closeds{X}$ and there exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$.
        There exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$.
        $U'$ is disjoint from $V'$.
        $x \in U'$.
        $x \notin C' \subseteq V'$.
        $U',V' \in \opens[X]$.
        $C' \in \closeds{X}$.
        We show that there exist $K \in \closeds{X}$ such that $x \notin K \ni y$.
        \begin{subproof}
            $X$ is Kolmogorov.
            For all $x',y'\in\carrier[X]$ such that $x'\neq y'$ there exist $H\in\opens[X]$ such that $x'\in H\not\ni y'$ or $x'\notin H\ni y'$.
            we show that there exist $H \in \opens[X]$ such that $x \notin H \ni y$ or $y \notin H \ni x$.
            \begin{subproof}
                Omitted.
            \end{subproof}
            $H \subseteq \carrier[X]$ by \cref{opens_type,subseteq}.
            Since $\carrier[X] \ni x \notin H$ or $\carrier[X] \ni y \notin H$, we have there exist $c \in H$. 
            Then $H \neq \carrier[X]$.
            Since $y \in H$ or $x \in H$, we have $H \neq \emptyset$.
            Let $K = \carrier[X] \setminus H$.
            $K$ is inhabited.
            $K \in \closeds{X}$ by \cref{complement_of_open_is_closed}.
            $x \notin K \ni y$ or $y \notin K \ni x$.
            \begin{byCase}
                \caseOf{$y \in K$.} Trivial.
                \caseOf{$y \notin K$.}
                Then there exist $U'',V'' \in \opens[X]$ such that $x \in U''$ and $K \subseteq V''$ and $U'' \inter V'' = \emptyset$ by \cref{is_regular}.
                Let $K' = \carrier[X] \setminus U''$.
                $x \in K'$.
                $K' \in \closeds{X}$.
            \end{byCase}


        \end{subproof}

        Follows by assumption.
    \end{subproof}
    $y \in V$ by assumption.
    Follows by assumption.

    
%\end{proof}