\import{set.tex}
\import{set/powerset.tex}
\import{set/cons.tex}

\section{Topological spaces}\label{form_sec_topospaces}

\begin{struct}\label{topological_space}
    A topological space $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\opens$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$.
        \item\label{carrier_open} $\carrier[X]\in\opens[X]$.
        \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$.
        \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$.
    \end{enumerate}
\end{struct}

\begin{abbreviation}\label{is_open_in}
    $U$ is open iff $U\in\opens$.
\end{abbreviation}

\begin{abbreviation}\label{is_open}
    $U$ is open in $X$ iff $U\in\opens[X]$.
\end{abbreviation}

\begin{proposition}\label{emptyset_open}
    Let $X$ be a topological space.
    Then $\emptyset$ is open in $X$.
\end{proposition}
\begin{proof}
    We have $\unions{\emptyset} = \emptyset\subseteq\opens[X]$ by \cref{unions_emptyset,emptyset_subseteq}.
    Follows by \cref{opens_unions}.
\end{proof}

\begin{proposition}\label{union_open}
    Let $X$ be a topological space.
    Suppose $A$, $B$ are open.
    Then $A\union B$ is open.
\end{proposition}
\begin{proof}
    $\{A, B\}\subseteq\opens$ by \cref{cons_iff,subseteq}.
    $\unions{\{A, B\}}$ is open by \cref{opens_unions}.
    $\unions{\{A, B\}}=A\union B$ by \cref{union_as_unions}.
    Follows by assumption.
\end{proof}

\begin{definition}[Interiors]\label{interiors}
    $\interiors{A}{X} = \{ U\in\opens[X]\mid U\subseteq A\}$.
\end{definition}

\begin{definition}[Interior]\label{interior}
    $\interior{A}{X} = \unions{\interiors{A}{X}}$.
\end{definition}

\begin{proposition}[Interior]\label{interior_elem_intro}
    Suppose $U\in\opens[X]$ and $a\in U\subseteq A$.
    Then $a\in\interior{A}{X}$.
\end{proposition}
\begin{proof}
    $U\in\interiors{A}{X}$ by \cref{interiors}.
    Follows by \cref{interior,unions_intro}.
\end{proof}

\begin{proposition}[Interior]\label{interior_elem_elim}
    Suppose $a\in\interior{A}{X}$.
    Then there exists $U\in\opens[X]$
    such that $a\in U\subseteq A$.
\end{proposition}
\begin{proof}
    Omitted.
    %Take $U\in\interiors{A}{X}$ such that $a\in U$.
\end{proof}

\begin{proposition}[Interior]\label{interior_elem_iff}
    $a\in\interior{A}{X}$ iff
    there exists $U\in\opens[X]$
    such that $a\in U\subseteq A$.
\end{proposition}
\begin{proof}
    Follows by \cref{interior_elem_intro,interior_elem_elim}.
\end{proof}

\begin{proposition}\label{interior_of_open}
    Let $X$ be a topological space.
    Suppose $U$ is open in $X$.
    Then $\interior{U}{X} = U$.
\end{proposition}
\begin{proof}
    $U\in\interiors{U}{X}$ by \cref{interiors,subseteq_refl}.
    Follows by \cref{subseteq,interior_elem_iff,neq_witness}.
\end{proof}

\begin{proposition}\label{interior_is_open}
    Let $X$ be a topological space.
    Then $\interior{A}{X}$ is open.
\end{proposition}
\begin{proof}
    $\interiors{A}{X}\subseteq\opens[X]$ by \cref{interiors,subseteq}.
    Follows by \cref{interior,opens_unions}.
\end{proof}

\begin{proposition}\label{interior_subseteq}
    Then $\interior{A}{X}\subseteq A$.
\end{proposition}
\begin{proof}
    For all $U\in\interiors{A}{X}$ we have $U\subseteq A$
        by \cref{interiors}.
    Follows by \cref{interior,unions_iff,subseteq}.
\end{proof}

\begin{proposition}\label{interior_maximal}
    Let $X$ be a topological space.
    Suppose $U\subseteq A\subseteq \carrier[X]$.
    Suppose $U$ is open.
    Then $U\subseteq \interior{A}{X}$.
