From 6129ebdf0d8549f3e4d23aa771f2c06020182b7e Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 7 Aug 2024 15:28:45 +0200
Subject: Created first urysohn formalization

---
 library/topology/urysohn.tex | 274 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 274 insertions(+)
 create mode 100644 library/topology/urysohn.tex

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
new file mode 100644
index 0000000..65457ea
--- /dev/null
+++ b/library/topology/urysohn.tex
@@ -0,0 +1,274 @@
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set.tex}
+\import{cardinal.tex}
+
+\section{Urysohns Lemma}
+%           In this section we want to proof Urysohns lemma. 
+%           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
+%           The Idea is to construct staircase functions as a chain.
+%           The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$.
+%           With the property that \[f\mid_{A}=1 \land f\mid_{B}=0\] for \[A,B\] closed sets.
+
+%Chains of  sets.
+
+The first tept will be a formalisation of chain constructions.
+
+\subsection{Chains of sets}
+%           Assume $A,B$ are subsets of a topological space $X$.
+
+%           As Jänich propose we want a special property on chains of subsets.
+%           We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. 
+%           \begin{align}
+%               A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B 
+%           \end{align} 
+%           such that for all elements in this chain following holds, 
+%           $\overline{A_{i-1}}  \subset \interior{A_{i}}$. 
+%           In this case we call the chain legal.
+
+\begin{definition}\label{one_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+\begin{definition}\label{cardinality}
+    $X$ has cardinality of $n$ iff
+    $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$.
+\end{definition}
+
+
+
+\begin{struct}\label{sequence}
+    A sequence $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\index$
+        \item $\indexset$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
+        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
+    \end{enumerate}
+\end{struct}
+
+\begin{definition}\label{cahin_of_subsets}
+    $C$ is a chain of subsets iff
+    $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$.
+\end{definition}
+
+\begin{definition}\label{chain_of_n_subsets}
+    $C$ is a chain of $n$ subsets iff
+    $C$ is a chain of subsets and $n \in \indexset[C]$ 
+    and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$.
+\end{definition}
+
+
+
+% TODO: The Notion above should be generalised to sequences since we need them as well for our limit
+% and also for the subproof of continuity of the limit.
+
+
+%     \begin{definition}\label{legal_chain}
+%         $C$ is a legal chain of subsets of $X$ iff 
+%         $C \subseteq \pow{X}$. %and 
+%         %there exist $f \in \funs{C}{\naturals}$ such that
+%         %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$.
+%     \end{definition}
+
+% TODO: We need a notion for declarinf new properties to existing thing. 
+%
+% The following gives a example and a wish want would be nice to have:
+% "A (structure) is called (adjectiv of property), if"
+%
+% This should then be use als follows:
+% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). 
+% Which should be translated to fol like this:
+% ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X)
+% ---------------------------------------------------------------
+
+
+
+\subsection{staircase function}
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+\begin{struct}\label{staircase_function}
+    A staircase function $f$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\chain$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
+        \item \label{staircase_domain} $\dom{f}$ is a topological space.
+        \item \label{staricase_def_chain} $C$ is a chain of subsets.
+        \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
+        \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. 
+        \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+    \end{enumerate}
+\end{struct}
+
+\begin{definition}\label{legal_staircase}
+    $f$ is a legal staircase function iff
+    $f$ is a staircase function and 
+    for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$.
+\end{definition}
+
+\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{urysohnchain}
+    $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
+    $C$ is a chain of subsets and
+    for all $A \in C$ we have $A \subseteq X$ and
+    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+\end{definition}
+
+\begin{abbreviation}\label{infinte_sequence}
+    $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite.
+\end{abbreviation}
+
+\begin{definition}\label{infinite_product}
+    $X$ is the infinite product of $Y$ iff
+    $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$.
+\end{definition}
+
+\begin{definition}\label{refinmant}
+    $C$ is a refinmant of $C'$ iff for all $x \in C'$ we have $x \in C$ and 
+    for all $y \in C'$ such that $y \subset x$ we have there exist $c \in C$ such that $y \subset c \subset x$
+    and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$.
+\end{definition}
+
+
+%                    The next thing we need to define is the uniform staircase function.
+%                    This function has it's domain in $X$ and maps to the closed interval $[0,1]$.
+%                    These functions should behave als follows,
+%                    \begin{align}
+%                        &f(A_{0}) = 1 &\text{consant} \\
+%                        &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.}
+%                    \end{align} 
+
+%                    We then prove that for any given $r$ we find a repolished chain,
+%                    which contains the $A_{i}$ and this replished chain is also legal.
+%                     
+%                    The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ 
+%                    be a staircase function with $n$ many refinemants. 
+%                    This limit will be continuous and we would be done. 
+
+
+% TODO: Since we want to prove that $f$ is continus, we have to formalize that 
+% \reals with the usual topology is a topological space. 
+% -------------------------------------------------------------
+
+\begin{theorem}\label{urysohn}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \subseteq \closeds{X}$.
+    Suppose $A \inter B$ is empty.
+    There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
+\end{theorem}
+\begin{proof}
+    We show that for all $n \in \naturals$ we have
+    if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ 
+    then there exist $C'$  such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ 
+    and $C'$ is a refinmant of $C$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    
+
+    Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
+    
+    We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+    and for all $i \in \indexset[\zeta]$ we have 
+    $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+    and $A \subseteq \index[\zeta](i)$
+    and $\index[\zeta](i) \subseteq (X \setminus B)$
+    and for all $j \in \indexset[\zeta]$ such that 
+    $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+  
+    
+
+
+    
+
+
+
+    We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    $g$ is a staircase function and $\chain[g] = C$.
+    $g$ is a legal staircase function.
+
+
+    We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+
+    %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. 
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+
+    %Proof Sheme Idea:
+    % -We proof for n=1 that C_{n} is a chain and legal
+    % -Then by induction with P(n+1) is refinmant of P(n)
+    % -Therefore we have a increing refinmant of these Chains such that our limit could even apply
+    % ---------------------------------------------------------
+
+    %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+
+
+    % Formalization idea of enumarted sequences:
+    % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
+    % - This should give all finite and infinte enumarable sequences
+    % - Introduce a notion for the indexing of these enumarable sequences.
+    % - Then we can define the limit of a enumarted sequence of functions.
+    % ---------------------------------------------------------
+    %
+    % Here we need a limit definition for sequences of functions
+    %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+    %
+    %We show that $F(A) = 1$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+    %
+    %We show that $F(B) = 0$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof} 
+    %
+    %We show that $F$ is continuous.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+\end{proof}
+
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
-- 
cgit v1.2.3


From 65e5a741655d8339ad5763e365ea2addd2e96e51 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Fri, 9 Aug 2024 15:15:49 +0200
Subject: put cardinalit to the right place

---
 library/cardinal.tex         |  6 ++++++
 library/topology/urysohn.tex | 39 ++++++++++++++++++++++++++++++++-------
 2 files changed, 38 insertions(+), 7 deletions(-)

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

diff --git a/library/cardinal.tex b/library/cardinal.tex
index d0dec59..8691b30 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -3,6 +3,7 @@
 \import{set.tex}
 \import{ordinal.tex}
 \import{function.tex}
+\import{numbers.tex}
 
 \begin{definition}\label{finite}
     $X$ is finite iff there exists a natural number $k$ such that
@@ -12,3 +13,8 @@
 \begin{abbreviation}\label{infinite}
     $X$ is infinite iff $X$ is not finite.
 \end{abbreviation}
+
+\begin{definition}\label{cardinality}
+    $X$ has cardinality $k$ iff $k$ is a natural number and 
+    there exists a bijection from $k$ to $X$.
+\end{definition}
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 65457ea..c795db8 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -33,10 +33,6 @@ The first tept will be a formalisation of chain constructions.
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
-\begin{definition}\label{cardinality}
-    $X$ has cardinality of $n$ iff
-    $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$.
-\end{definition}
 
 
 
@@ -134,6 +130,13 @@ The first tept will be a formalisation of chain constructions.
     for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
 \end{definition}
 
+\begin{definition}\label{urysohnchain_without_cardinality}
+    $C$ is a urysohnchain in $X$ iff
+    $C$ is a chain of subsets and
+    for all $A \in C$ we have $A \subseteq X$ and
+    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+\end{definition}
+
 \begin{abbreviation}\label{infinte_sequence}
     $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite.
 \end{abbreviation}
@@ -149,6 +152,26 @@ The first tept will be a formalisation of chain constructions.
     and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
+\begin{abbreviation}\label{two}
+    $\two = \suc{1}$.
+\end{abbreviation}
+
+\begin{lemma}\label{two_in_reals}
+    $\two \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{two_in_naturals}
+    $\two \in \naturals$.
+\end{lemma}
+
+\begin{inductive}\label{power_of_two}
+    Define $\powerOfTwoSet \subseteq \naturals$.
+    \begin{enumerate}
+        \item  $\two \in \powerOfTwoSet$.
+        \item  If $n \in \powerOfTwoSet$, then $n \rmul \two \in \powerOfTwoSet$.
+    \end{enumerate}
+
+\end{inductive}
 
 %                    The next thing we need to define is the uniform staircase function.
 %                    This function has it's domain in $X$ and maps to the closed interval $[0,1]$.
@@ -186,6 +209,8 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
+    There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$.
+
     
 
     Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
@@ -269,6 +294,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


From d49a4f85a928c4e93c6cbb2ebada5875e12c4b4f Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 10 Aug 2024 01:25:48 +0200
Subject: more ur<sohn

---
 library/topology/urysohn.tex | 133 ++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 125 insertions(+), 8 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index c795db8..bb28116 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -147,9 +147,9 @@ The first tept will be a formalisation of chain constructions.
 \end{definition}
 
 \begin{definition}\label{refinmant}
-    $C$ is a refinmant of $C'$ iff for all $x \in C'$ we have $x \in C$ and 
-    for all $y \in C'$ such that $y \subset x$ we have there exist $c \in C$ such that $y \subset c \subset x$
-    and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$.
+    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
+    for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
+    and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
 \begin{abbreviation}\label{two}
@@ -165,14 +165,131 @@ The first tept will be a formalisation of chain constructions.
 \end{lemma}
 
 \begin{inductive}\label{power_of_two}
-    Define $\powerOfTwoSet \subseteq \naturals$.
+    Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
     \begin{enumerate}
-        \item  $\two \in \powerOfTwoSet$.
-        \item  If $n \in \powerOfTwoSet$, then $n \rmul \two \in \powerOfTwoSet$.
+        \item  $(\zero, 1) \in \powerOfTwoSet$.
+        \item  If $(m,k) \in \powerOfTwoSet$, then $(m+1, k \rmul \two) \in \powerOfTwoSet$.
     \end{enumerate}
-
 \end{inductive}
 
+\begin{abbreviation}\label{pot}
+    $\pot = \powerOfTwoSet$.
+\end{abbreviation}
+
+\begin{lemma}\label{dom_pot}
+    $\dom{\pot} = \naturals$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{ran_pot}
+    $\ran{\pot} \subseteq \naturals$.
+\end{lemma}
+
+
+
+
+
+
+
+
+\begin{proposition}\label{urysohnchain_induction_begin}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \inter B$ is empty.
+    Suppose $U = \{A,(X \setminus B)\}$.
+    Suppose $\indexset[U]= \{\zero, 1\}$.
+    Suppose $\index[U](\zero) = A$.
+    Suppose $\index[U](1) = (X \setminus B)$.
+    Then $U$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+    We show that $U$ is a sequence.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that $A \subseteq (X \setminus B)$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that $U$ is a chain of subsets.
+    \begin{subproof}
+        For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
+        It suffices to show that for all $n \in \indexset[U]$ we have
+        for all $m \in \indexset[U]$ such that 
+        $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
+        Fix $n \in \indexset[U]$.
+        Fix $m \in \indexset[U]$.
+        \begin{byCase}
+            \caseOf{$n = 1$.} Trivial.
+            \caseOf{$n = \zero$.} 
+                \begin{byCase}
+                    \caseOf{$m = \zero$.} Trivial.
+                    \caseOf{$m = 1$.} Omitted.
+                \end{byCase}
+        \end{byCase}
+    \end{subproof}
+
+    $A \subseteq X$.
+    $(X \setminus B) \subseteq X$.
+    We show that for all $x \in U$ we have $x \subseteq X$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
+    $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+\end{proof}
+
+
+\begin{proposition}\label{t_four_propositon}
+    Let $X$ be a urysohn space.
+    Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
+    we have there exists $C \subseteq X$ such that 
+    $\closure{A}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{B}{X}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{urysohnchain_induction_step_existence}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain in $X$.
+    Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+    
+    
+    %\begin{definition}\label{refinmant}
+    %    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
+    %    for all $y \in C$ such that $y \subset x$ 
+    %    we have there exist $c \in C'$ such that $y \subset c \subset x$
+    %    and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
+    %\end{definition}
+    
+    
+
+
+\end{proof}
+
+
+
+
+
+
+
+
+
 %                    The next thing we need to define is the uniform staircase function.
 %                    This function has it's domain in $X$ and maps to the closed interval $[0,1]$.
 %                    These functions should behave als follows,
@@ -195,7 +312,7 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
-    Suppose $A,B \subseteq \closeds{X}$.
+    Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
     There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
     and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
-- 
cgit v1.2.3


