diff options
Diffstat (limited to 'library/topology/basis.tex')
| -rw-r--r-- | library/topology/basis.tex | 105 |
1 files changed, 69 insertions, 36 deletions
diff --git a/library/topology/basis.tex b/library/topology/basis.tex index cc9d7e5..4c1ac79 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -13,11 +13,23 @@ 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. @@ -36,6 +48,7 @@ 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". @@ -55,6 +68,13 @@ 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} @@ -64,18 +84,25 @@ 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}. + 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\in \unions{F}$ there exists $W \in B$ - such that $x\in W$ and $W \subseteq \unions{F}$. + 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 \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}$. + 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} - Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} \begin{lemma}\label{basis_is_in_genopens} @@ -83,14 +110,19 @@ $B \subseteq \genOpens{B}{X}$. \end{lemma} \begin{proof} - We show for all $V \in B$ $V \in \genOpens{B}{X}$. + Show for all $V$ we have if $V\in B$, then + $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}$. + 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} @@ -98,11 +130,10 @@ $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}$. - For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$. - Follows by \cref{powerset_top,genopens}. + $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} @@ -111,23 +142,25 @@ 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}. - 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$. + 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 \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 \subseteq V', 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} + 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} - - $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} |