\end{proposition}
\begin{proof}
    $U\in\interiors{A}{X}$ by \cref{interiors}.
    $U\subseteq\unions{\interiors{A}{X}}$ by \cref{unions_iff,subseteq}.
    Follows by \cref{interior}.
\end{proof}

\begin{proposition}\label{interior_eq_self_implies_open}
    Let $X$ be a topological space.
    Suppose $\interior{A}{X} = A$.
    Then $A$ is open.
\end{proposition}
\begin{proof}
    $\interior{A}{X}$ is open by \cref{interior_is_open}.
    Follows by assumption.
\end{proof}

\begin{corollary}\label{interior_eq_self_iff_open}
    Let $X$ be a topological space.
    Then $\interior{A}{X} = A$ iff $A$ is open in $X$.
\end{corollary}
\begin{proof}
    Follows by \cref{interior_eq_self_implies_open,interior_of_open}.
\end{proof}

\begin{proposition}\label{interior_carrier}
    Let $X$ be a topological space.
    $\interior{\carrier[X]}{X} = \carrier[X]$.
\end{proposition}
\begin{proof}
    Follows by \cref{carrier_open,interior_of_open}.
\end{proof}

\begin{proposition}\label{interior_type}
    Let $X$ be a topological space.
    Then $\interior{A}{X}\in\pow{\carrier[X]}$.
\end{proposition}
\begin{proof}
    We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$
        by \cref{interiors,opens_type,subseteq}.
    For all $x\in\interior{A}{X}$ we have $x\in\carrier[X]$
        by \cref{interior,unions_iff,pow_iff,subseteq}.
    Follows by \cref{pow_iff}.
\end{proof}

\subsection{Closed sets}

\begin{definition}\label{is_closed_in}
    $A$ is closed in $X$ iff $\carrier[X]\setminus A$ is open in $X$.
\end{definition}

\begin{abbreviation}\label{is_clopen_in}
    $A$ is clopen in $X$ iff $A$ is open in $X$ and closed in $X$.
\end{abbreviation}

\begin{proposition}\label{emptyset_is_closed}
    Let $X$ be a topological space.
    Then $\emptyset$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus \emptyset = \carrier[X]$ by \cref{setminus_emptyset}.
    Follows by \cref{is_closed_in,carrier_open}.
\end{proof}

\begin{proposition}\label{carrier_is_closed}
    Let $X$ be a topological space.
    Then $\carrier[X]$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus \carrier[X] = \emptyset$ by \cref{setminus_self}.
    Follows by \cref{emptyset_open,is_closed_in}.
\end{proof}

\begin{proposition}\label{opens_minus_closed_is_open}
    Let $X$ be a topological space.
    Suppose $A, B \subseteq \carrier[X]$.
    Suppose $A$ is open in $X$.
    Suppose $B$ is closed in $X$.
    Then $A \setminus B$ is open in $X$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_eq_emptyset_iff_subseteq,is_closed_in,opens_inter,inter_comm_left,setminus_union,inter_assoc,inter_setminus,inter_lower_left,inter_lower_right,setminus_subseteq,double_complement,setminus_setminus,setminus_eq_inter_complement,setminus_self,setminus_inter,union_comm,emptyset_subseteq,setminus_partition}.
\end{proof}

\begin{definition}[Closed sets]\label{closeds}
    $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$.
\end{definition}

\begin{proposition}\label{complement_of_open_elem_closeds}
    Let $X$ be a topological space.
    Let $U\in\opens[X]$.
    Then $\carrier[X]\setminus U\in\closeds{X}$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus U\subseteq\carrier[X]$
        by \cref{setminus_subseteq}.
    $\carrier[X]\setminus U\in\pow{\carrier[X]}$
        by \cref{pow_iff,subseteq}.
    $U\subseteq\carrier[X]$ by \cref{opens_type}.
    Hence $\carrier[X]\setminus(\carrier[X]\setminus U) = U$ by \cref{double_relative_complement}.
    $\carrier[X]\setminus U$ is closed in $X$ by \cref{is_closed_in}.
    Follows by \cref{closeds}.
