From 5a7450eedc020867ee52ae9f1ecb6def7aa998bb Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 14 Aug 2024 10:50:26 +0200
Subject: The added proposition and definition should have resloved some
 proofing complications, but they can prove flase together with lemmas about
 ordinal, the exat lemma are in urysohn.tex at line 522.

---
 library/topology/urysohn.tex | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ba9780a..c3c72f0 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -503,11 +503,24 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-% Note this could maybe reslove some issues!!!!
+ 
 \begin{definition}\label{sequencetwo}
    $Z$ is a sequencetwo iff  $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$.
 \end{definition}
 
+\begin{proposition}\label{sequence_existence}
+    Suppose $N \subseteq \naturals$.
+    Suppose $M \subseteq \naturals$.
+    Suppose $N = M$.
+    Then there exist $Z,f$ such that $f$ is a bijection from $N$ to $M$ and $Z=(N,f,M)$ and $Z$ is a sequencetwo.
+\end{proposition}
+\begin{proof}
+    Let $f(x) = x$ for $x \in N$.
+    Let $Z=(N,f,M)$.
+\end{proof}
+%The proposition above and the definition prove false together with
+% ordinal_subseteq_unions, omega_is_an_ordinal, powerset_intro, in_irrefl
+
 
 
 
@@ -544,7 +557,7 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
-    For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.
+    %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.
 
     We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
@@ -824,6 +837,6 @@ The first tept will be a formalisation of chain constructions.
     %   \end{subproof}
 \end{proof}
 
-%\begin{theorem}\label{safe}
-%    Contradiction.     
-%\end{theorem}
+\begin{theorem}\label{safe}
+    Contradiction.     
+\end{theorem}
-- 
cgit v1.2.3

