diff options
| -rw-r--r-- | library/set.tex | 6 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 10 |
2 files changed, 11 insertions, 5 deletions
diff --git a/library/set.tex b/library/set.tex index e7e062f..fcd2642 100644 --- a/library/set.tex +++ b/library/set.tex @@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and “$A \neq B$”. If $x$ and $y$ are empty, then $x = y$. \end{proposition} -\begin{proposition}% -\label{emptyset_subseteq} +\begin{proposition}\label{emptyset_subseteq} For all $a$ we have $\emptyset \subseteq a$. % LATER $\emptyset$ is a subset of every set. \end{proposition} @@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio There exists $B\in C$ such that $A\in B$. \end{proof} -\begin{proposition}% -\label{unions_emptyset} +\begin{proposition}\label{unions_emptyset} $\unions{\emptyset} = \emptyset$. \end{proposition} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index e467d48..2bbdf09 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -11,7 +11,6 @@ such that \begin{enumerate} \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$. - \item\label{emptyset_open} $\emptyset\in\opens[X]$. \item\label{carrier_open} $\carrier[X]\in\opens[X]$. \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$. \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$. @@ -26,6 +25,15 @@ $U$ is open in $X$ iff $U\in\opens[X]$. \end{abbreviation} +\begin{proposition}\label{emptyset_open} + Let $X$ be a topological space. + Then $\emptyset$ is open in $X$. +\end{proposition} +\begin{proof} + We have $\unions{\emptyset} = \emptyset\subseteq\opens[X]$ by \cref{unions_emptyset,emptyset_subseteq}. + Follows by \cref{opens_unions}. +\end{proof} + \begin{proposition}\label{union_open} Let $X$ be a topological space. Suppose $A$, $B$ are open. |