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.

1 files changed, 18 insertions, 5 deletions

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}