\import{topology/topological-space.tex}
\import{set.tex}
\import{set/powerset.tex}

\subsection{Topological basis}

\begin{abbreviation}\label{covers}
    $C$ covers $X$ iff
    for all $x\in X$ there exists $U\in C$ such that $x\in U$.
\end{abbreviation}

\begin{proposition}\label{covers_unions_intro}
    Suppose $C$ covers $X$.
    Then $X\subseteq\unions{C}$.
\end{proposition}

\begin{proposition}\label{covers_unions_elim}
    Suppose $X\subseteq\unions{C}$.
    Then $C$ covers $X$.
\end{proposition}

% Also called "prebase", "subbasis", or "subbase". We prefer "pre-" or "quasi-"
% for consistency when handling generalizations, even if "subbasis" is more common.
\begin{abbreviation}\label{topological_prebasis}
    $B$ is a topological prebasis for $X$ iff $\unions{B} = X$.
\end{abbreviation}

\begin{proposition}\label{topological_prebasis_iff_covering_family}
    $B$ is a topological prebasis for $X$ iff
    $B$ is a family of subsets of $X$ and $B$ covers $X$.
\end{proposition}
\begin{proof}
    If $B$ is a family of subsets of $X$ and $B$ covers $X$,
        then $\unions{B} = X$
            by \cref{subseteq_antisymmetric,unions_family,covers_unions_intro}.
    If $\unions{B} = X$,
        then $B$ is a family of subsets of $X$ and $B$ covers $X$
            by \cref{covers_unions_intro,subseteq_refl,covers_unions_elim}.
\end{proof}

% Also called "base of topology".
\begin{definition}\label{topological_basis}
    $B$ is a topological basis for $X$ iff
    $B$ is a topological prebasis for $X$ and
    for all $U, V, x$ such that $U, V\in B$ and $x\in U,V$
    there exists $W\in B$ such that $x\in W\subseteq U, V$.
\end{definition}

\begin{definition}\label{genopens}
    $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$
    \\ such that $x\in V\subseteq U$}\right\}$.
\end{definition}

\begin{lemma}\label{emptyset_in_genopens}
    Assume $B$ is a topological basis for $X$.
    $\emptyset \in \genOpens{B}{X}$.
\end{lemma}

\begin{lemma}\label{all_is_in_genopens}
    Assume $B$ is a topological basis for $X$.
    $X \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
    $\unions{B} \in \genOpens{B}{X}$.
    $X \subseteq \unions{B}$.
\end{proof}

\begin{lemma}\label{union_in_genopens}
    Assume $B$ is a topological basis for $X$.
    For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}




\begin{lemma}\label{inters_in_genopens}
    Assume $B$ is a topological basis for $X$.
    %For all $A, C$ 
    If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
    
    Show $(A \inter C) \in \pow{X}$.
    \begin{subproof}
        $(A \inter C) \subseteq X$ by assumption.
    \end{subproof}
    Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$.
    

    Show for all $x\in (A\inter C)$ there exists $W \in B$
    such that $x\in W$ and $W \subseteq (A\inter C)$.
    \begin{subproof}
        Fix $x \in (A\inter C)$.
        There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption.  %TODO: Warum muss hier by assumtion hin?
        There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption.
        There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption.
        
        Show $W \subseteq (A\inter C)$.
        \begin{subproof}
            %$W \subseteq v'$ and $W \subseteq V''$.
            For all $y \in W$ we have $y \in V'$ and $y \in V''$ by assumption.
        \end{subproof}
    \end{subproof}
    %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
    %such that $x\in W$ and $W \subseteq (A\inter C)$.

    $(A\inter C) \in \genOpens{B}{X}$ by assumption.
    
 
\end{proof}