library/topology/preclosure.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

\import{set.tex}
\import{function.tex}

\section{Preclosure spaces}


\begin{struct}\label{preclosure_space}
    A preclosure space $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\cl$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{preclosure_type} For all $Y\subseteq\carrier[X]$ we have
            $\cl[X](Y)\subseteq\carrier[X]$.
        \item\label{preclosure_empty} $\cl[X](\emptyset)=\emptyset$.
        \item\label{preclosure_extensive} For all $A\subseteq\carrier[X]$ we have
            $A\subseteq\cl[X](A)$.
        \item\label{preclosure_union} For all $A,B\subseteq\carrier[X]$ we have
            $\cl[X](A\union B)=\cl[X](A)\union\cl[X](B)$.
    \end{enumerate}
\end{struct}