From 36065f6a7fcc8f4d23b98be642c7fa7019ce2b79 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 2 Sep 2024 12:46:14 +0200
Subject: Corrected Contradiction. Contradiction was due to a misstake in the
 definition in sequence.

---
 library/topology/urysohn2.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'library/topology/urysohn2.tex')

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}
 
 
 
-- 
cgit v1.2.3