From 894dd1c6e66099f65ebb8860e0cdf258fa143e89 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 10 Aug 2024 16:02:43 +0200
Subject: more urysohn

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

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index bb28116..3152de7 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -262,12 +262,26 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
 \begin{proposition}\label{urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$.
     Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
+    % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
+    % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
+
+    Let $m = \max{\indexset[U]}$.
+    For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
     
     
     %\begin{definition}\label{refinmant}
@@ -276,9 +290,7 @@ The first tept will be a formalisation of chain constructions.
     %    we have there exist $c \in C'$ such that $y \subset c \subset x$
     %    and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
     %\end{definition}
-    
-    
-
+    Omitted.
 
 \end{proof}
 
-- 
cgit v1.2.3


From 34aad4be8fb8433f0205517732da0d449d077572 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 10 Aug 2024 19:18:39 +0200
Subject: more more urysohn

---
 library/cardinal.tex         |   2 +
 library/topology/urysohn.tex | 341 ++++++++++++++++++++++++-------------------
 2 files changed, 190 insertions(+), 153 deletions(-)

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

diff --git a/library/cardinal.tex b/library/cardinal.tex
index 8691b30..044e5d1 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -18,3 +18,5 @@
     $X$ has cardinality $k$ iff $k$ is a natural number and 
     there exists a bijection from $k$ to $X$.
 \end{definition}
+
+
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 3152de7..028e10f 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -198,60 +198,82 @@ The first tept will be a formalisation of chain constructions.
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
-    Suppose $U = \{A,(X \setminus B)\}$.
-    Suppose $\indexset[U]= \{\zero, 1\}$.
-    Suppose $\index[U](\zero) = A$.
-    Suppose $\index[U](1) = (X \setminus B)$.
-    Then $U$ is a urysohnchain in $X$.
+    Then there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexset[U]= \{\zero, 1\}$
+    and $\index[U](\zero) = A$
+    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    %$U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
-    We show that $U$ is a sequence.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
 
-    We show that $A \subseteq (X \setminus B)$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+    Omitted.
 
-    We show that $U$ is a chain of subsets.
-    \begin{subproof}
-        For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
-        It suffices to show that for all $n \in \indexset[U]$ we have
-        for all $m \in \indexset[U]$ such that 
-        $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
-        Fix $n \in \indexset[U]$.
-        Fix $m \in \indexset[U]$.
-        \begin{byCase}
-            \caseOf{$n = 1$.} Trivial.
-            \caseOf{$n = \zero$.} 
-                \begin{byCase}
-                    \caseOf{$m = \zero$.} Trivial.
-                    \caseOf{$m = 1$.} Omitted.
-                \end{byCase}
-        \end{byCase}
-    \end{subproof}
+    %   We show that $U$ is a sequence.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $A \subseteq (\carrier[X] \setminus B)$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $U$ is a chain of subsets.
+    %   \begin{subproof}
+    %       For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
+    %       It suffices to show that for all $n \in \indexset[U]$ we have
+    %       for all $m \in \indexset[U]$ such that 
+    %       $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
+    %       Fix $n \in \indexset[U]$.
+    %       Fix $m \in \indexset[U]$.
+    %       \begin{byCase}
+    %           \caseOf{$n = 1$.} Trivial.
+    %           \caseOf{$n = \zero$.} 
+    %               \begin{byCase}
+    %                   \caseOf{$m = \zero$.} Trivial.
+    %                   \caseOf{$m = 1$.} Omitted.
+    %               \end{byCase}
+    %       \end{byCase}
+    %   \end{subproof}
+%   
+    %   $A \subseteq X$.
+    %   $(X \setminus B) \subseteq X$.
+    %   We show that for all $x \in U$ we have $x \subseteq X$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
+    %   $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
 
-    $A \subseteq X$.
-    $(X \setminus B) \subseteq X$.
-    We show that for all $x \in U$ we have $x \subseteq X$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+    
+\end{proof}
 
-    We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-    We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
-    $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+\begin{proposition}\label{urysohnchain_induction_begin_step_two}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \inter B$ is empty.
+    Suppose there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexset[U]= \{\zero, 1\}$
+    and $\index[U](\zero) = A$
+    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    Then $U$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+    Omitted.
 \end{proof}
 
 
+
 \begin{proposition}\label{t_four_propositon}
     Let $X$ be a urysohn space.
     Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
@@ -295,134 +317,147 @@ The first tept will be a formalisation of chain constructions.
 \end{proof}
 
 
+\begin{proposition}\label{existence_of_staircase_function}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
+    Suppose $k \neq \zero$.
+    Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ 
+    we have $f(x) = \rfrac{n}{k}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{abbreviation}\label{refinment_abbreviation}
+    $x \refine y$ iff $x$ is a refinmant of $y$.
+\end{abbreviation}
 
 
 
 
-
-
-%                    The next thing we need to define is the uniform staircase function.
-%                    This function has it's domain in $X$ and maps to the closed interval $[0,1]$.
-%                    These functions should behave als follows,
-%                    \begin{align}
-%                        &f(A_{0}) = 1 &\text{consant} \\
-%                        &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.}
-%                    \end{align} 
-
-%                    We then prove that for any given $r$ we find a repolished chain,
-%                    which contains the $A_{i}$ and this replished chain is also legal.
-%                     
-%                    The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ 
-%                    be a staircase function with $n$ many refinemants. 
-%                    This limit will be continuous and we would be done. 
-
-
-% TODO: Since we want to prove that $f$ is continus, we have to formalize that 
-% \reals with the usual topology is a topological space. 
-% -------------------------------------------------------------
-
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
-    There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
     and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
 \end{theorem}
 \begin{proof}
-    We show that for all $n \in \naturals$ we have
-    if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ 
-    then there exist $C'$  such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ 
-    and $C'$ is a refinmant of $C$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$.
-
-    
 
-    Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
+    There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
+    and $\indexset[\eta] = \{\zero, 1\}$ 
+    and $\index[\eta](\zero) = A$
+    and $\index[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
     
-    We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
-    and for all $i \in \indexset[\zeta]$ we have 
-    $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
-    and $A \subseteq \index[\zeta](i)$
-    and $\index[\zeta](i) \subseteq (X \setminus B)$
-    and for all $j \in \indexset[\zeta]$ such that 
-    $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
+    We show that there exist $\zeta$ such that $\zeta$ is a sequence 
+    and $\indexset[\zeta] = \naturals$
+    and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$
+    and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
+    and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
     \begin{subproof}
-        Omitted.
-    \end{subproof}
-  
-    
-
-
-    
-
+        %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$.
+        %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$.
+        Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
+        Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
 
-
-    We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$.
-    \begin{subproof}
-        Omitted.
+        % TODO: Proof that \beta is a function which would be used for the indexing.
+        
     \end{subproof}
-    $g$ is a staircase function and $\chain[g] = C$.
-    $g$ is a legal staircase function.
 
 
-    We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
 
 
-    %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. 
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-
-    %Proof Sheme Idea:
-    % -We proof for n=1 that C_{n} is a chain and legal
-    % -Then by induction with P(n+1) is refinmant of P(n)
-    % -Therefore we have a increing refinmant of these Chains such that our limit could even apply
-    % ---------------------------------------------------------
-
-    %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-
-
-    % Formalization idea of enumarted sequences:
-    % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
-    % - This should give all finite and infinte enumarable sequences
-    % - Introduce a notion for the indexing of these enumarable sequences.
-    % - Then we can define the limit of a enumarted sequence of functions.
-    % ---------------------------------------------------------
-    %
-    % Here we need a limit definition for sequences of functions
-    %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-    %
-    %We show that $F(A) = 1$.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-    %
-    %We show that $F(B) = 0$.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof} 
-    %
-    %We show that $F$ is continuous.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
+    %Suppose $\eta$ is a urysohnchain in $X$.
+    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
+    %and $\indexset[\eta] = \{\zero, 1\}$
+    %and $\index[\eta](\zero) = A$ 
+    %and $\index[\eta](1) = (X \setminus B)$.
+
+
+    %Then $\eta$ is a urysohnchain in $X$.
+
+    %   Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
+    %   
+    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+    %   and for all $i \in \indexset[\zeta]$ we have 
+    %   $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+    %   and $A \subseteq \index[\zeta](i)$
+    %   and $\index[\zeta](i) \subseteq (X \setminus B)$
+    %   and for all $j \in \indexset[\zeta]$ such that 
+    %   $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   $g$ is a staircase function and $\chain[g] = C$.
+    %   $g$ is a legal staircase function.
+    %   
+    %   
+    %   We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    %   and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+
+    %   We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. 
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+    %   Proof Sheme Idea:
+    %    -We proof for n=1 that C_{n} is a chain and legal
+    %    -Then by induction with P(n+1) is refinmant of P(n)
+    %    -Therefore we have a increing refinmant of these Chains such that our limit could even apply
+    %    ---------------------------------------------------------
+
+    %   We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+
+    %    Formalization idea of enumarted sequences:
+    %    - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
+    %    - This should give all finite and infinte enumarable sequences
+    %    - Introduce a notion for the indexing of these enumarable sequences.
+    %    - Then we can define the limit of a enumarted sequence of functions.
+    %    ---------------------------------------------------------
+    %   
+    %    Here we need a limit definition for sequences of functions
+    %   We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   We show that $F(A) = 1$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   We show that $F(B) = 0$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof} 
+    %   
+    %   We show that $F$ is continuous.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
 \end{proof}
 
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
-- 
cgit v1.2.3


From e9fa2c5d9539067d9ecce52bbbccacdfd020c563 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 11 Aug 2024 17:10:57 +0200
Subject: more more more urysohn

---
 library/topology/urysohn.tex | 34 +++++++++++++++++++++++++++-------
 1 file changed, 27 insertions(+), 7 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 028e10f..f34f12f 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -5,6 +5,7 @@
 \import{function.tex}
 \import{set.tex}
 \import{cardinal.tex}
+\import{relation.tex}
 
 \section{Urysohns Lemma}
 %           In this section we want to proof Urysohns lemma. 
@@ -188,10 +189,20 @@ The first tept will be a formalisation of chain constructions.
 \end{lemma}
 
 
+\begin{axiom}\label{pot1}
+    $\pot \in \funs{\naturals}{\naturals}$.
+\end{axiom}
 
+\begin{axiom}\label{pot2} 
+    For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$.
+    %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$.
+\end{axiom}
 
 
-
+%Without this abbreviation \pot cant be sed as a function in the standard sense
+\begin{abbreviation}\label{pot_as_function}
+    $\pot(n) = \apply{\pot}{n}$.
+\end{abbreviation}
 
 
 \begin{proposition}\label{urysohnchain_induction_begin}
@@ -356,15 +367,24 @@ The first tept will be a formalisation of chain constructions.
     and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
     and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
     \begin{subproof}
-        %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$.
-        %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$.
-        Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
-        Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
+            %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
+            %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
+            %
+            %    % TODO: Proof that \beta is a function which would be used for the indexing.
+            %For all $n \in \naturals$ we have there exist $x \in \alpha$ such that $(n,x) \in \beta$.
+            %$\dom{\beta} = \naturals$.
+            %$\ran{\beta} = \alpha$.
+            %$\beta \in \funs{\naturals}{\alpha}$.
+            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$.
+        Omitted.
+    \end{subproof}
 
-        % TODO: Proof that \beta is a function which would be used for the indexing.
-        
+    We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
+    \begin{subproof}
+        Trivial.
     \end{subproof}
 
+    
 
 
 
-- 
cgit v1.2.3


From c4894bc4e788fae079b76b824a8d86c167098cc8 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 00:12:07 +0200
Subject: more more way more urysohn

---
 library/topology/urysohn.tex | 127 ++++++++++++++++++++++++++++++++++++++++---
 source/Api.hs                |   8 +--
 source/CommandLine.hs        |   5 +-
 source/Syntax/Lexicon.hs     |   1 +
 4 files changed, 127 insertions(+), 14 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index f34f12f..6662706 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -36,7 +36,12 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-