\end{proof}


\begin{definition}[Closed covers]\label{closures}
    $\closures{A}{X} = \{ D\in\pow{\carrier[X]}\mid \text{$A\subseteq D$ and $D$ is closed in $X$}\}$.
\end{definition}

\begin{definition}[Closure]\label{closure}
    $\closure{A}{X} = \inters{\closures{A}{X}}$.
\end{definition}

\begin{proposition}\label{closure_emptyset}
    Let $X$ be a topological space.
    Then $\closure{\emptyset}{X} = \emptyset$.
\end{proposition}
\begin{proof}
    $\emptyset\in\pow{\carrier[X]}$ by \cref{emptyset_subseteq,pow_iff}.
    $\emptyset$ is closed in $X$ by \cref{emptyset_is_closed}.
    $\emptyset\in\closures{\emptyset}{X}$ by \cref{closures,subseteq_refl}.
    For all $x\in\closure{\emptyset}{X}$ we have $x\in\emptyset$
        by \cref{closure,inters_subseteq_elem,subseteq}.
    For all $x\in\emptyset$ we have $x\in\closure{\emptyset}{X}$
        by \cref{emptyset_subseteq,subseteq}.
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{closure_carrier}
    Let $X$ be a topological space.
    Then $\closure{\carrier[X]}{X} = \carrier[X]$.
\end{proposition}
\begin{proof}
    For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$
        by \cref{closures}.
    For all $D\in\closures{\carrier[X]}{X}$ we have
        $D\in\pow{\carrier[X]}$ by \cref{closures}.
    For all $D\in\closures{\carrier[X]}{X}$ we have $D\subseteq\carrier[X]$
        by \cref{pow_iff,subseteq}.
    For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$
        by \cref{subseteq_antisymmetric}.
    $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}.
    $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq}.
    Now $\carrier[X]\in\closures{\carrier[X]}{X}$
        by \cref{closures,carrier_is_closed}.
    Thus $\closures{\carrier[X]}{X} = \{\carrier[X]\}$
        by \cref{singleton_iff_inhabited_subsingleton}.
    Follows by \cref{inters_singleton,closure}.
\end{proof}

\begin{proposition}\label{subseteq_inters_iff_to_right}
    Let $A,F$ be sets.
    Suppose $A \subseteq \inters{F}$.
    Then for all $X \in F$ we have $A \subseteq X$.
\end{proposition}
\begin{proof}
    Follows by \cref{inters_subseteq_elem,subseteq}.
\end{proof}


\begin{proposition}\label{subseteq_of_all_then_subset_of_union}
    Let $A,F$ be sets.
    Suppose $F$ is inhabited. %TODO: Remove!!
    Suppose for all $X \in F$ we have $A \subseteq X$.
    Then $A \subseteq \unions{F}$.
\end{proposition}
\begin{proof}
    Take $X$ such that $X\in F$ by assumption.
    $X\subseteq\unions{F}$ by \cref{unions_iff,subseteq}.
    $A\subseteq X$ by assumption.
    Follows by \cref{subseteq_transitive}.
\end{proof}



\begin{proposition}\label{subseteq_inters_iff_to_left}
    Let $A,F$ be sets.
    Suppose $F$ is inhabited.    % TODO:Remove!!
    Suppose for all $X \in F$ we have $A \subseteq X$.
    Then $A \subseteq \inters{F}$.
\end{proposition}
\begin{proof}
    For all $a\in A$ we have for all $X\in F$ we have $a\in X$
        by \cref{subseteq}.
    For all $a\in A$ we have $a\in\inters{F}$
        by \cref{inters_iff_forall}.
    Follows by \cref{subseteq}.
\end{proof}

\begin{proposition}\label{subseteq_inters_iff_new}
    Suppose $F$ is inhabited.
    $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq_inters_iff_to_left,subseteq_inters_iff_to_right}.
\end{proof}

