diff options
| -rw-r--r-- | library/topology/urysohn2.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 7f98bc2..f70d679 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -41,7 +41,7 @@ \begin{definition}\label{sequence} - $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$. + $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$. \end{definition} @@ -169,6 +169,9 @@ \begin{theorem}\label{safe} Contradiction. \end{theorem} +\begin{proof} + Follows by \cref{iff_sequence,codom_of_emptyset_can_be_anything,sequence,emptyset_is_function_on_emptyset,id_dom,in_irrefl,suc_subseteq_implies_in,emptyset_subseteq}. +\end{proof} |