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

\subsection{Topological basis}\label{form_sec_topobasis}

\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{proof}
    For all $x\in X$ there exists $U\in C$ such that $x\in U$
        by assumption.
    For all $x\in X$ we have $x\in\unions{C}$ by \cref{unions_iff}.
    Follows by \cref{subseteq}.
\end{proof}

\begin{proposition}\label{covers_unions_elim}
    Suppose $X\subseteq\unions{C}$.
    Then $C$ covers $X$.
\end{proposition}
\begin{proof}
    For all $x\in X$ we have $x\in\unions{C}$ by \cref{subseteq}.
    For all $x\in X$ there exists $U\in C$ such that $x\in U$
        by \cref{unions_iff}.
    Follows by assumption.
\end{proof}

% 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}.
    Follows by assumption.
\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{proof}
    $\emptyset\in\pow{X}$ by \cref{emptyset_subseteq,pow_iff}.
    For all $x\in\emptyset$ there exists $V\in B$
        such that $x\in V\subseteq\emptyset$
        by \cref{emptyset_subseteq,subseteq}.
    Follows by \cref{genopens}.
\end{proof}



\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}
    For all $x\in\unions{F}$ we have $x\in X$
        by \cref{unions_iff,genopens,subseteq}.
    We have $\unions{F}\in\pow{X}$ by \cref{pow_iff,subseteq}.

    Show for all $x$ we have if $x\in\unions{F}$, then
    there exists $W\in B$ such that $x\in W$ and
    $W\subseteq\unions{F}$.
    \begin{subproof}
        Fix $x$.
        Assume $x\in\unions{F}$.
        Take $V$ such that $V\in F$ and $x\in V$ by \cref{unions_iff}.
        $V\in\genOpens{B}{X}$ by \cref{subseteq}.
        Take $W$ such that $W\in B$ and $x\in W\subseteq V$
            by \cref{genopens}.
        $V\subseteq\unions{F}$ by \cref{unions_iff,subseteq}.
        $W\subseteq\unions{F}$ by \cref{subseteq_transitive}.
        Follows by assumption.
    \end{subproof}
    Follows 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}
    Show for all $V$ we have if $V\in B$, then
    $V\in\genOpens{B}{X}$.
    \begin{subproof}
        Fix $V$.
        Assume $V\in B$.
        $V\subseteq X$
            by \cref{topological_prebasis_iff_covering_family,topological_basis}.
        $V\in\pow{X}$ by \cref{pow_iff,subseteq}.
        For all $x\in V$ there exists $W\in B$
            such that $x\in W\subseteq V$ by \cref{subseteq_refl}.
        Follows by \cref{genopens}.
    \end{subproof}
    Follows by \cref{subseteq}.
\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}
    $X\in\pow{X}$ by \cref{pow_iff,subseteq_refl}.
    For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$
        by \cref{topological_prebasis_iff_covering_family,topological_basis,pow_iff,subseteq}.
    Follows by \cref{genopens}.
\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}
    For all $x\in A\inter C$ we have $x\in X$
        by \cref{genopens,inter_elim_left,pow_iff,subseteq}.
    We have $(A\inter C)\in\pow{X}$ by \cref{pow_iff,subseteq}.

    Show for all $x$ we have if $x\in A\inter C$, then
    there exists $W\in B$ such that $x\in W$ and $W\subseteq A\inter C$.
    \begin{subproof}
        Fix $x$.
        Assume $x\in A\inter C$.
        $x\in A,C$ by \cref{inter_elim_left,inter_elim_right}.
        Take $V'$ such that $V'\in B$ and $x\in V'\subseteq A$
            by \cref{genopens}.
        Take $V''$ such that $V''\in B$ and $x\in V''\subseteq C$
            by \cref{genopens}.
        Take $W$ such that $W\in B$ and $x\in W$ and
            $W\subseteq V',V''$ by \cref{topological_basis}.
        $W\subseteq A,C$ by \cref{subseteq_transitive}.
        $W\subseteq A\inter C$ by \cref{inter_intro,subseteq}.
        Follows by assumption.
    \end{subproof}
    Follows by \cref{genopens}.
\end{proof}