naproch sty extension

4 files changed, 87 insertions, 14 deletions

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 7ef2359..5ca673d 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -100,6 +100,7 @@
 \newcommand{\memrel}[1]{{\in_{#1}}}
 \newcommand{\monusNat}{-_{\naturals}}
 \newcommand{\naturals}{\mathcal{N}}
+\newcommand{\naturalsPlus}{\mathcal{N}_{+}}
 \newcommand{\notmeets}{\mathrel{\not\meets}}
 \newcommand{\pow}[1]{\fun{Pow}(#1)}
 \newcommand{\precedes}{<}
@@ -133,6 +134,14 @@
 \newcommand{\zero}{0}
 \newcommand{\one}{1}
 \newcommand{\rmul}{\cdot}
+\newcommand{\inv}[1]{#1^{-1}}
+\newcommand{\rfrac}[2]{\frac{#1}{#2}}
+\newcommand{\rationals}{\mathcal{Q}}
+\newcommand{\rminus}{-_{\mathcal{R}}}
+\newcommand{\seq}[2]{\{#1, ... ,#2\}}
+\newcommand{\indexx}[2]{index_{#1}(#2)}
+\newcommand{\indexset}[2]{#1}
+
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
@@ -166,6 +175,7 @@
 \newcommand{\closure}[2]{\fun{cl}_{#2}{#1}}
 \newcommand{\frontier}[2]{\fun{fr}_{#2}{#1}}
 \newcommand{\neighbourhoods}[2]{\textsf{N}_{#2}{#1}}
+\newcommand{\neighbourhoodsSet}[2]{\textsf{N}_{SET #2}{#1}}
 \newcommand{\disconnections}[1]{\fun{Disconnections}{#1}}
 
 \newcommand{\teezero}{\ensuremath{T_0}} % Kolmogorov
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index dba42a2..2faa267 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -46,4 +46,6 @@
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
     \input{../library/numbers.tex}
+    \input{../library/topology/urysohn.tex}
+    \input{../library/wunschzettel.tex}
 \end{document}
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}