\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{union_in_genopens}
    Assume $B$ is a topological basis for $X$.
    Assume $F\subseteq \genOpens{B}{X}$.
    Then $\unions{F}\in\genOpens{B}{X}$.
\end{lemma}
\begin{proof}
    We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}.

    Show for all $x\in \unions{F}$ there exists $W \in B$
    such that $x\in W$ and $W \subseteq \unions{F}$.
    \begin{subproof}
        Fix $x \in \unions{F}$.
        There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}.
        $V \in \genOpens{B}{X}$.
        There exists $W \in B$ such that $x \in W \subseteq V$.
        Then $W \subseteq \unions{F}$.
    \end{subproof}
    Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}.
\end{proof}

\begin{lemma}\label{basis_is_in_genopens}
    Assume $B$ is a topological basis for $X$.
    $B \subseteq \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
    We show for all $V \in B$ $V \in \genOpens{B}{X}$.
    \begin{subproof}
        Fix $V \in B$.
        For all $x \in V$ $x \in V \subseteq V$.
        $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
        $V \in \pow{X}$.
        $V \in \genOpens{B}{X}$.
    \end{subproof}
\end{proof}

\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{inters_in_genopens}
    Assume $B$ is a topological basis for $X$.
    Assume $A, C\in \genOpens{B}{X}$.
    Then $(A\inter C) \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}

    We have $(A \inter C) \in \pow{X}$ by \cref{genopens,inter_powerset}.


    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)$.
        Then $x\in A,C$.
        There exists $V'  \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}.
        There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}.
        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$ by \cref{topological_basis}.

        Show $W \subseteq (A\inter C)$.
        \begin{subproof}
            For all $y \in W$ we have $y \in V'$ and $y \in V''$.
        \end{subproof}
    \end{subproof}

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