\begin{proposition}\label{set_is_subseteq_to_closure_of_the_set}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    $A \subseteq \closure{A}{X}$.
\end{proposition}
\begin{proof}
    $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq_refl}.
    $\carrier[X]$ is closed in $X$ by \cref{carrier_is_closed}.
    $\carrier[X]\in\closures{A}{X}$
        by \cref{closures,subseteq_refl}.
    $\closures{A}{X}$ is inhabited by assumption.
    For all $A'\in\closures{A}{X}$ we have $A\subseteq A'$
        by \cref{closures}.
    $A\subseteq\inters{\closures{A}{X}}$
        by \cref{subseteq_inters_iff_to_left}.
    Follows by \cref{closure}.
\end{proof}

\begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$.
\end{proposition}
\begin{proof}
    For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$
    we have $x\in\carrier[X]$
        by \cref{setminus_elim_left}.
    For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$
    we have $x\notin\closure{(\carrier[X]\setminus A)}{X}$
        by \cref{setminus_elim_right}.
    For all $x$ we have if
    $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ and
    $x\in\carrier[X]\setminus A$, then
    $x\in\closure{(\carrier[X]\setminus A)}{X}$
        by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,subseteq}.
    For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$
    we have $x\in A$ by \cref{setminus}.
    Follows by \cref{subseteq}.
\end{proof}

\begin{proposition}\label{complement_of_closed_is_open}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    Suppose $A$ is closed in $X$.
    Then $\carrier[X] \setminus A$ is open in $X$.
\end{proposition}
\begin{proof}
    Follows by \cref{is_closed_in}.
\end{proof}

\begin{proposition}\label{complement_of_open_is_closed}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    Suppose $A$ is open in $X$.
    Then $\carrier[X] \setminus A$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus(\carrier[X]\setminus A)=A$
        by \cref{double_relative_complement}.
    Follows by \cref{is_closed_in}.
\end{proof}

\begin{proposition}\label{intersection_of_closed_is_closed}
    Let $X$ be a topological space.
    Suppose $A, B \subseteq \carrier[X]$.
    Suppose $A$ is closed in $X$.
    Suppose $B$ is closed in $X$.
    Then $A \inter B$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$
        by \cref{is_closed_in}.
    $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B)
        \in \opens[X]$ by \cref{union_open}.
    $\carrier[X]\setminus(A\inter B)
        =(\carrier[X]\setminus A)\union(\carrier[X]\setminus B)$
        by \cref{setminus_inter}.
    Follows by \cref{is_closed_in}.
\end{proof}

\begin{proposition}\label{union_of_closed_is_closed}
    Let $X$ be a topological space.
    Suppose $A, B \subseteq \carrier[X]$.
    Suppose $A$ is closed in $X$.
    Suppose $B$ is closed in $X$.
    Then $A \union B$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$
        by \cref{is_closed_in}.
    $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B)
        \in \opens[X]$ by \cref{opens_inter}.
    $\carrier[X]\setminus(A\union B)
        =(\carrier[X]\setminus A)\inter(\carrier[X]\setminus B)$
        by \cref{setminus_union}.
    Follows by \cref{is_closed_in}.
\end{proof}

\begin{proposition}\label{closed_minus_open_is_closed}
    Let $X$ be a topological space.
    Suppose $A, B \subseteq \carrier[X]$.
    Suppose $A$ is open in $X$.
    Suppose $B$ is closed in $X$.
    Then $B \setminus A$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus A\subseteq\carrier[X]$
        by \cref{setminus_subseteq}.
    $\carrier[X]\setminus A$ is closed in $X$
        by \cref{complement_of_open_is_closed}.
    $B\inter(\carrier[X]\setminus A)$ is closed in $X$
        by \cref{intersection_of_closed_is_closed}.
    Follows by \cref{setminus_eq_inter_complement}.
\end{proof}



\begin{proposition}\label{intersection_of_closed_is_closed_infinite}
    Let $X$ be a topological space.
    Suppose $F \subseteq \pow{\carrier[X]}$.
    Suppose for all $A \in F$ we have $A$ is closed in $X$.
    Suppose $F$ is inhabited.
    Then $\inters{F}$ is closed in $X$.
