1 files changed, 102 insertions, 14 deletions
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 0c4052d..d8b1e14 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -402,18 +402,32 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
+\begin{definition}\label{limit_sequence}
+    $x$ is the limit sequence of $f$ iff
+    $x$ is a sequence and $\indexset[x] = \dom{f}$ and
+    for all $n \in \indexset[x]$ we have
+    $\index[x](n) = f(n)$.
+\end{definition}
 
+\begin{definition}\label{realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
+\end{definition}
+
+\begin{abbreviation}\label{realsplus}
+    $\realsplus = \reals \setminus \realsminus$.
+\end{abbreviation}
 
 
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
+    Suppose $\carrier[X]$ is inhabited.
     There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = 0$ and $f(B)= 1$ and $f$ is continuous.
+    and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
 \end{theorem}
 \begin{proof}
-
+    
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
     and $\indexset[\eta] = \{\zero, 1\}$ 
     and $\index[\eta](\zero) = A$
@@ -498,29 +512,103 @@ The first tept will be a formalisation of chain constructions.
     \}$.
     
     Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
-    
 
+    %We show that there exist $\kappa$ such that $\kappa$ is the limit sequence of $\gamma$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
 
-    We show that there exist $F$ such that 
-    $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and
-    for all $x \in \carrier[X]$ we have 
-    there exist $k \in \intervalclosed{\zero}{1}$ 
-    such that $F(x) = k$ and 
-    for all $\epsilon \in \reals$ such that $\epsilon > \zero$
-    we have there exist $N \in \naturals$ such that 
-    for all $N' \in \naturals$ such that $N' > N$
-    we have $\abs{(k - \apply{\gamma(N')}{x})} \leq \epsilon$.
+    %Let $\gamma(n)(x) = \apply{\gamma(n)}{x}$ for $x\in \carrier[X]$
+
+    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+    is a function from $\carrier[X]$ to $\reals$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
+
+
+    We show that there exist $g$ such that 
+    for all $x \in \carrier[X]$ we have
+    there exist $k \in \reals$ such that
+    for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
+    there exist $N \in \naturals$ such that
+    for all $N' \in \naturals$ such that $N' > N$ we have
+    $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$ and $g(x)= k$.
+    \begin{subproof}
+
+        %Let $G(x) = \{k \in \carrier[X] \mid \forall \epsilon \in \realsplus. \exists N \in \naturals. \forall N' \in \naturals. (N' > N) \land (\abs{\apply{\gamma(n)}{x} - k} < \epsilon)\}$ for $x \in \carrier[X]$.        
+%
+        %We show that for all $x \in \carrier[X]$ we have $G(x)$ has cardinality $1$.
+        %\begin{subproof}
+        %    Omitted.
+        %\end{subproof}
+%
+        %Let $H(x) = \unions{G(x)}$ for $x \in \carrier[X]$.
+        %For all $x \in \carrier[X]$ we have $\{H(x)\} = G(x)$. 
+        
+        We show that for all $x \in \carrier[X]$ we have
+        there exist $k \in \reals$ such that
+        for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
+        there exist $N \in \naturals$ such that
+        for all $N' \in \naturals$ such that $N' > N$ we have
+        $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$.
+        \begin{subproof}
+            Omitted.
+        \end{subproof}
+
+
+    \end{subproof}
+
+
+    %Let $S(x) = \{(n,x) \mid n \in naturals \mid x = (\gamma(n))(x)\}$.
+    
+    %Let $S(x)
+
+    %We show that there exist $F$ such that
+    %for all $x \in \carrier[X]$ we have $F(x)$ is
+
+
+    %We show that there exist $F$ such that 
+    %$F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and
+    %for all $x \in \carrier[X]$ we have 
+    %there exist $k \in \intervalclosed{\zero}{1}$ 
+    %such that $F(x) = k$ and 
+    %for all $\epsilon \in \reals$ such that $\epsilon > \zero$
+    %we have there exist $N \in \naturals$ such that 
+    %for all $N' \in \naturals$ such that $N' > N$
+    %we have $\abs{(k - \apply{\gamma(N')}{x})} \leq \epsilon$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+
+
     
     We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
-    \begin{subproof}
+    \begin{subproof}        
         Omitted.
+        
+        %It suffices to show that $\dom{F} = \carrier[X]$ and 
+        %$F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $F$ is right-unique.
+        %
+        %We show that $F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$.
+        %\begin{subproof}
+        %    It suffices to show that $F \in \pow{\carrier[X] \times \intervalclosed{\zero}{1}}$.
+        %    It suffices to show that for all $w \in F$ we have $w \in (\carrier[X] \times \intervalclosed{\zero}{1})$.
+%
+        %    Fix $w \in F$.
+%   
+        %    %Take $x$ such that there exist $k \in \intervalclosed{\zero}{1}$ such that $w = (x,k)$.
+%
+%
+        %\end{subproof}
+        %
+%
+%
+        %Trivial.
     \end{subproof}
 
-    We show that $F(A) = 0$.
+    We show that $F(A) = \zero$.
     \begin{subproof}
         Omitted.
     \end{subproof}