+%%-----------------------
+%   Idea:
+%   A sequence could be define as a family of sets, 
+%   together with the existence of an indexing function.
+%
+%%-----------------------
 \begin{struct}\label{sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
@@ -148,8 +153,9 @@ The first tept will be a formalisation of chain constructions.
 \end{definition}
 
 \begin{definition}\label{refinmant}
-    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
-    for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
+    $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$
+    and for all $x \in C$ we have $x \in C'$ 
+    and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
     and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
@@ -312,9 +318,9 @@ The first tept will be a formalisation of chain constructions.
     % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
     % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
 
-    Let $m = \max{\indexset[U]}$.
-    For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
-    such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
+    % Let $m = \max{\indexset[U]}$.
+    % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
     
     
     %\begin{definition}\label{refinmant}
@@ -347,6 +353,58 @@ The first tept will be a formalisation of chain constructions.
 
 
 
+
+\begin{abbreviation}\label{sequence_of_functions}
+    $f$ is a sequence of functions iff $f$ is a sequence 
+    and for all $g \in \carrier[f]$ we have $g$ is a function.
+\end{abbreviation}
+
+\begin{abbreviation}\label{sequence_in_reals}
+    $s$ is a sequence of real numbers iff $s$ is a sequence 
+    and for all $r \in \carrier[s]$ we have $r \in \reals$.
+\end{abbreviation}
+
+
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\begin{abbreviation}\label{converge}
+    $s$ converges iff $s$ is a sequence of real numbers 
+    and $\indexset[s]$ is infinite
+    and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
+    there exist $N \in \indexset[s]$ such that
+    for all $m \in \indexset[s]$ such that $m > N$ 
+    we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$.
+\end{abbreviation}
+
+
+\begin{definition}\label{limit_of_sequence}
+    $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
+    and $x \in \reals$ and 
+    for all $\epsilon \in \reals$ such that $\epsilon > \zero$
+    we have there exist $n \in \indexset[s]$ such that 
+    for all $m \in \indexset[s]$ such that $m > n$ 
+    we have $\abs{x - \index[s](n)} < \epsilon$.
+\end{definition}
+
+\begin{proposition}\label{existence_of_limit}
+    Let $s$ be a sequence of real numbers.
+    Then $s$ converges iff there exist $x \in \reals$ 
+    such that $x$ is the limit of $s$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -381,12 +439,65 @@ The first tept will be a formalisation of chain constructions.
 
     We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
-        Trivial.
+        Omitted.
     \end{subproof}
 
-    
+    For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
 
 
+    %%------------- Maybe use Abstrect.hs line 368 "Local Function".
+
+    We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
+    we have $f(x) = \rfrac{n}{\pot(m)}$.
+    \begin{subproof}
+        %   Fix $m \in \indexset[\zeta]$.
+        %   $\index[\zeta](m)$ is a urysohnchain in $X$.
+        %   
+        %   Follows by \cref{existence_of_staircase_function}.
+
+        Omitted.
+    \end{subproof}
+
+    
+
+    %The sequenc of the functions
+    Let $\gamma = \{
+        (n,f) \mid 
+        n \in \naturals \mid 
+        
+        \forall n' \in \indexset[\index[\zeta](n)].             
+        \forall x \in \carrier[X].      
+        
+
+        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
+
+
+        % (n,f) \in \gamma  <=>   \phi(n,f)
+        % with \phi (n,f) :=        (x \in (A_k) \ (A_k-1))                 =>      f(x) = ( k / 2^n )        
+        %                       \/  (x \notin A_k for all k \in {1,..,n}    =>      f(x) = 1 
+
+            (       (n' = \zero)   
+            \land   (x \in \index[\index[\zeta](n)](n')) 
+            \land   (f(x)= \zero) ) 
+        
+        \lor
+        
+            (       (n' > \zero)    
+            \land   (x \in \index[\index[\zeta](n)](n'))
+            \land   (x \notin \index[\index[\zeta](n)](n'-1))
+            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
+            
+        \lor
+
+            (       (x \notin  \index[\index[\zeta](n)](n'))
+            \land   (f(x) = 1) )
+        
+    \}$.
+    
+    
+    
+     
 
     %Suppose $\eta$ is a urysohnchain in $X$.
     %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
diff --git a/source/Api.hs b/source/Api.hs
index f597153..3fb0ca2 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -292,10 +292,10 @@ exportMegalodon file = do
 -- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use
 showFailedTask :: (a, ProverAnswer) -> IO()
 showFailedTask (_, Yes ) = Text.putStrLn ""
-showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("Prover found countermodel: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("Contradictory axioms: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("Out of resources: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("Error at: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
 --showFailedTask (_, _) = Text.putStrLn "Error!"
 
 
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 47efe22..711f7f0 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -87,15 +87,16 @@ run = do
                             Text.hPutStrLn stderr tptp
                         Error err tptp task -> do
                             putStr "Error at:"
+
                             Text.putStrLn task
                             Text.putStrLn err
                             Text.putStrLn tptp
                             
                 WithFailList -> liftIO case result of
-                    VerificationSuccess -> putStrLn "Verification successful."
+                    VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m"
                     VerificationFailure [] -> error "Empty verification fail"
                     VerificationFailure fails -> do
-                        putStrLn "Following task couldn't be solved by the ATP: "
+                        putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m"
                         traverse_ showFailedTask fails
                         Text.hPutStrLn stderr "Don't give up!"
 
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index de6d966..4fe8730 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -112,6 +112,7 @@ prefixOps =
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
     , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
     , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
+    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))    
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
-- 
cgit v1.2.3


From a79924e85260c911045f43bac3f051a8be6e5334 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 00:52:54 +0200
Subject: Completed the structure of the proof of Urysohn. Now every single
 step has to be proven.

---
 library/topology/urysohn.tex | 44 ++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 40 insertions(+), 4 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 6662706..0c4052d 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -410,7 +410,7 @@ The first tept will be a formalisation of chain constructions.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
     There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
+    and $f(A) = 0$ and $f(B)= 1$ and $f$ is continuous.
 \end{theorem}
 \begin{proof}
 
@@ -442,8 +442,10 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
-    For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
-
+    We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
 
     %%------------- Maybe use Abstrect.hs line 368 "Local Function".
 
@@ -495,9 +497,43 @@ 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 $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}
+        Omitted.
+    \end{subproof}
+
+    We show that $F(A) = 0$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that $F(B) = 1$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that $F$ is continuous.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
 
     %Suppose $\eta$ is a urysohnchain in $X$.
     %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
-- 
cgit v1.2.3


From 85920f166c95904550134a1d4e84d5430c05d009 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 11:43:26 +0200
Subject: way more urysohn

---
 library/topology/urysohn.tex | 116 +++++++++++++++++++++++++++++++++++++------
 1 file changed, 102 insertions(+), 14 deletions(-)

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

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}
-- 
cgit v1.2.3


From b51f61e6be5be4729e61ede79fb0bd3cb26f57a6 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 14:41:32 +0200
Subject: way way more urysohn

---
 library/topology/urysohn.tex | 82 +++++++++++++++++++++++---------------------
 source/CommandLine.hs        |  3 ++
 2 files changed, 45 insertions(+), 40 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index d8b1e14..414043f 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -526,6 +526,11 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
+    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
 
 
     We show that there exist $g$ such that 
@@ -535,18 +540,7 @@ The first tept will be a formalisation of chain constructions.
     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)$. 
-        
+    \begin{subproof}       
         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
@@ -554,10 +548,9 @@ The first tept will be a formalisation of chain constructions.
         for all $N' \in \naturals$ such that $N' > N$ we have
         $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$.
         \begin{subproof}
-            Omitted.
+            Fix $x \in \carrier[X]$.
+            Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
         \end{subproof}
-
-
     \end{subproof}
 
 
@@ -581,44 +574,53 @@ The first tept will be a formalisation of chain constructions.
     %\begin{subproof}
     %    Omitted.
     %\end{subproof}
+    
 
+    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
+    We have $\dom{G} = \carrier[X]$.
 
-    
-    We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
-    \begin{subproof}        
+    %For all $x \in \carrier[X]$ for all $n \in \naturals$ we have $g(x) \leq \apply{\gamma(n)}{x}$.
+
+    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
+    \begin{subproof}
+        Fix $x \in \dom{G}$.
+        It suffices to show that $g(x) \in \reals$.
+
+        %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$.
+
+
+
+    \end{subproof}
+
+    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
+    \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) = \zero$.
+
+    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
+    \begin{subproof}        
+        It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
+        It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
+        Fix $x \in \dom{G}$.
+        Then $x \in \carrier[X]$.
+        $g(x) = G(x)$.
+        We have $G(x) \in \reals$.
+        $\zero \leq G(x) \leq 1$.
+        We have $G(x) \in \intervalclosed{\zero}{1}$ .
+    \end{subproof}
+
+    We show that $G(A) = \zero$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
-    We show that $F(B) = 1$.
+    We show that $G(B) = 1$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
-    We show that $F$ is continuous.
+    We show that $G$ is continuous.
     \begin{subproof}
         Omitted.
     \end{subproof}
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 711f7f0..b8c170e 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -43,10 +43,12 @@ run = do
     case withDump opts of
         WithoutDump -> skip
         WithDump dir -> do
+            liftIO (Text.putStrLn "\ESC[1;36mCreating Dumpfiles.\ESC[0m")
             let serials = [dir </> show n <.> "p" | n :: Int <- [1..]]
             tasks <- zip serials <$> encodeTasks (inputPath opts)
             createDirectoryIfMissing True dir
             forM_ tasks (uncurry dumpTask)
+            liftIO (Text.putStrLn "\ESC[35mDump ready.\ESC[0m")
     case (withParseOnly opts, withMegalodon opts) of
         (WithParseOnly, _) -> do
             ast <- parse (inputPath opts)
@@ -60,6 +62,7 @@ run = do
             -- A custom E executable can be configured using environment variables.
             -- If the environment variable is undefined we fall back to the
             -- a globally installed E executable.
+            liftIO (Text.putStrLn "\ESC[1;96mStart of verification.\ESC[0m")
             vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE"
             eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER"
             let prover = case withProver opts of
-- 
cgit v1.2.3


From 8a19eec1e581efa473af0173ba79b553e4191ffa Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 15:55:17 +0200
Subject: way way way more urysohn

---
 library/topology/urysohn.tex | 58 +++++++++++++++++---------------------------
 1 file changed, 22 insertions(+), 36 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 414043f..3be3c30 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -461,8 +461,7 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
-    %%------------- Maybe use Abstrect.hs line 368 "Local Function".
-
+    
     We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
     and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
     we have $f(x) = \rfrac{n}{\pot(m)}$.
@@ -513,13 +512,7 @@ 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}
-
-    %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}
@@ -552,49 +545,42 @@ The first tept will be a formalisation of chain constructions.
             Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
         \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}
     
 
     Let $G(x) = g(x)$ for $x \in \carrier[X]$.
     We have $\dom{G} = \carrier[X]$.
 
-    %For all $x \in \carrier[X]$ for all $n \in \naturals$ we have $g(x) \leq \apply{\gamma(n)}{x}$.
-
     We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
     \begin{subproof}
         Fix $x \in \dom{G}$.
         It suffices to show that $g(x) \in \reals$.
 
-        %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$.
-
+        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$.
+        $g(x)= k$.
+        
 
+        Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
 
     \end{subproof}
 
     We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
     \begin{subproof}
-        Omitted.
+        Fix $x \in \dom{G}$.
+        Then $x \in \carrier[X]$.
+        \begin{byCase}
+            \caseOf{$x \in A$.} 
+                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 0$.
+
+
+            \caseOf{$x \notin A$.} 
+                \begin{byCase}
+                    \caseOf{$x \in B$.} 
+                        OFor all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+
+                    \caseOf{$x \notin B$.}
+                        Omitted.
+                \end{byCase}
+        \end{byCase}
     \end{subproof}
 
 
-- 
cgit v1.2.3


From 41357a4c0ad22b1ea0094ea52c832d117ec3fec4 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 16:30:47 +0200
Subject: way way way way more urysohn

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

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 3be3c30..c94dbd4 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -98,6 +98,10 @@ The first tept will be a formalisation of chain constructions.
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
+\begin{definition}\label{intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
+
 
 \begin{struct}\label{staircase_function}
     A staircase function $f$ is a onesorted structure equipped with
@@ -333,6 +337,34 @@ The first tept will be a formalisation of chain constructions.
 
 \end{proof}
 
+\begin{lemma}\label{fraction1}
+    Let $x \in \reals$.
+    Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{frection2}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $\intervalopen{a}{b}$ is infinite.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{frection3}
+    Suppose $a,b \in \reals$.
+    Suppose $\zero < a < 1$.
+    Suppose $\zero < b < 1$.
+    % Here take exist n such that n/2^n is between a and b
+    T
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
 
 \begin{proposition}\label{existence_of_staircase_function}
     Let $X$ be a urysohn space.
@@ -489,8 +521,9 @@ The first tept will be a formalisation of chain constructions.
 
 
         % (n,f) \in \gamma  <=>   \phi(n,f)
-        % with \phi (n,f) :=        (x \in (A_k) \ (A_k-1))                 =>      f(x) = ( k / 2^n )        
-        %                       \/  (x \notin A_k for all k \in {1,..,n}    =>      f(x) = 1 
+        % with \phi (n,f) :=        
+        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
+        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
 
             (       (n' = \zero)   
             \land   (x \in \index[\index[\zeta](n)](n')) 
@@ -556,7 +589,15 @@ The first tept will be a formalisation of chain constructions.
         It suffices to show that $g(x) \in \reals$.
 
         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$.
-        $g(x)= k$.
+
+        We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
+        \begin{subproof}
+            Fix $\epsilon \in \reals$.
+            %Assume $\epsilon > \zero$.
+            %Take $N' \in \naturals$ such that $\epsilon > \rfrac{1}{\pot(N')}$.
+        \end{subproof}
+
+        
         
 
         Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
@@ -569,13 +610,13 @@ The first tept will be a formalisation of chain constructions.
         Then $x \in \carrier[X]$.
         \begin{byCase}
             \caseOf{$x \in A$.} 
-                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 0$.
+                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
 
 
             \caseOf{$x \notin A$.} 
                 \begin{byCase}
                     \caseOf{$x \in B$.} 
-                        OFor all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+                        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
 
                     \caseOf{$x \notin B$.}
                         Omitted.
-- 
cgit v1.2.3


From ee24a73a01608125e6648f7b66d9c679e955009d Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 13 Aug 2024 23:51:57 +0200
Subject: less urysohn

---
 library/relation.tex         |   1 +
 library/topology/urysohn.tex | 182 +++++++++++++++++++++++++++++++------------
 2 files changed, 133 insertions(+), 50 deletions(-)

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

diff --git a/library/relation.tex b/library/relation.tex
index 4c4065f..d63e747 100644
--- a/library/relation.tex
+++ b/library/relation.tex
@@ -633,6 +633,7 @@ This lets us use the same symbol for composition of functions.
 \begin{proof}
     %$x\in\dom{R}$ and $z\in\ran{S}$.
     There exists $y$ such that $x\mathrel{R} y\mathrel{S} z$ by \cref{circ,pair_eq_iff}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{circ_iff}
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index c94dbd4..ba9780a 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -1,11 +1,17 @@
 \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}
 %           In this section we want to proof Urysohns lemma. 
@@ -337,33 +343,8 @@ The first tept will be a formalisation of chain constructions.
 
 \end{proof}
 
-\begin{lemma}\label{fraction1}
-    Let $x \in \reals$.
-    Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
-\end{lemma}
-\begin{proof}
-    Omitted.
-\end{proof}
 
-\begin{lemma}\label{frection2}
-    Suppose $a,b \in \reals$.
-    Suppose $a < b$.
-    Then $\intervalopen{a}{b}$ is infinite.
-\end{lemma}
-\begin{proof}
-    Omitted.
-\end{proof}
 
-\begin{lemma}\label{frection3}
-    Suppose $a,b \in \reals$.
-    Suppose $\zero < a < 1$.
-    Suppose $\zero < b < 1$.
-    % Here take exist n such that n/2^n is between a and b
-    T
-\end{lemma}
-\begin{proof}
-    Omitted.
-\end{proof}
 
 
 \begin{proposition}\label{existence_of_staircase_function}
@@ -449,6 +430,86 @@ The first tept will be a formalisation of chain constructions.
     $\realsplus = \reals \setminus \realsminus$.
 \end{abbreviation}
 
+\begin{proposition}\label{intervalclosed_subseteq_reals}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $\intervalclosed{a}{b} \subseteq \reals$.
+\end{proposition}
+
+
+
+\begin{lemma}\label{fraction1}
+    Let $x \in \reals$.
+    Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{frection2}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $\intervalopen{a}{b}$ is infinite.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{frection3}
+    Suppose $a \in \reals$.
+    Suppose $a < \zero$.
+    Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. 
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{fraction4}
+    Suppose $a,b,\epsilon \in \reals$.
+    Suppose $\epsilon > \zero$.
+    $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{fraction5}
+    Suppose $a,b,\epsilon \in \reals$.
+    Suppose $\epsilon > \zero$.
+    $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{fraction6}
+    Suppose $a,\epsilon \in \reals$.
+    Suppose $\epsilon > \zero$.
+    $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $.
+\end{proposition}
+
+\begin{abbreviation}\label{epsilonball}
+    $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
+\end{abbreviation}
+
+\begin{proposition}\label{fraction7}
+    Suppose $a,\epsilon \in \reals$.
+    Suppose $\epsilon > \zero$.
+    Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+% 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{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
@@ -483,6 +544,8 @@ 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$.
+
     We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
         Omitted.
@@ -493,6 +556,11 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
+    We show that for all $m \in \naturals$ we have $\pot(m) \in \naturals$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
     
     We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
     and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
@@ -545,37 +613,56 @@ The first tept will be a formalisation of chain constructions.
     
     Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
 
-    
     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 for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+    
+    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
+    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \index[\index[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+    \begin{subproof}
+        Fix $n \in \naturals$.
+        Fix $x \in \carrier[X]$.
+    \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$.
+
+    We show that 
+    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
+    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
+    \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  $g(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{\apply{\gamma(N')}{x} - k} < \epsilon$.
     \begin{subproof}       
-        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$.
+        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}
             Fix $x \in \carrier[X]$.
-            Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+            
+            
+            
+            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
         \end{subproof}
     \end{subproof}
     
@@ -588,20 +675,15 @@ The first tept will be a formalisation of chain constructions.
         Fix $x \in \dom{G}$.
         It suffices to show that $g(x) \in \reals$.
 
-        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$.
+        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$.
 
-        We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
+        We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
         \begin{subproof}
             Fix $\epsilon \in \reals$.
-            %Assume $\epsilon > \zero$.
-            %Take $N' \in \naturals$ such that $\epsilon > \rfrac{1}{\pot(N')}$.
-        \end{subproof}
-
-        
-        
+            
 
+        \end{subproof}
         Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
-
     \end{subproof}
 
     We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
-- 
cgit v1.2.3


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


From 29027c9d2cdbdfe59e48b5aa28eb2d32d1a4c1f7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 24 Aug 2024 11:43:29 +0200
Subject: naproch sty extension

---
 latex/naproche.sty            | 10 ++++++++
 latex/stdlib.tex              |  2 ++
 library/topology/urysohn.tex  | 33 ++++++++++++++-----------
 library/topology/urysohn2.tex | 56 +++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 87 insertions(+), 14 deletions(-)
 create mode 100644 library/topology/urysohn2.tex

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

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}
-- 
cgit v1.2.3


From 565db8eb643673f15c44bd8a8ac30debc9b388fd Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 29 Aug 2024 15:22:11 +0200
Subject: working commit

---
 library/topology/urysohn.tex  | 43 +++++++++++++++++++++++++++++++------------
 library/topology/urysohn2.tex | 30 ++++++++++++++++++++++--------
 2 files changed, 53 insertions(+), 20 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index b8a5fa5..79d65dc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -100,6 +100,14 @@ The first tept will be a formalisation of chain constructions.
 
 \subsection{staircase function}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
 \begin{definition}\label{intervalclosed}
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
@@ -122,6 +130,9 @@ The first tept will be a formalisation of chain constructions.
         \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
         \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. 
         \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$.
+        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ 
+            such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
@@ -311,13 +322,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{definition}\label{minimum}
-    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
-\end{definition}
 
-\begin{definition}\label{maximum}
-    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
-\end{definition}
 
 \begin{proposition}\label{urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
@@ -562,6 +567,16 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
+    Let $\alpha = \carrier[X]$.
+    %Define $f : \alpha \to \naturals$ such that $f(x) =$
+    %\begin{cases}
+    %    & 1        & \text{if} x \in A \lor x \in B 
+    %    & k     & \text{if} \exists k \in \naturals 
+    %\end{cases}
+%
+    %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
+    %$k(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)$.
@@ -581,15 +596,19 @@ The first tept will be a formalisation of chain constructions.
 
     
     We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
+    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ 
     we have $f(x) = \rfrac{n}{\pot(m)}$.
     \begin{subproof}
-        %   Fix $m \in \indexset[\zeta]$.
-        %   $\index[\zeta](m)$ is a urysohnchain in $X$.
-        %   
-        %   Follows by \cref{existence_of_staircase_function}.
+        Fix $m \in \indexset[\zeta]$.
+        $\index[\zeta](m)$ is a urysohnchain in $X$.
+        Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+        \begin{cases}
+            & 0  & \text{if} x \in A 
+            & 1 & \text{if} x \in B 
+            & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
+        \end{cases}
 
-        Omitted.
+        
     \end{subproof}
 
     
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 40a3615..71de210 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -68,18 +68,32 @@
 
     Let $H = \carrier[X] \setminus B$.
     Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$.
+    Let $\eta = \carrier[X]$.
 
-
-
-    Define $f : X \to \reals$ such that  $f(x) = $
+    
+    % Provable 
+    % vvv
+    Define $F : \eta \to \reals$ such that $F(x) =$
     \begin{cases}
-        &(x + k) &\text{if} x \in X \land k \in \naturals
-        & x &\text{if} x \neq \zero
-        & \zero & \text{if} x = \zero
-        % & x ,x \in X    <- will result in technicly ambigus parse
+        & \zero                 &\text{if} x \in  A\\
+        & \rfrac{1}{1+1}    &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
+        & 1                 &\text{if} x \in  B
     \end{cases}
 
-
+    %Define $f : \naturals \to \pow{P}$ such that $f(x)=$
+    %\begin{cases}
+    %    & \emptyset             & \text{if} x = \zero \\
+    %    & \{A, H\}             & \text{if} x = 1  \\
+    %    & G                     & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land  G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \}
+    %\end{cases}
+
+    Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
+    Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
+        $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
+        for all $q_1, q_2, S_1, S_2$ 
+        such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
+        we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
+        and $q \mathrel{R} S$.
     
     Trivial.
     
-- 
cgit v1.2.3


From 8155ba18260743b1e45507e6fb8d4f80c22c425e Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Fri, 30 Aug 2024 19:25:00 +0200
Subject: working commit

---
 library/topology/urysohn.tex | 151 +++++++++++++++++++++++++++++--------------
 1 file changed, 101 insertions(+), 50 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 79d65dc..e1fa924 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -231,6 +231,51 @@ The first tept will be a formalisation of chain constructions.
     $\pot(n) = \apply{\pot}{n}$.
 \end{abbreviation}
 
+%Take all points, besids one but then take all open sets not containing x but all other, so \{x\} has to be closed
+\begin{axiom}\label{hausdorff_implies_singltons_closed}
+    For all $X$ such that $X$ is Hausdorff we have
+    for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
+\end{axiom}
+
+\begin{lemma}\label{urysohn_set_in_between}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \subset B$.
+    %Suppose $B \union A \neq \carrier[X]$.
+    There exist $C \in \closeds{X}$
+    such that $A \subset C \subset B$ or $A, B \in \opens[X]$.
+\end{lemma}
+\begin{proof}
+    We have $B \setminus A$ is inhabited.
+    Take $x$ such that $x \in (B \setminus A)$.
+    Then $A \subset (A \union \{x\})$.
+    Let $C = \closure{A \union \{x\}}{X}$.
+    We have $(A \union \{x\}) \subseteq \closure{A \union \{x\}}{X}$.
+    Therefore $A \subset C$.
+    $A \subseteq B \subseteq \carrier[X]$.
+    $x \in B$.
+    Therefore $x \in \carrier[X]$.
+    $(A \union \{x\}) \subseteq \carrier[X]$.
+    We have $\closure{A \union \{x\}}{X}$ is closed in $X$ by \cref{closure_is_closed}.
+    Therefore $C$ is closed in $X$ by \cref{closure_is_closed}.
+    \begin{byCase}
+        \caseOf{$C = B$.}
+            %We have $\carrier[X] \setminus A$ is open in $X$.    
+            %We have $\carrier[X] \setminus B$ is open in $X$.
+            %$\{x\}$ is closed in $X$.% by \cref{hausdorff_implies_singltons_closed}.
+            %$A \union \{x\} = C$.
+            %$\carrier[X] \setminus (A \union \{x\}) = (\carrier[X] \setminus C)$.
+            %$\carrier[X] \setminus (A) = \{x\} \union (\carrier[X] \setminus C)$.
+
+
+            %Therefore $\{x\}$ is open in $X$.
+            Omitted.
+        \caseOf{$C \neq B$.}
+            Omitted.
+    \end{byCase}
+
+\end{proof}
+
 
 \begin{proposition}\label{urysohnchain_induction_begin}
     Let $X$ be a urysohn space.
@@ -600,15 +645,16 @@ The first tept will be a formalisation of chain constructions.
     we have $f(x) = \rfrac{n}{\pot(m)}$.
     \begin{subproof}
         Fix $m \in \indexset[\zeta]$.
-        $\index[\zeta](m)$ is a urysohnchain in $X$.
-        Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
-        \begin{cases}
-            & 0  & \text{if} x \in A 
-            & 1 & \text{if} x \in B 
-            & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
-        \end{cases}
-
-        
+        %$\index[\zeta](m)$ is a urysohnchain in $X$.
+
+        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+        %\begin{cases}
+        %    & 0  & \text{if} x \in A 
+        %    & 1 & \text{if} x \in B 
+        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
+        %\end{cases}
+%
+        Omitted.
     \end{subproof}
 
     
@@ -677,6 +723,7 @@ The first tept will be a formalisation of chain constructions.
     \begin{subproof}
         Fix $n \in \naturals$.
         Fix $x \in \carrier[X]$.
+        Omitted.
     \end{subproof}
 
 
@@ -696,11 +743,12 @@ The first tept will be a formalisation of chain constructions.
         \begin{subproof}
             Fix $x \in \carrier[X]$.
             
-            
+            Omitted.
             
             % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
             %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
         \end{subproof}
+        Omitted.
     \end{subproof}
     
 
@@ -709,51 +757,54 @@ The first tept will be a formalisation of chain constructions.
 
     We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
     \begin{subproof}
-        Fix $x \in \dom{G}$.
-        It suffices to show that $g(x) \in \reals$.
-
-        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$.
-
-        We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
-        \begin{subproof}
-            Fix $\epsilon \in \reals$.
-            
-
-        \end{subproof}
-        Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
+        %Fix $x \in \dom{G}$.
+        %It suffices to show that $g(x) \in \reals$.
+%
+        %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$.
+%
+        %We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
+        %\begin{subproof}
+        %    Fix $\epsilon \in \reals$.
+        %    
+%
+        %\end{subproof}
+        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
+        Omitted.
     \end{subproof}
 
     We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
     \begin{subproof}
-        Fix $x \in \dom{G}$.
-        Then $x \in \carrier[X]$.
-        \begin{byCase}
-            \caseOf{$x \in A$.} 
-                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
-
-
-            \caseOf{$x \notin A$.} 
-                \begin{byCase}
-                    \caseOf{$x \in B$.} 
-                        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
-
-                    \caseOf{$x \notin B$.}
-                        Omitted.
-                \end{byCase}
-        \end{byCase}
+        %Fix $x \in \dom{G}$.
+        %Then $x \in \carrier[X]$.
+        %\begin{byCase}
+        %    \caseOf{$x \in A$.} 
+        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
+%
+%
+        %    \caseOf{$x \notin A$.} 
+        %        \begin{byCase}
+        %            \caseOf{$x \in B$.} 
+        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+%
+        %            \caseOf{$x \notin B$.}
+        %                Omitted.
+        %        \end{byCase}
+        %\end{byCase}
+        Omitted.
     \end{subproof}
 
 
     We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
     \begin{subproof}        
-        It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
-        It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
-        Fix $x \in \dom{G}$.
-        Then $x \in \carrier[X]$.
-        $g(x) = G(x)$.
-        We have $G(x) \in \reals$.
-        $\zero \leq G(x) \leq 1$.
-        We have $G(x) \in \intervalclosed{\zero}{1}$ .
+        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
+        %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
+        %Fix $x \in \dom{G}$.
+        %Then $x \in \carrier[X]$.
+        %$g(x) = G(x)$.
+        %We have $G(x) \in \reals$.
+        %$\zero \leq G(x) \leq 1$.
+        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
+        Omitted.
     \end{subproof}
 
     We show that $G(A) = \zero$.
@@ -860,7 +911,7 @@ The first tept will be a formalisation of chain constructions.
     %       Omitted.
     %   \end{subproof}
 \end{proof}
-
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
-- 
cgit v1.2.3


From 26cf156763f71aaa9f638408ba4bffb85b886ab0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 31 Aug 2024 18:02:42 +0200
Subject: working commit

---
 library/algebra/group.tex     |  10 +++
 library/topology/urysohn.tex  |   6 ++
 library/topology/urysohn2.tex | 157 +++++++++++++++++++++++++++++++++++-------
 3 files changed, 148 insertions(+), 25 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index a79bd2f..7de1051 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -80,3 +80,13 @@
 \begin{definition}\label{group_automorphism}
     Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
 \end{definition}
+
+\begin{definition}\label{trivial_group}
+    $G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$.
+\end{definition}
+
+\begin{theorem}\label{trivial_implies_abelian}
+    Let $G$ be a group.
+    Suppose $G$ is the trivial group.
+    Then $G$ is an abelian group.
+\end{theorem}
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index e1fa924..17e2911 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -61,6 +61,11 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
 \end{struct}
 
+% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen 
+
+
+
+
 \begin{definition}\label{cahin_of_subsets}
     $C$ is a chain of subsets iff
     $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$.
@@ -237,6 +242,7 @@ The first tept will be a formalisation of chain constructions.
     for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
 \end{axiom}
 
+
 \begin{lemma}\label{urysohn_set_in_between}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 71de210..e963951 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,23 +15,35 @@
 
 \section{Urysohns Lemma}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
+
 
 \begin{definition}\label{one_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
-\begin{struct}\label{sequence}
-    A sequence $X$ is a onesorted structure equipped with
-    \begin{enumerate}
-        \item $\index$
-        \item $\indexset$
-    \end{enumerate}
-    such that
-    \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
-    \end{enumerate}
-\end{struct}
+
+\begin{definition}\label{sequence}
+    $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$.
+\end{definition}
+
 
 \begin{abbreviation}\label{urysohnspace}
     $X$ is a urysohn space iff
@@ -42,10 +54,66 @@
 \end{abbreviation}
 
 
-\begin{definition}\label{intervalclosed}
-    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\begin{abbreviation}\label{at}
+    $\at{f}{n} = f(n)$.
+\end{abbreviation}
+
+
+\begin{definition}\label{chain_of_subsets}
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$. 
+\end{definition}
+
+
+\begin{definition}\label{urysohnchain}%<-- zulässig
+    $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$.
+\end{definition}
+
+
+\begin{definition}\label{finer} %<-- verfeinerung 
+    $X$ is finer then $Y$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $ \closure{\at{X}{n}}{U} \subseteq \interior{\at{Y}{k}}{U} \subseteq \closure{\at{Y}{k}}{U} \subseteq \interior{\at{X}{m}}{U}$.
+\end{definition}
+
+
+\begin{definition}\label{sequence_of_reals}
+    $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$.
+\end{definition}
+
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\begin{definition}\label{realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
 \end{definition}
 
+\begin{definition}\label{realsplus}
+    $\realsplus = \reals \setminus \realsminus$.
+\end{definition}
+
+\begin{definition}\label{epsilon_ball}
+    $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$.
+\end{definition}
+
+\begin{definition}\label{pointwise_convergence}
+    $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+
+
+
+
+
+
+
+
+
+
+
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -55,7 +123,6 @@
 \end{theorem}
 
 
-
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -76,8 +143,8 @@
     Define $F : \eta \to \reals$ such that $F(x) =$
     \begin{cases}
         & \zero                 &\text{if} x \in  A\\
-        & \rfrac{1}{1+1}    &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
-        & 1                 &\text{if} x \in  B
+        & \rfrac{1}{1+1}        &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
+        & 1                     &\text{if} x \in  B
     \end{cases}
 
     %Define $f : \naturals \to \pow{P}$ such that $f(x)=$
@@ -87,19 +154,59 @@
     %    & G                     & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land  G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \}
     %\end{cases}
 
-    Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
-    Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
-        $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
-        for all $q_1, q_2, S_1, S_2$ 
-        such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
-        we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
-        and $q \mathrel{R} S$.
+    %Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
+    %Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
+    %    $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
+    %    for all $q_1, q_2, S_1, S_2$ 
+    %    such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
+    %    we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
+    %    and $q \mathrel{R} S$.
     
-    Trivial.
     
     
+    %Let $J = \{(n,f) \mid n denots the cardinality of a urysohn chain on which f is a staircase function\}$.
+%
+    %Let $N = \naturals$.
+    %Define $j : N \to \funs{\carrier[X]}{\eals}$ such that $j(n) =$
+    %\begin{cases}
+    %    & f     &\text{if} n \in N \land \exist w \in J. J=(n,f)
+    %\end{cases}
+
+
+
+
+
+
+
+
+    
 \end{proof}
 
 \begin{theorem}\label{safe}
     Contradiction.     
 \end{theorem}
+
+
+
+
+%
+%Ideen:
+%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
+%
+%zulässig und verfeinerung von ketten als predicat definieren. 
+%
+%limits und punkt konvergenz als prädikat.
+%
+%
+%Vor dem Beweis vor dem eigentlichen Beweis.
+%die abgeleiteten Funktionen
+%
+%\derivedstiarcasefunction on A
+%
+%abbreviation: \at{f}{n} = f_{n}
+%
+%
+%TODO:
+%Reals ist ein topologischer Raum
+%
+
-- 
cgit v1.2.3


From 588c6ab14184cab4bb7df89def641acaafe3b7eb Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 11:34:01 +0200
Subject: working commit

---
 latex/naproche.sty                          |  20 +-
 latex/stdlib.tex                            |   4 +-
 library/topology/real-topological-space.tex | 121 ++++++-
 library/topology/urysohn.tex                | 515 ++++++++++++++--------------
 library/topology/urysohn2.tex               |  14 +-
 5 files changed, 387 insertions(+), 287 deletions(-)

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

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 5ca673d..1a8afb6 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -40,6 +40,7 @@
 \newtheorem{remark}[theoremcount]{Remark}
 \newtheorem{signature}[theoremcount]{Signature}
 \newtheorem{theorem}[theoremcount]{Theorem}
+\newtheorem{inductive}[theoremcount]{Inductive}
 
 % Theorem environments without numbering.
 \newtheorem*{quotedaxiom}{Axiom}
@@ -139,9 +140,22 @@
 \newcommand{\rationals}{\mathcal{Q}}
 \newcommand{\rminus}{-_{\mathcal{R}}}
 \newcommand{\seq}[2]{\{#1, ... ,#2\}}
-\newcommand{\indexx}[2]{index_{#1}(#2)}
-\newcommand{\indexset}[2]{#1}
-
+\newcommand{\indexx}[2][]{index_{#1}(#2)}
+\newcommand{\indexxset}[1]{#1}
+\newcommand{\topoBasisReals}{\mathbb{B}_{\mathcal{R}}}
+\newcommand{\intervalopen}[2]{(#1, #2)}
+\newcommand{\intervalclosed}[2]{[#1, #2]}
+\newcommand{\epsBall}[2]{\mathcal{B}_{#1,#2}}
+\newcommand{\realsplus}{\reals_{+}}
+\newcommand{\rless}{<}
+\newcommand{\two}{2}
+\newcommand{\powerOfTwoSet}{\mathbb{P}_{2^{}}}
+\newcommand{\pot}{\powerOfTwoSet}
+\newcommand{\chain}[1]{#1}
+\newcommand{\refine}{\text{ finer than }}
+\newcommand{\abs}[1]{\left\lvert#1\right\rvert}
+\newcommand{\realsminus}{\reals_{-}}
+\newcommand{\at}[2]{#1(#2)}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index 2faa267..9879708 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -47,5 +47,7 @@
     \input{../library/topology/disconnection.tex}
     \input{../library/numbers.tex}
     \input{../library/topology/urysohn.tex}
-    \input{../library/wunschzettel.tex}
+    \input{../library/topology/urysohn2.tex}
+    \input{../library/topology/real-topological-space.tex}
+    %\input{../library/wunschzettel.tex}
 \end{document}
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 1c5e4cb..ffdf46e 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{The canonical topology on $\mathbbR$}
+\section{The canonical topology on $\mathbb{R}$}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
@@ -101,12 +101,15 @@
     For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$.
 \end{lemma}
 \begin{proof}
-    %Fix $x,y \in \reals$.
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{reals_order_is_transitive}
     For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
 \end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{lemma}\label{reals_order_plus_minus}
     Suppose $a,b \in \reals$.
@@ -134,16 +137,9 @@
     $x + \epsilon \in \reals$.
 
 
-    %It suffices to show that for all $c$ such that $c \rless x$ we have $c \in \epsBall{x}{\epsilon}$.
-    %Fix $c$ such that $c \rless x$.
-%
-    %It suffices to show that for all $c$ such that $c < x$ we have $c \in \epsBall{x}{\epsilon}$.
-    %Fix $c$ such that $c < x$.
-
-
     It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
     Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$.
-    %Suppose $(x - \epsilon) < c < (x + \epsilon)$.
+    $(x - \epsilon) < c < (x + \epsilon)$.
 \end{proof}
 
 \begin{theorem}\label{topological_basis_reals_is_prebasis}
@@ -158,9 +154,9 @@
             \caseOf{$x = \emptyset$.}
                 Trivial.
             \caseOf{$x \neq \emptyset$.}
-                There exists $U \in \topoBasisReals$ such that $x \in \topoBasisReals$.
-                Take $U \in \topoBasisReals$ such that $x \in \topoBasisReals$.
-
+                %There exists $U \in \topoBasisReals$ such that $x \in U$.
+                Take $U \in \topoBasisReals$ such that $x \in U$.
+                Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}.
         \end{byCase}
     \end{subproof}
     We show that $\reals \subseteq \unions{\topoBasisReals}$.
@@ -168,10 +164,63 @@
         It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
         Fix $x \in \reals$.
         $\epsBall{x}{1} \in \topoBasisReals$.
-        Therefore $x \in \unions{\topoBasisReals}$.
+        Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}.
     \end{subproof}
 \end{proof}
 
+%\begin{lemma}\label{intervl_intersection_is_interval}
+%    Suppose $a,b,a',b' \in \reals$.
+%    Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%    Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%\end{lemma}
+%
+
+\begin{lemma}\label{reals_order_total}
+    For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. 
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. 
+    Fix $x \in \reals$.
+    Fix $y \in \reals$.
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{topo_basis_reals_eps_iff}
+    $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$.
+\end{lemma}
+
+\begin{lemma}\label{topo_basis_reals_intro}
+For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$.
+\end{lemma}
+
+\begin{lemma}\label{realspuls_in_reals_plus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{realspuls_in_reals_minus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{eps_ball_implies_open_interval}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$. 
+    Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+
+\begin{lemma}\label{open_interval_eq_eps_ball}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+\begin{proof}
+    Let $\delta = (b-a)$.
+    $\delta$ is positiv by \cref{minus_}.
+    There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+
+\end{proof}
+
+
+
 \begin{theorem}\label{topological_basis_reals_is_basis}
     $\topoBasisReals$ is a topological basis for $\reals$.
 \end{theorem}
@@ -188,7 +237,45 @@
             Trivial.
         \caseOf{$U \inter V \neq \emptyset$.}
             Then $U \inter V$ is inhabited.
-            %It suffices to show that 
+            $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}.
+            There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$.
+            \begin{subproof}
+                Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+                $x \in \epsBall{x}{\delta}$.
+                $\epsBall{x}{\delta} \subseteq U$.
+                $\epsBall{x}{\delta} \subseteq V$.
+                $\epsBall{x}{\delta} \in B$.
+            \end{subproof}
+            It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+
+
+            %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$.
+            %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            %Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            %\begin{byCase}
+            %    \caseOf{$x_1 = x_2$.}
+            %        Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$.
+            %    \caseOf{$x_1 < x_2$.}
+            %    \caseOf{$x_1 > x_2$.}
+            %\end{byCase}
+            %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$.
+            %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$.
+            %Then $m < x < n$.
+            %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$.
+            %\begin{subproof}
+            %    Suppose not.
+            %    Then For all $y \in U \inter V$ we have $x \leq y$.
+            %\end{subproof}
+            %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$.
+            %\begin{subproof}
+            %    Trivial.
+            %\end{subproof}
     \end{byCase}
 \end{proof}
 
@@ -230,7 +317,3 @@
     Suppose $a,b \in \reals$.
     Then $\intervalopen{a}{b} \in \opens[\reals]$.
 \end{proposition}
-
-\begin{lemma}\label{safetwo}
-    Contradiction.
-\end{lemma}
\ No newline at end of file
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 17e2911..ff6a231 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -51,13 +51,14 @@ The first tept will be a formalisation of chain constructions.
 \begin{struct}\label{sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
-        \item $\index$
-        \item $\indexset$
+        \item $\indexx$
+        \item $\indexxset$
+        
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
+        \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
+        \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
     \end{enumerate}
 \end{struct}
 
@@ -68,13 +69,13 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{definition}\label{cahin_of_subsets}
     $C$ is a chain of subsets iff
-    $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$.
+    $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$.
 \end{definition}
 
 \begin{definition}\label{chain_of_n_subsets}
     $C$ is a chain of $n$ subsets iff
-    $C$ is a chain of subsets and $n \in \indexset[C]$ 
-    and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$.
+    $C$ is a chain of subsets and $n \in \indexxset[C]$ 
+    and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$.
 \end{definition}
 
 
@@ -133,18 +134,18 @@ The first tept will be a formalisation of chain constructions.
         \item \label{staircase_domain} $\dom{f}$ is a topological space.
         \item \label{staricase_def_chain} $C$ is a chain of subsets.
         \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
-        \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. 
+        \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
         \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
-        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$.
-        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ 
-            such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. 
+        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
+        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
+            such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
 \begin{definition}\label{legal_staircase}
     $f$ is a legal staircase function iff
     $f$ is a staircase function and 
-    for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$.
+    for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$.
 \end{definition}
 
 \begin{abbreviation}\label{urysohnspace}
@@ -159,23 +160,23 @@ The first tept will be a formalisation of chain constructions.
     $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
-    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+    for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
 \begin{definition}\label{urysohnchain_without_cardinality}
     $C$ is a urysohnchain in $X$ iff
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
-    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+    for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
 \begin{abbreviation}\label{infinte_sequence}
-    $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite.
+    $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
 \end{abbreviation}
 
 \begin{definition}\label{infinite_product}
     $X$ is the infinite product of $Y$ iff
-    $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$.
+    $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$.
 \end{definition}
 
 \begin{definition}\label{refinmant}
@@ -289,9 +290,9 @@ The first tept will be a formalisation of chain constructions.
     Suppose $A \inter B$ is empty.
     Then there exist $U$
     such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
-    and $\indexset[U]= \{\zero, 1\}$
-    and $\index[U](\zero) = A$
-    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
     %$U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
@@ -310,12 +311,12 @@ The first tept will be a formalisation of chain constructions.
 %   
     %   We show that $U$ is a chain of subsets.
     %   \begin{subproof}
-    %       For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
-    %       It suffices to show that for all $n \in \indexset[U]$ we have
-    %       for all $m \in \indexset[U]$ such that 
-    %       $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
-    %       Fix $n \in \indexset[U]$.
-    %       Fix $m \in \indexset[U]$.
+    %       For all $n \in \indexxset[U]$ we have $n = \zero \lor n = 1$.
+    %       It suffices to show that for all $n \in \indexxset[U]$ we have
+    %       for all $m \in \indexxset[U]$ such that 
+    %       $n < m$ we have $\indexx[U](n) \subseteq \indexx[U](m)$.
+    %       Fix $n \in \indexxset[U]$.
+    %       Fix $m \in \indexxset[U]$.
     %       \begin{byCase}
     %           \caseOf{$n = 1$.} Trivial.
     %           \caseOf{$n = \zero$.} 
@@ -337,8 +338,8 @@ The first tept will be a formalisation of chain constructions.
     %   \begin{subproof}
     %       Omitted.
     %   \end{subproof}
-    %   We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
-    %   $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
+    %   We show that for all $n,m \in \indexxset[U]$ such that $n < m$ we have
+    %   $\closure{\indexx[U](n)}{X} \subseteq \interior{\indexx[U](m)}{X}$.
     %   \begin{subproof}
     %       Omitted.
     %   \end{subproof}
@@ -352,9 +353,9 @@ The first tept will be a formalisation of chain constructions.
     Suppose $A \inter B$ is empty.
     Suppose there exist $U$
     such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
-    and $\indexset[U]= \{\zero, 1\}$
-    and $\index[U](\zero) = A$
-    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
     Then $U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
@@ -384,9 +385,9 @@ The first tept will be a formalisation of chain constructions.
     % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
     % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
 
-    % Let $m = \max{\indexset[U]}$.
-    % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
-    % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
+    % Let $m = \max{\indexxset[U]}$.
+    % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$.
     
     
     %\begin{definition}\label{refinmant}
@@ -408,7 +409,7 @@ The first tept will be a formalisation of chain constructions.
     Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
     Suppose $k \neq \zero$.
     Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ 
+    and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ 
     we have $f(x) = \rfrac{n}{k}$.
 \end{proposition}
 \begin{proof}
@@ -445,11 +446,11 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{abbreviation}\label{converge}
     $s$ converges iff $s$ is a sequence of real numbers 
-    and $\indexset[s]$ is infinite
+    and $\indexxset[s]$ is infinite
     and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
-    there exist $N \in \indexset[s]$ such that
-    for all $m \in \indexset[s]$ such that $m > N$ 
-    we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$.
+    there exist $N \in \indexxset[s]$ such that
+    for all $m \in \indexxset[s]$ such that $m > N$ 
+    we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$.
 \end{abbreviation}
 
 
@@ -457,9 +458,9 @@ The first tept will be a formalisation of chain constructions.
     $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
     and $x \in \reals$ and 
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
-    we have there exist $n \in \indexset[s]$ such that 
-    for all $m \in \indexset[s]$ such that $m > n$ 
-    we have $\abs{x - \index[s](n)} < \epsilon$.
+    we have there exist $n \in \indexxset[s]$ such that 
+    for all $m \in \indexxset[s]$ such that $m > n$ 
+    we have $\abs{x - \indexx[s](n)} < \epsilon$.
 \end{definition}
 
 \begin{proposition}\label{existence_of_limit}
@@ -473,9 +474,9 @@ The first tept will be a formalisation of chain constructions.
 
 \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)$.
+    $x$ is a sequence and $\indexxset[x] = \dom{f}$ and
+    for all $n \in \indexxset[x]$ we have
+    $\indexx[x](n) = f(n)$.
 \end{definition}
 
 \begin{definition}\label{realsminus}
@@ -596,15 +597,15 @@ The first tept will be a formalisation of chain constructions.
 \begin{proof}
     
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
-    and $\indexset[\eta] = \{\zero, 1\}$ 
-    and $\index[\eta](\zero) = A$
-    and $\index[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
+    and $\indexxset[\eta] = \{\zero, 1\}$ 
+    and $\indexx[\eta](\zero) = A$
+    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
     
     We show that there exist $\zeta$ such that $\zeta$ is a sequence 
-    and $\indexset[\zeta] = \naturals$
-    and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$
-    and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
-    and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
+    and $\indexxset[\zeta] = \naturals$
+    and $\eta \in \carrier[\zeta]$ and $\indexx[\zeta](\eta) = \zero$
+    and for all $n \in \indexxset[\zeta]$ we have $n+1 \in \indexxset[\zeta]$ 
+    and $\indexx[\zeta](n+1)$ is a refinmant of $\indexx[\zeta](n)$.
     \begin{subproof}
             %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
             %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
@@ -614,7 +615,7 @@ The first tept will be a formalisation of chain constructions.
             %$\dom{\beta} = \naturals$.
             %$\ran{\beta} = \alpha$.
             %$\beta \in \funs{\naturals}{\alpha}$.
-            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$.
+            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$.
         Omitted.
     \end{subproof}
 
@@ -628,14 +629,14 @@ The first tept will be a formalisation of chain constructions.
     %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
     %$k(x)$
 
-    %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.
+    %For all $n \in \naturals$ we have $\indexx[\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)$.
+    We show that for all $n \in \indexxset[\zeta]$ we have $\indexx[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
-    We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
+    We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$.
     \begin{subproof}
         Omitted.
     \end{subproof}
@@ -646,212 +647,212 @@ The first tept will be a formalisation of chain constructions.
     \end{subproof}
 
     
-    We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ 
-    we have $f(x) = \rfrac{n}{\pot(m)}$.
-    \begin{subproof}
-        Fix $m \in \indexset[\zeta]$.
-        %$\index[\zeta](m)$ is a urysohnchain in $X$.
-
-        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
-        %\begin{cases}
-        %    & 0  & \text{if} x \in A 
-        %    & 1 & \text{if} x \in B 
-        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
-        %\end{cases}
+%    We show that for all $m \in \indexxset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+%    and for all $n \in \indexxset[\indexx[\zeta](m)]$ we have for all $x \in \indexx[\indexx[\zeta](m)](n)$ such that $x \notin \indexx[\indexx[\zeta](m)](n-1)$ 
+%    we have $f(x) = \rfrac{n}{\pot(m)}$.
+%    \begin{subproof}
+%        Fix $m \in \indexxset[\zeta]$.
+%        %$\indexx[\zeta](m)$ is a urysohnchain in $X$.
 %
-        Omitted.
-    \end{subproof}
-
-    
-
-    %The sequenc of the functions
-    Let $\gamma = \{
-        (n,f) \mid 
-        n \in \naturals \mid 
-        
-        \forall n' \in \indexset[\index[\zeta](n)].             
-        \forall x \in \carrier[X].      
-        
-
-        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
-
-
-        % (n,f) \in \gamma  <=>   \phi(n,f)
-        % with \phi (n,f) :=        
-        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
-        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
-
-            (       (n' = \zero)   
-            \land   (x \in \index[\index[\zeta](n)](n')) 
-            \land   (f(x)= \zero) ) 
-        
-        \lor
-        
-            (       (n' > \zero)    
-            \land   (x \in \index[\index[\zeta](n)](n'))
-            \land   (x \notin \index[\index[\zeta](n)](n'-1))
-            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
-            
-        \lor
-
-            (       (x \notin  \index[\index[\zeta](n)](n'))
-            \land   (f(x) = 1) )
-        
-    \}$.
-    
-    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
-
-    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 for all $n \in \naturals$ we have $\gamma(n)$ 
-    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \index[\index[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
-    \begin{subproof}
-        Fix $n \in \naturals$.
-        Fix $x \in \carrier[X]$.
-        Omitted.
-    \end{subproof}
-
-
-
-    We show that 
-    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
-    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
-    \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  $g(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{\apply{\gamma(N')}{x} - k} < \epsilon$.
-    \begin{subproof}       
-        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}
-            Fix $x \in \carrier[X]$.
-            
-            Omitted.
-            
-            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
-            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
-        \end{subproof}
-        Omitted.
-    \end{subproof}
-    
-
-    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
-    We have $\dom{G} = \carrier[X]$.
-
-    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
-    \begin{subproof}
-        %Fix $x \in \dom{G}$.
-        %It suffices to show that $g(x) \in \reals$.
+%        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+%        %\begin{cases}
+%        %    & 0  & \text{if} x \in A 
+%        %    & 1 & \text{if} x \in B 
+%        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \indexx[\indexx[\zeta](m)](n) \land x \notin \indexx[\indexx[\zeta](m)](n-1)
+%        %\end{cases}
+%%
+%        Omitted.
+%    \end{subproof}
 %
-        %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$.
+%    
 %
-        %We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
-        %\begin{subproof}
-        %    Fix $\epsilon \in \reals$.
-        %    
+%    %The sequenc of the functions
+%    Let $\gamma = \{
+%        (n,f) \mid 
+%        n \in \naturals \mid 
+%        
+%        \forall n' \in \indexxset[\indexx[\zeta](n)].             
+%        \forall x \in \carrier[X].      
+%        
 %
-        %\end{subproof}
-        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
-        Omitted.
-    \end{subproof}
-
-    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
-    \begin{subproof}
-        %Fix $x \in \dom{G}$.
-        %Then $x \in \carrier[X]$.
-        %\begin{byCase}
-        %    \caseOf{$x \in A$.} 
-        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
-%
-%
-        %    \caseOf{$x \notin A$.} 
-        %        \begin{byCase}
-        %            \caseOf{$x \in B$.} 
-        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
-%
-        %            \caseOf{$x \notin B$.}
-        %                Omitted.
-        %        \end{byCase}
-        %\end{byCase}
-        Omitted.
-    \end{subproof}
-
-
-    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
-    \begin{subproof}        
-        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
-        %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
-        %Fix $x \in \dom{G}$.
-        %Then $x \in \carrier[X]$.
-        %$g(x) = G(x)$.
-        %We have $G(x) \in \reals$.
-        %$\zero \leq G(x) \leq 1$.
-        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
-        Omitted.
-    \end{subproof}
-
-    We show that $G(A) = \zero$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $G(B) = 1$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $G$ is continuous.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    %Suppose $\eta$ is a urysohnchain in $X$.
-    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
-    %and $\indexset[\eta] = \{\zero, 1\}$
-    %and $\index[\eta](\zero) = A$ 
-    %and $\index[\eta](1) = (X \setminus B)$.
-
-
-    %Then $\eta$ is a urysohnchain in $X$.
-
-    %   Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
-    %   
-    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
-    %   and for all $i \in \indexset[\zeta]$ we have 
-    %   $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
-    %   and $A \subseteq \index[\zeta](i)$
-    %   and $\index[\zeta](i) \subseteq (X \setminus B)$
-    %   and for all $j \in \indexset[\zeta]$ such that 
-    %   $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
-    %   \begin{subproof}
-    %       Omitted.
-    %   \end{subproof}
-    %   
-    %   
-    %   
+%        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
+%
+%
+%        % (n,f) \in \gamma  <=>   \phi(n,f)
+%        % with \phi (n,f) :=        
+%        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
+%        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
+%
+%            (       (n' = \zero)   
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n')) 
+%            \land   (f(x)= \zero) ) 
+%        
+%        \lor
+%        
+%            (       (n' > \zero)    
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n'))
+%            \land   (x \notin \indexx[\indexx[\zeta](n)](n'-1))
+%            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
+%            
+%        \lor
+%
+%            (       (x \notin  \indexx[\indexx[\zeta](n)](n'))
+%            \land   (f(x) = 1) )
+%        
+%    \}$.
+%    
+%    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
+%
+%    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 for all $n \in \naturals$ we have $\gamma(n)$ 
+%    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \indexx[\indexx[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+%    \begin{subproof}
+%        Fix $n \in \naturals$.
+%        Fix $x \in \carrier[X]$.
+%        Omitted.
+%    \end{subproof}
+%
+%
+%
+%    We show that 
+%    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
+%    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
+%    \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  $g(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{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%    \begin{subproof}       
+%        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}
+%            Fix $x \in \carrier[X]$.
+%            
+%            Omitted.
+%            
+%            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%        \end{subproof}
+%        Omitted.
+%    \end{subproof}
+%    
+%
+%    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
+%    We have $\dom{G} = \carrier[X]$.
+%
+%    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %It suffices to show that $g(x) \in \reals$.
+%%
+%        %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$.
+%%
+%        %We show 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} - g(x)} < \epsilon$ and $g(x)= k$.
+%        %\begin{subproof}
+%        %    Fix $\epsilon \in \reals$.
+%        %    
+%%
+%        %\end{subproof}
+%        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %Then $x \in \carrier[X]$.
+%        %\begin{byCase}
+%        %    \caseOf{$x \in A$.} 
+%        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
+%%
+%%
+%        %    \caseOf{$x \notin A$.} 
+%        %        \begin{byCase}
+%        %            \caseOf{$x \in B$.} 
+%        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+%%
+%        %            \caseOf{$x \notin B$.}
+%        %                Omitted.
+%        %        \end{byCase}
+%        %\end{byCase}
+%        Omitted.
+%    \end{subproof}
+%
+%
+%    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
+%    \begin{subproof}        
+%        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
+%        %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
+%        %Fix $x \in \dom{G}$.
+%        %Then $x \in \carrier[X]$.
+%        %$g(x) = G(x)$.
+%        %We have $G(x) \in \reals$.
+%        %$\zero \leq G(x) \leq 1$.
+%        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(A) = \zero$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(B) = 1$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G$ is continuous.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    %Suppose $\eta$ is a urysohnchain in $X$.
+%    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
+%    %and $\indexxset[\eta] = \{\zero, 1\}$
+%    %and $\indexx[\eta](\zero) = A$ 
+%    %and $\indexx[\eta](1) = (X \setminus B)$.
+%
+%
+%    %Then $\eta$ is a urysohnchain in $X$.
+%
+%    %   Take $P$ such that $P$ is a infinite sequence and $\indexxset[P] = \naturals$ and for all $i \in \indexxset[P]$ we have $\indexx[P](i) = \pow{X}$.
+%    %   
+%    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+%    %   and for all $i \in \indexxset[\zeta]$ we have 
+%    %   $\indexx[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+%    %   and $A \subseteq \indexx[\zeta](i)$
+%    %   and $\indexx[\zeta](i) \subseteq (X \setminus B)$
+%    %   and for all $j \in \indexxset[\zeta]$ such that 
+%    %   $j < i$ we have for all $x \in \indexx[\zeta](j)$ we have $x \in \indexx[\zeta](i)$.
+%    %   \begin{subproof}
+%    %       Omitted.
+%    %   \end{subproof}
+%    %   
+%    %   
+%    %   
     %   
     %   
     %   
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 838b121..83e3aa4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -367,10 +367,10 @@
             \end{subproof}
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
-            Define $V : N \to M$ such that $V(n)=$
+            Define $V : N \to M$ such that $V(n)=
             \begin{cases}
-                &\at{U}{F(n)} & \text{if} n \in N
-            \end{cases}
+                \at{U}{F(n)} & \text{if} n \in N
+            \end{cases}$
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
@@ -445,11 +445,11 @@
     $B \subseteq X'$ by \cref{powerset_elim,closeds}.
     $A \subseteq X'$.
     Therefore $A \subseteq A'$.
-    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$
+    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =
     \begin{cases}
-        &A  &\text{if} n = \zero \\
-        &A' &\text{if} n = 1
-    \end{cases}
+        A  &\text{if} n = \zero \\
+        A' &\text{if} n = 1
+    \end{cases}$
     $U_0$ is a function.
     $\dom{U_0} = N$.
     $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
-- 
cgit v1.2.3


From 29f32e2031eafa087323d79d812a1b38ac78f977 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 01:20:05 +0200
Subject: working commit

---
 library/nat.tex                             |  22 +--
 library/topology/real-topological-space.tex |   2 +-
 library/topology/urysohn.tex                | 140 +++++++--------
 library/topology/urysohn2.tex               | 254 +++++++++++++++++++++-------
 4 files changed, 278 insertions(+), 140 deletions(-)

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

diff --git a/library/nat.tex b/library/nat.tex
index ac9a141..841ac36 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -3,48 +3,48 @@
 
 \section{Natural numbers}
 
-\begin{abbreviation}\label{inductive_set}
+\begin{abbreviation}\label{num_inductive_set}
     $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
 \end{abbreviation}
 
-\begin{axiom}\label{naturals_inductive_set}
+\begin{axiom}\label{num_naturals_inductive_set}
     $\naturals$ is an inductive set.
 \end{axiom}
 
-\begin{axiom}\label{naturals_smallest_inductive_set}
+\begin{axiom}\label{num_naturals_smallest_inductive_set}
     Let $A$ be an inductive set.
     Then $\naturals\subseteq A$.
 \end{axiom}
 
-\begin{abbreviation}\label{naturalnumber}
+\begin{abbreviation}\label{num_naturalnumber}
     $n$ is a natural number iff $n\in \naturals$.
 \end{abbreviation}
 
-\begin{lemma}\label{emptyset_in_naturals}
+\begin{lemma}\label{num_emptyset_in_naturals}
     $\emptyset\in\naturals$.    
 \end{lemma}
 
-\begin{signature}\label{addition_is_set}
+\begin{signature}\label{num_addition_is_set}
     $x+y$ is a set.
 \end{signature}
 
-\begin{axiom}\label{addition_on_naturals}
+\begin{axiom}\label{num_addition_on_naturals}
     $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number.
 \end{axiom}
 
-\begin{abbreviation}\label{zero_is_emptyset}
+\begin{abbreviation}\label{num_zero_is_emptyset}
     $\zero = \emptyset$.
 \end{abbreviation}
 
-\begin{axiom}\label{addition_axiom_1}
+\begin{axiom}\label{num_addition_axiom_1}
     For all $x \in \naturals$ $x + \zero = \zero + x = x$.
 \end{axiom}
 
-\begin{axiom}\label{addition_axiom_2}
+\begin{axiom}\label{num_addition_axiom_2}
     For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
 \end{axiom}
 
-\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+\begin{lemma}\label{num_naturals_is_equal_to_two_times_naturals}
     $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
 \end{lemma}
 
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index b2e5ea9..c76fd46 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{The canonical topology on $\mathbb{R}$}
+\section{Topology Reals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ff6a231..ae03273 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -36,7 +36,7 @@ The first tept will be a formalisation of chain constructions.
 %           $\overline{A_{i-1}}  \subset \interior{A_{i}}$. 
 %           In this case we call the chain legal.
 
-\begin{definition}\label{one_to_n_set}
+\begin{definition}\label{urysohnone_one_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
@@ -48,7 +48,7 @@ The first tept will be a formalisation of chain constructions.
 %   together with the existence of an indexing function.
 %
 %%-----------------------
-\begin{struct}\label{sequence}
+\begin{struct}\label{urysohnone_sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\indexx$
@@ -57,8 +57,8 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
+        \item\label{urysohnone_indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
+        \item\label{urysohnone_index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
     \end{enumerate}
 \end{struct}
 
@@ -67,12 +67,12 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{definition}\label{cahin_of_subsets}
+\begin{definition}\label{urysohnone_cahin_of_subsets}
     $C$ is a chain of subsets iff
     $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$.
 \end{definition}
 
-\begin{definition}\label{chain_of_n_subsets}
+\begin{definition}\label{urysohnone_chain_of_n_subsets}
     $C$ is a chain of $n$ subsets iff
     $C$ is a chain of subsets and $n \in \indexxset[C]$ 
     and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$.
@@ -84,7 +84,7 @@ The first tept will be a formalisation of chain constructions.
 % and also for the subproof of continuity of the limit.
 
 
-%     \begin{definition}\label{legal_chain}
+%     \begin{definition}\label{urysohnone_legal_chain}
 %         $C$ is a legal chain of subsets of $X$ iff 
 %         $C \subseteq \pow{X}$. %and 
 %         %there exist $f \in \funs{C}{\naturals}$ such that
@@ -106,49 +106,49 @@ The first tept will be a formalisation of chain constructions.
 
 \subsection{staircase function}
 
-\begin{definition}\label{minimum}
+\begin{definition}\label{urysohnone_minimum}
     $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
 \end{definition}
 
-\begin{definition}\label{maximum}
+\begin{definition}\label{urysohnone_maximum}
     $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
 \end{definition}
 
-\begin{definition}\label{intervalclosed}
+\begin{definition}\label{urysohnone_intervalclosed}
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
-\begin{definition}\label{intervalopen}
+\begin{definition}\label{urysohnone_intervalopen}
     $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
 \end{definition}
 
 
-\begin{struct}\label{staircase_function}
+\begin{struct}\label{urysohnone_staircase_function}
     A staircase function $f$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\chain$
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
-        \item \label{staircase_domain} $\dom{f}$ is a topological space.
-        \item \label{staricase_def_chain} $C$ is a chain of subsets.
-        \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
-        \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
-        \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
-        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
-        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
+        \item \label{urysohnone_staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
+        \item \label{urysohnone_staircase_domain} $\dom{f}$ is a topological space.
+        \item \label{urysohnone_staricase_def_chain} $C$ is a chain of subsets.
+        \item \label{urysohnone_staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
+        \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
+        \item \label{urysohnone_staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+        \item \label{urysohnone_staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
+        \item \label{urysohnone_staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
             such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
-\begin{definition}\label{legal_staircase}
+\begin{definition}\label{urysohnone_legal_staircase}
     $f$ is a legal staircase function iff
     $f$ is a staircase function and 
     for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$.
 \end{definition}
 
-\begin{abbreviation}\label{urysohnspace}
+\begin{abbreviation}\label{urysohnone_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$
@@ -156,49 +156,49 @@ The first tept will be a formalisation of chain constructions.
     such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
 \end{abbreviation}
 
-\begin{definition}\label{urysohnchain}
+\begin{definition}\label{urysohnone_urysohnchain}
     $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{definition}\label{urysohnchain_without_cardinality}
+\begin{definition}\label{urysohnone_urysohnchain_without_cardinality}
     $C$ is a urysohnchain in $X$ iff
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{abbreviation}\label{infinte_sequence}
+\begin{abbreviation}\label{urysohnone_infinte_sequence}
     $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
 \end{abbreviation}
 
-\begin{definition}\label{infinite_product}
+\begin{definition}\label{urysohnone_infinite_product}
     $X$ is the infinite product of $Y$ iff
     $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$.
 \end{definition}
 
-\begin{definition}\label{refinmant}
+\begin{definition}\label{urysohnone_refinmant}
     $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$
     and for all $x \in C$ we have $x \in C'$ 
     and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
     and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
-\begin{abbreviation}\label{two}
+\begin{abbreviation}\label{urysohnone_two}
     $\two = \suc{1}$.
 \end{abbreviation}
 
-\begin{lemma}\label{two_in_reals}
+\begin{lemma}\label{urysohnone_two_in_reals}
     $\two \in \reals$.
 \end{lemma}
 
-\begin{lemma}\label{two_in_naturals}
+\begin{lemma}\label{urysohnone_two_in_naturals}
     $\two \in \naturals$.
 \end{lemma}
 
-\begin{inductive}\label{power_of_two}
+\begin{inductive}\label{urysohnone_power_of_two}
     Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
     \begin{enumerate}
         \item  $(\zero, 1) \in \powerOfTwoSet$.
@@ -206,45 +206,45 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
 \end{inductive}
 
-\begin{abbreviation}\label{pot}
+\begin{abbreviation}\label{urysohnone_pot}
     $\pot = \powerOfTwoSet$.
 \end{abbreviation}
 
-\begin{lemma}\label{dom_pot}
+\begin{lemma}\label{urysohnone_dom_pot}
     $\dom{\pot} = \naturals$.
 \end{lemma}
 \begin{proof}
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{ran_pot}
+\begin{lemma}\label{urysohnone_ran_pot}
     $\ran{\pot} \subseteq \naturals$.
 \end{lemma}
 
 
-\begin{axiom}\label{pot1}
+\begin{axiom}\label{urysohnone_pot1}
     $\pot \in \funs{\naturals}{\naturals}$.
 \end{axiom}
 
-\begin{axiom}\label{pot2} 
+\begin{axiom}\label{urysohnone_pot2} 
     For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$.
     %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$.
 \end{axiom}
 
 
 %Without this abbreviation \pot cant be sed as a function in the standard sense
-\begin{abbreviation}\label{pot_as_function}
+\begin{abbreviation}\label{urysohnone_pot_as_function}
     $\pot(n) = \apply{\pot}{n}$.
 \end{abbreviation}
 
 %Take all points, besids one but then take all open sets not containing x but all other, so \{x\} has to be closed
-\begin{axiom}\label{hausdorff_implies_singltons_closed}
+\begin{axiom}\label{urysohnone_hausdorff_implies_singltons_closed}
     For all $X$ such that $X$ is Hausdorff we have
     for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
 \end{axiom}
 
 
-\begin{lemma}\label{urysohn_set_in_between}
+\begin{lemma}\label{urysohnone_urysohn_set_in_between}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \subset B$.
@@ -284,7 +284,7 @@ The first tept will be a formalisation of chain constructions.
 \end{proof}
 
 
-\begin{proposition}\label{urysohnchain_induction_begin}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -347,7 +347,7 @@ The first tept will be a formalisation of chain constructions.
     
 \end{proof}
 
-\begin{proposition}\label{urysohnchain_induction_begin_step_two}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -364,7 +364,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{t_four_propositon}
+\begin{proposition}\label{urysohnone_t_four_propositon}
     Let $X$ be a urysohn space.
     Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
     we have there exists $C \subseteq X$ such that 
@@ -376,7 +376,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{urysohnchain_induction_step_existence}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$.
     Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
@@ -390,7 +390,7 @@ The first tept will be a formalisation of chain constructions.
     % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$.
     
     
-    %\begin{definition}\label{refinmant}
+    %\begin{definition}\label{urysohnone_refinmant}
     %    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
     %    for all $y \in C$ such that $y \subset x$ 
     %    we have there exist $c \in C'$ such that $y \subset c \subset x$
@@ -404,7 +404,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{existence_of_staircase_function}
+\begin{proposition}\label{urysohnone_existence_of_staircase_function}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
     Suppose $k \neq \zero$.
@@ -416,7 +416,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{abbreviation}\label{refinment_abbreviation}
+\begin{abbreviation}\label{urysohnone_refinment_abbreviation}
     $x \refine y$ iff $x$ is a refinmant of $y$.
 \end{abbreviation}
 
@@ -424,27 +424,27 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{abbreviation}\label{sequence_of_functions}
+\begin{abbreviation}\label{urysohnone_sequence_of_functions}
     $f$ is a sequence of functions iff $f$ is a sequence 
     and for all $g \in \carrier[f]$ we have $g$ is a function.
 \end{abbreviation}
 
-\begin{abbreviation}\label{sequence_in_reals}
+\begin{abbreviation}\label{urysohnone_sequence_in_reals}
     $s$ is a sequence of real numbers iff $s$ is a sequence 
     and for all $r \in \carrier[s]$ we have $r \in \reals$.
 \end{abbreviation}
 
 
 
-\begin{axiom}\label{abs_behavior1}
+\begin{axiom}\label{urysohnone_abs_behavior1}
     If $x \geq \zero$ then $\abs{x} = x$.
 \end{axiom}
 
-\begin{axiom}\label{abs_behavior2}
+\begin{axiom}\label{urysohnone_abs_behavior2}
     If $x < \zero$ then $\abs{x} = \neg{x}$.
 \end{axiom}
 
-\begin{abbreviation}\label{converge}
+\begin{abbreviation}\label{urysohnone_converge}
     $s$ converges iff $s$ is a sequence of real numbers 
     and $\indexxset[s]$ is infinite
     and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
@@ -454,7 +454,7 @@ The first tept will be a formalisation of chain constructions.
 \end{abbreviation}
 
 
-\begin{definition}\label{limit_of_sequence}
+\begin{definition}\label{urysohnone_limit_of_sequence}
     $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
     and $x \in \reals$ and 
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
@@ -463,7 +463,7 @@ The first tept will be a formalisation of chain constructions.
     we have $\abs{x - \indexx[s](n)} < \epsilon$.
 \end{definition}
 
-\begin{proposition}\label{existence_of_limit}
+\begin{proposition}\label{urysohnone_existence_of_limit}
     Let $s$ be a sequence of real numbers.
     Then $s$ converges iff there exist $x \in \reals$ 
     such that $x$ is the limit of $s$.
@@ -472,22 +472,22 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{definition}\label{limit_sequence}
+\begin{definition}\label{urysohnone_limit_sequence}
     $x$ is the limit sequence of $f$ iff
     $x$ is a sequence and $\indexxset[x] = \dom{f}$ and
     for all $n \in \indexxset[x]$ we have
     $\indexx[x](n) = f(n)$.
 \end{definition}
 
-\begin{definition}\label{realsminus}
+\begin{definition}\label{urysohnone_realsminus}
     $\realsminus = \{r \in \reals \mid r < \zero\}$.
 \end{definition}
 
-\begin{abbreviation}\label{realsplus}
+\begin{abbreviation}\label{urysohnone_realsplus}
     $\realsplus = \reals \setminus \realsminus$.
 \end{abbreviation}
 
-\begin{proposition}\label{intervalclosed_subseteq_reals}
+\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalclosed{a}{b} \subseteq \reals$.
@@ -495,7 +495,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{lemma}\label{fraction1}
+\begin{lemma}\label{urysohnone_fraction1}
     Let $x \in \reals$.
     Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
 \end{lemma}
@@ -503,7 +503,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection2}
+\begin{lemma}\label{urysohnone_frection2}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalopen{a}{b}$ is infinite.
@@ -512,7 +512,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection3}
+\begin{lemma}\label{urysohnone_frection3}
     Suppose $a \in \reals$.
     Suppose $a < \zero$.
     Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. 
@@ -521,7 +521,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction4}
+\begin{proposition}\label{urysohnone_fraction4}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
@@ -530,7 +530,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction5}
+\begin{proposition}\label{urysohnone_fraction5}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$.
@@ -539,17 +539,17 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction6}
+\begin{proposition}\label{urysohnone_fraction6}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $.
 \end{proposition}
 
-\begin{abbreviation}\label{epsilonball}
+\begin{abbreviation}\label{urysohnone_epsilonball}
     $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
 \end{abbreviation}
 
-\begin{proposition}\label{fraction7}
+\begin{proposition}\label{urysohnone_fraction7}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$.
@@ -561,11 +561,11 @@ The first tept will be a formalisation of chain constructions.
 
 
  
-%\begin{definition}\label{sequencetwo}
+%\begin{definition}\label{urysohnone_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}
+%\begin{proposition}\label{urysohnone_sequence_existence}
 %    Suppose $N \subseteq \naturals$.
 %    Suppose $M \subseteq \naturals$.
 %    Suppose $N = M$.
@@ -586,7 +586,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{theorem}\label{urysohn}
+\begin{theorem}\label{urysohnone_urysohn1}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -599,7 +599,7 @@ The first tept will be a formalisation of chain constructions.
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
     and $\indexxset[\eta] = \{\zero, 1\}$ 
     and $\indexx[\eta](\zero) = A$
-    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
+    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnone_urysohnchain_induction_begin}.
     
     We show that there exist $\zeta$ such that $\zeta$ is a sequence 
     and $\indexxset[\zeta] = \naturals$
@@ -919,6 +919,6 @@ The first tept will be a formalisation of chain constructions.
     %   \end{subproof}
 \end{proof}
 %
-%\begin{theorem}\label{safe}
+%\begin{theorem}\label{urysohnone_safe}
 %    Contradiction.     
 %\end{theorem}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ce6d742..08841da 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -40,7 +40,7 @@
 
 
 \begin{definition}\label{chain_of_subsets}
-    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $n < m$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
 \end{definition}
 
 
@@ -49,11 +49,11 @@
 \end{definition}
 
 \begin{definition}\label{urysohn_finer_set}
-    $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$.
+    $A$ is finer between $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$.
 \end{definition}
 
 \begin{definition}\label{finer} %<-- verfeinerung 
-    $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$.
+    $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$.
 \end{definition}
 
 \begin{definition}\label{follower_index}
@@ -92,6 +92,46 @@
     $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$.
 \end{definition}
 
+
+%\begin{definition}\label{staircase}
+%    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$.
+%\end{definition}
+
+
+\begin{definition}\label{staircase_step_value1}
+    $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value2}
+    $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value3}
+    $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$.
+\end{definition}
+
+
+\begin{definition}\label{staircase2}
+    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_sequence}
+    $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_limit_point}
+    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+%\begin{definition}\label{staircase_limit_function}
+%    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+%\end{definition}
+%
+\begin{definition}\label{staircase_limit_function}
+    $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+\end{definition}
+
+
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
@@ -659,33 +699,26 @@
 \end{proof}
 
 
-\begin{definition}\label{staircase}
-    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
-\end{definition}
-
-\begin{definition}\label{staircase_sequence}
-    $S$ is staircase sequence of $U$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_point}
-    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_function}
-    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-\end{definition}
+\begin{proposition}\label{staircase_ran_in_zero_to_one}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $f$ is a staircase function adapted to $U$ in $X$.
+    Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
-%\begin{definition}\label{staircase_limit_function}
-%    $f$ is a limit function of staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-%\end{definition}
-%
-%\begin{proposition}\label{staircase_limit_is_continuous}
-%    Suppose $X$ is a urysohnspace.
-%    Suppose $U$ is a lifted urysohnchain of $X$.
-%    Suppose $S$ is staircase sequence of $U$.
-%    Suppose $f$ is the limit function of a staircase $S$.
-%    Then $f$ is continuous.
-%\end{proposition}
+\begin{proposition}\label{staircase_limit_is_continuous}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a lifted urysohnchain of $X$.
+    Suppose $S$ is staircase sequence of $U$ in $X$.
+    Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
@@ -712,8 +745,26 @@
     Omitted.
 \end{proof}
 
+\begin{lemma}\label{fractions_between_zero_one}
+    Suppose $n,m \in \naturals$.
+    Suppose $m > n$.
+    Then $\zero \leq \rfrac{n}{m} \leq 1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{lemma}\label{intervalclosed_border_is_elem}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $a,b \in \intervalclosed{a}{b}$.  
+\end{lemma}
 
+\begin{lemma}\label{urysohnchain_subseteqrel}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$.
+\end{lemma}
 
 
 \begin{theorem}\label{urysohn}
@@ -721,8 +772,8 @@
     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.
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f$ is continuous
+    and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$.
 \end{theorem}
 \begin{proof}
     Let $X' = \carrier[X]$.
@@ -796,46 +847,133 @@
     \end{subproof}
     Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
 
-    We show that there exist $S$ such that $S$ is staircase sequence of $U$.
+    We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$.
     \begin{subproof}
         Omitted.
     \end{subproof}
-    Take $S$ such that $S$ is staircase sequence of $U$.
+    Take $S$ such that $S$ is staircase sequence of $U$ in $X$.
 
     %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
 %
     %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
-%
+    We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+    We show that $\dom{f} = \carrier[X]$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    $f$ is a function.
+    We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+    \begin{subproof}
+        It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$.
+        It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$.
+        Fix $x \in \dom{f}$.
+        $f(x)$ is the staircase limit of $S$ with $x$.
+        Therefore $f(x) \in \reals$.
+        
+        We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+        \begin{subproof}
+            Fix $n \in \naturals$.
+            Let $g = \at{S}{n}$.
+            Let $U' = \at{U}{n}$.
+            $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            $g$ is a staircase function adapted to $U'$ in $X$.
+            $U'$ is a urysohnchain of $X$.
+            $g$ is a function from $\carrier[X]$ to $\reals$.
+            It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}.
+            It suffices to show that for all $x \in \dom{g}$ we have $g(x) \in \intervalclosed{\zero}{1}$.
+            Fix $x\in \dom{g}$.
+            Then $x \in \carrier[X]$.
+            \begin{byCase}
+                \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
+                    Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
+                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
+                    Then $g(x) = 1$ .
+                \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
+                    \begin{byCase}
+                        \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
+                            $g(x) = \zero$.
+                        \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
+                            Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                    \end{byCase}
+            \end{byCase}
+
+            
+
+            %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            %$\at{U}{n}$ is a urysohnchain of $X$.
+            %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$.
+            %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %\begin{byCase}
+            %    \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        $1 \in \intervalclosed{\zero}{1}$.
+            %        We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$.
+            %        \begin{subproof}
+            %            Omitted.
+            %        \end{subproof}
+            %        Then $\apply{\at{S}{n}}{x} = 1$.
+            %    \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Then  $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$.
+            %        It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$.
+            %        $\zero \leq m' \leq k$.
+            %\end{byCase}
+            %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$.
+            %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$.
+        \end{subproof}
+
+        Suppose not.
+        Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}.
+        For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}.
+        \begin{byCase}
+            \caseOf{$f(x) < \zero$.}
+                Let $\delta = \zero - f(x)$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+            \caseOf{$f(x) > 1$.}
+                Let $\delta = f(x) - 1$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+        \end{byCase}
+
+    \end{subproof}
+    Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}.
+
+    We show that for all $a \in A$ we have $f(a) = \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    We show that for all $b \in B$ we have $f(b) = 1$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
 
-    
 \end{proof}
 
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
 
 
 
 
 
-%
-%Ideen:
-%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
-%
-%zulässig und verfeinerung von ketten als predicat definieren. 
-%
-%limits und punkt konvergenz als prädikat.
-%
-%
-%Vor dem Beweis vor dem eigentlichen Beweis.
-%die abgeleiteten Funktionen
-%
-%\derivedstiarcasefunction on A
-%
-%abbreviation: \at{f}{n} = f_{n}
-%
-%
-%TODO:
-%Reals ist ein topologischer Raum
-%
 
-- 
cgit v1.2.3


From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 03:05:41 +0200
Subject: Abgabe

---
 library/algebra/group.tex                   |  2 +-
 library/algebra/monoid.tex                  |  2 +-
 library/cardinal.tex                        |  2 +-
 library/numbers.tex                         |  2 +-
 library/topology/basis.tex                  |  2 +-
 library/topology/continuous.tex             |  2 ++
 library/topology/metric-space.tex           |  4 ++--
 library/topology/real-topological-space.tex |  2 +-
 library/topology/separation.tex             |  2 ++
 library/topology/topological-space.tex      |  2 +-
 library/topology/urysohn.tex                |  4 ++--
 library/topology/urysohn2.tex               | 18 ++++++++++++++----
 12 files changed, 29 insertions(+), 15 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 7de1051..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index 06fcb50..3249a93 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -1,5 +1,5 @@
 \import{algebra/semigroup.tex}
-\section{Monoid}
+\section{Monoid}\label{form_sec_monoid}
 
 \begin{struct}\label{monoid}
     A monoid $A$ is a semigroup equipped with
diff --git a/library/cardinal.tex b/library/cardinal.tex
index 044e5d1..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,4 +1,4 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \import{set.tex}
 \import{ordinal.tex}
diff --git a/library/numbers.tex b/library/numbers.tex
index ac0a683..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,7 +4,7 @@
 \import{ordinal.tex}
 
 
-\section{The real numbers}
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 052c551..f0f77e4 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -2,7 +2,7 @@
 \import{set.tex}
 \import{set/powerset.tex}
 
-\subsection{Topological basis}
+\subsection{Topological basis}\label{form_sec_topobasis}
 
 \begin{abbreviation}\label{covers}
     $C$ covers $X$ iff
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index a9bc58e..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -3,6 +3,8 @@
 \import{function.tex}
 \import{set.tex}
 
+\subsection{Continuous}\label{form_sec_continuous}
+
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
 \end{definition}
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 0ed7bab..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,10 +4,10 @@
 \import{set/powerset.tex}
 \import{topology/basis.tex}
 
-\section{Metric Spaces}
+\section{Metric Spaces}\label{form_sec_metric}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index c76fd46..db7ee94 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{Topology Reals}
+\section{Topology Reals}\label{form_sec_toporeals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 0c68290..aaa3907 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,6 +1,8 @@
 \import{topology/topological-space.tex}
 \import{set.tex}
 
+\subsection{Separation}\label{form_sec_separation}
+
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
     $X$ is Kolmogorov iff
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index f8bcb93..409e107 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -2,7 +2,7 @@
 \import{set/powerset.tex}
 \import{set/cons.tex}
 
-\section{Topological spaces}
+\section{Topological spaces}\label{form_sec_topospaces}
 
 \begin{struct}\label{topological_space}
     A topological space $X$ is a onesorted structure equipped with
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ae03273..cd85fbc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,7 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
 %           In this section we want to proof Urysohns lemma. 
 %           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
 %           The Idea is to construct staircase functions as a chain.
@@ -22,7 +22,7 @@
 
 %Chains of  sets.
 
-The first tept will be a formalisation of chain constructions.
+This is the first attempt to prove Urysohns Lemma with the usage of struct. 
 
 \subsection{Chains of sets}
 %           Assume $A,B$ are subsets of a topological space $X$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 08841da..a1a3ba0 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,7 +15,7 @@
 \import{topology/real-topological-space.tex}
 \import{set/equinumerosity.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma}\label{form_sec_urysohn}
 
 
 
@@ -891,15 +891,25 @@
             \begin{byCase}
                 \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
                     Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
-                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                     Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
-                    Then $g(x) = 1$ .
+                    We show that $g(x) = 1$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                 \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
                     \begin{byCase}
                         \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
-                            $g(x) = \zero$.
+                            We show that $g(x) = \zero$.
+                            \begin{subproof}
+                                Omitted.
+                            \end{subproof}
                         \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
                             Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                            Omitted.
                     \end{byCase}
             \end{byCase}
 
-- 
cgit v1.2.3