\end{proposition}
\begin{proof}
    Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $.
    Show for all $Y$ we have if $Y\in F'$, then $Y$ is open in $X$.
    \begin{subproof}
        Fix $Y$.
        Assume $Y\in F'$.
        Take $C$ such that $C\in F$ and
            $Y=\carrier[X]\setminus C$ by assumption.
        $C$ is closed in $X$ by assumption.
        $\carrier[X]\setminus C$ is open in $X$
            by \cref{complement_of_closed_is_open,pow_iff,subseteq}.
        Follows by assumption.
    \end{subproof}
    $F'\subseteq\opens[X]$ by \cref{subseteq}.
    $\unions{F'}$ is open in $X$ by \cref{opens_unions}.
    $\unions{F'}\subseteq\carrier[X]$
        by \cref{opens_type,unions_iff,pow_iff,subseteq}.
    $\inters{F}\subseteq\carrier[X]$
        by \cref{inters_iff_forall,pow_iff,subseteq}.
    Show $\inters{F} = \carrier[X] \setminus (\unions{F'})$.
    \begin{subproof}
        Show for all $a$ we have if $a\in\inters{F}$, then
            $a\in\carrier[X]\setminus\unions{F'}$.
        \begin{subproof}
            Fix $a$.
            Assume $a\in\inters{F}$.
            $a\in\carrier[X]$
                by \cref{inters_iff_forall,pow_iff,subseteq}.
            For all $A\in F$ we have $a\in A$
                by \cref{inters_iff_forall}.
            For all $A\in F$ we have
                $a\notin\carrier[X]\setminus A$ by \cref{setminus}.
            $a\notin\unions{F'}$ by \cref{unions_iff}.
            Follows by \cref{setminus_intro}.
        \end{subproof}
        Show for all $a$ we have if
            $a\in\carrier[X]\setminus\unions{F'}$, then $a\in\inters{F}$.
        \begin{subproof}
            Fix $a$.
            Assume $a\in\carrier[X]\setminus\unions{F'}$.
            Omitted.
        \end{subproof}
        Follows by set extensionality.
    \end{subproof}
    Follows by \cref{complement_of_open_is_closed}.
\end{proof}

\begin{proposition}\label{closure_is_closed}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    Then $\closure{A}{X}$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\carrier[X]\in\closures{A}{X}$
        by \cref{closures,pow_iff,carrier_is_closed,subseteq_refl}.
    $\closures{A}{X}$ is inhabited by assumption.
    $\closures{A}{X}\subseteq\pow{\carrier[X]}$ by \cref{closures,subseteq}.
    For all $B\in\closures{A}{X}$ we have $B$ is closed in $X$
        by \cref{closures}.
    $\inters{\closures{A}{X}}$ is closed in $X$
        by \cref{intersection_of_closed_is_closed_infinite}.
    Follows by \cref{closure}.
\end{proof}



\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$.
\end{proposition}
\begin{proof}
    Follows by \cref{closure,closeds,inters_subseteq_elem,closures}.
\end{proof}

\begin{proposition}\label{interior_is_maximal}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$.
\end{proposition}
\begin{proof}
    Follows by \cref{interior_maximal}.
\end{proof}

\begin{proposition}\label{complement_interior_eq_closure_complement}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$.
\end{proposition}
\begin{proof}
    $\carrier[X]\setminus A\subseteq\carrier[X]$ by \cref{setminus_subseteq}.
    $\carrier[X]\in\closeds{X}$
        by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}.
    $\closure{(\carrier[X]\setminus A)}{X}\subseteq\carrier[X]$
        by \cref{closure_is_minimal_closed_set}.
    $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$
        is open in $X$ by \cref{closure_is_closed,complement_of_closed_is_open}.
    $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}\subseteq A$
        by \cref{complement_of_closure_of_complement_of_x_subseteq_x}.
    $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}
        \subseteq\interior{A}{X}$ by \cref{interior_maximal}.
    $\carrier[X]\setminus\interior{A}{X}
        \subseteq\carrier[X]\setminus
            (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X})$
        by \cref{subseteq_implies_setminus_supseteq}.
    $\carrier[X]\setminus
        (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X})
        =\closure{(\carrier[X]\setminus A)}{X}$
        by \cref{double_relative_complement}.
    $\carrier[X]\setminus\interior{A}{X}
        \subseteq\closure{(\carrier[X]\setminus A)}{X}$
        by \cref{subseteq_transitive}.

    $\interior{A}{X}\subseteq A$ by \cref{interior_subseteq}.
    $\carrier[X]\setminus A
        \subseteq\carrier[X]\setminus\interior{A}{X}$
        by \cref{subseteq_implies_setminus_supseteq}.
    $\carrier[X]\setminus\interior{A}{X}\in\closeds{X}$
        by \cref{interior_is_open,complement_of_open_elem_closeds}.
    $\closure{(\carrier[X]\setminus A)}{X}
        \subseteq\carrier[X]\setminus\interior{A}{X}$
        by \cref{closure_is_minimal_closed_set}.
    Follows by \cref{subseteq_antisymmetric}.
\end{proof}



\begin{definition}[Frontier]\label{frontier}
    $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$.
\end{definition}

\begin{proposition}\label{closure_interior_frontier_is_in_carrier}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$.
\end{proposition}
\begin{proof}
    $\carrier[X]\in\closeds{X}$
        by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}.
    $\closure{A}{X}\subseteq\carrier[X]$
        by \cref{closure_is_minimal_closed_set}.
    $\interior{A}{X}\subseteq\carrier[X]$
        by \cref{interior_type,pow_iff,subseteq}.
    $\frontier{A}{X}\subseteq\carrier[X]$
        by \cref{frontier,setminus_subseteq,subseteq_transitive}.
    Follows by assumption.
\end{proof}

\begin{proposition}\label{frontier_is_closed}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    Then $\frontier{A}{X}$ is closed in $X$.
\end{proposition}
\begin{proof}
    $\closure{A}{X},\interior{A}{X}\subseteq\carrier[X]$
        by \cref{closure_interior_frontier_is_in_carrier}.
    $\closure{A}{X}$ is closed in $X$ by \cref{closure_is_closed}.
    $\interior{A}{X}$ is open in $X$ by \cref{interior_is_open}.
    $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$
        by \cref{closed_minus_open_is_closed}.
    Follows by \cref{frontier}.
\end{proof}

\begin{proposition}\label{setdifference_eq_intersection_with_complement}
    Suppose $A,B \subseteq C$.
    Then $A \setminus B = A \inter (C \setminus B)$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_eq_inter_complement}.
\end{proof}



\begin{proposition}\label{frontier_as_inter}
    Let $X$ be a topological space.
    Suppose $A \subseteq \carrier[X]$.
    $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$.
\end{proposition}
\begin{proof}
    $\closure{A}{X}\setminus\interior{A}{X}
        =\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$
        by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}.
    $\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})
        =\closure{A}{X}\inter\closure{(\carrier[X]\setminus A)}{X}$
        by \cref{complement_interior_eq_closure_complement}.
    Follows by \cref{frontier}.
\end{proof}

\begin{proposition}\label{frontier_of_emptyset}
    Let $X$ be a topological space.
    Then $\frontier{\emptyset}{X} = \emptyset$.
\end{proposition}
\begin{proof}
    $\interior{\emptyset}{X}=\emptyset$
        by \cref{emptyset_open,interior_of_open}.
    Follows by \cref{frontier,closure_emptyset,setminus_self}.
\end{proof}

\begin{proposition}\label{frontier_of_carrier}
    Let $X$ be a topological space.
    Then $\frontier{\carrier[X]}{X} = \emptyset$.
\end{proposition}
\begin{proof}
    $\frontier{\carrier[X]}{X} = \carrier[X]\setminus\carrier[X]$
        by \cref{frontier,interior_carrier,closure_carrier}.
    Follows by \cref{setminus_self}.
\end{proof}

\begin{definition}\label{neighbourhoods}
    $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$.
\end{definition}

\begin{definition}\label{neighbourhoods_set}
    $\neighbourhoodsSet{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\subseteq U\subseteq N\}$.
\end{definition}