naproch sty extension

2 files changed, 75 insertions, 14 deletions

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index c3c72f0..b8a5fa5 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -504,26 +504,31 @@ The first tept will be a formalisation of chain constructions.
 
 
  
-\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}
+%\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
 
 
 
 
+
+
+
+
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
new file mode 100644
index 0000000..8e5261e
--- /dev/null
+++ b/library/topology/urysohn2.tex
@@ -0,0 +1,56 @@
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set.tex}
+\import{cardinal.tex}
+\import{relation.tex}
+\import{relation/uniqueness.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+
+\section{Urysohns Lemma}
+
+
+
+\begin{abbreviation}\label{urysohnspace}
+    $X$ is a urysohn space iff
+    $X$ is a topological space and
+    for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$
+    we have there exist $A',B' \in \opens[X]$
+    such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
+\end{abbreviation}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+
+
+\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) = \zero$ and $f(B)= 1$ and $f$ is continuous.
+\end{theorem}
+\begin{proof}
+
+
+
+
+    
+    Contradiction.
+    
+\end{proof}
+
+\begin{theorem}\label{safe}
+    Contradiction.     
+\end{theorem}