Linting

2 files changed, 155 insertions, 155 deletions

diff --git a/library/numbers.tex b/library/numbers.tex
index d3af3f1..a675ea5 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -93,8 +93,8 @@
     For all $n,m \in \naturals$ we have $(n + m) \in \naturals$.
 \end{axiom}
 
-\subsubsection{Natural numbers as ordinals}
 
+\subsubsection{Natural numbers as ordinals}
 
 \begin{lemma}\label{nat_is_successor_ordinal}
     Let $n\in\naturals$.
@@ -187,7 +187,7 @@
     Follows by \cref{suc_eq_plus_one,naturals_addition_axiom_2,naturals_addition_axiom_1,naturals_inductive_set,one_is_suc_zero}.
 \end{proof}
 
-\begin{proposition}\label{naturals_add_kommu}
+\begin{proposition}\label{naturals_add_comm}
     For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$.
 \end{proposition}
 \begin{proof}
@@ -235,17 +235,17 @@
     \end{align*}
 \end{proof}
 
-\begin{proposition}\label{naturals_add_remove_brakets}
+\begin{proposition}\label{naturals_add_remove_parens}
     Suppose $n,m,k \in \naturals$.
-    Then $(n + m) + k = n + m + k = n + (m + k)$.    
+    Then $(n + m) + k = n + m + k = n + (m + k)$.
 \end{proposition}
 
-\begin{proposition}\label{naturals_add_remove_brakets2}
+\begin{proposition}\label{naturals_add_remove_parens2}
     Suppose $n,m,k,l \in \naturals$.
-    Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.    
+    Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.
 \end{proposition}
 
-%\begin{proposition}\label{natural_disstro_oneline}
+%\begin{proposition}\label{natural_distrib_oneline}
 %    Suppose $n,m,k \in \naturals$.
 %    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
 %\end{proposition}
@@ -262,7 +262,7 @@
 %    $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k')  = ((n \rmul m') + (n \rmul k')) + m' + k'    = (((n \rmul m') + (n \rmul k')) + m') + k'  = (m' + ((n \rmul m') + (n \rmul k'))) + k'  = ((m' + (n \rmul m')) + (n \rmul k')) + k'  = (((n \rmul m') + m') + (n \rmul k')) + k'  = ((n \rmul m') + m') + ((n \rmul k') + k')  = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
 %\end{proof}
 
-\begin{proposition}\label{natural_disstro}
+\begin{proposition}\label{natural_distrib}
     Suppose $n,m,k \in \naturals$.
     Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
 \end{proposition}
@@ -283,11 +283,11 @@
         \suc{n} \rmul (m' + k') \\
         &= (n \rmul (m' + k')) + (m' + k') \\% \explanation{by \cref{naturals_mul_axiom_2}}\\
         &= ((n \rmul m') + (n \rmul k')) + (m' + k') \\%\explanation{by assumption}\\
-        &= ((n \rmul m') + (n \rmul k')) + m' + k'   \\%\explanation{by \cref{naturals_add_remove_brakets,naturals_add_kommu}}\\
-        &= (((n \rmul m') + (n \rmul k')) + m') + k' \\%\explanation{by \cref{naturals_add_kommu,naturals_add_remove_brakets,naturals_add_assoc}}\\
-        &= (m' + ((n \rmul m') + (n \rmul k'))) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
+        &= ((n \rmul m') + (n \rmul k')) + m' + k'   \\%\explanation{by \cref{naturals_add_remove_parens,naturals_add_comm}}\\
+        &= (((n \rmul m') + (n \rmul k')) + m') + k' \\%\explanation{by \cref{naturals_add_comm,naturals_add_remove_parens,naturals_add_assoc}}\\
+        &= (m' + ((n \rmul m') + (n \rmul k'))) + k' \\%\explanation{by \cref{naturals_add_comm}}\\
         &= ((m' + (n \rmul m')) + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_assoc}}\\
-        &= (((n \rmul m') + m') + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
+        &= (((n \rmul m') + m') + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_comm}}\\
         &= ((n \rmul m') + m') + ((n \rmul k') + k') \\%\explanation{by \cref{naturals_add_assoc}}\\
         &= (\suc{n} \rmul m') + (\suc{n} \rmul k')   %\explanation{by \cref{naturals_mul_axiom_2}}
     \end{align*}
@@ -353,7 +353,7 @@
         &=(k' \rmul (n' \rmul m')) + (k' \rmul m')  \\
         &=k' \rmul ((n' \rmul m') + m')             \\
         &=k' \rmul (\suc{n'} \rmul m')              \\
-        &=(\suc{n'} \rmul m') \rmul k'              
+        &=(\suc{n'} \rmul m') \rmul k'
     \end{align*}
 \end{proof}
 
@@ -385,7 +385,7 @@ Commutivatiy of the standart operations
 \begin{axiom}\label{reals_axiom_kommu}
     For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$.
 \end{axiom}
-  
+
 \begin{axiom}\label{reals_axiom_assoc}
     For all $x,y,z \in \reals$ we have $(x + y) + z = x + (y + z)$.
 \end{axiom}
@@ -393,7 +393,7 @@ Commutivatiy of the standart operations
 
 Existence of  one and Zero
 \begin{axiom}\label{reals_axiom_zero}
-    For all $x \in \reals$ $x + \zero = x$. 
+    For all $x \in \reals$ $x + \zero = x$.
 \end{axiom}
 
 \begin{axiom}\label{reals_axiom_one}
@@ -453,7 +453,7 @@ Laws of the order on the reals
 \end{axiom}
 
 \begin{axiom}\label{reals_dense}
-    For all $x,y \in \reals$ if $x < y$ then 
+    For all $x,y \in \reals$ if $x < y$ then
     there exist $z \in \reals$ such that $x < z$ and $z < y$.
 \end{axiom}
 
@@ -471,15 +471,15 @@ Laws of the order on the reals
 \end{axiom}
 
 \begin{axiom}\label{reals_postiv_mul_is_positiv}
-    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
+    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$.
 \end{axiom}
 
 \begin{axiom}\label{reals_postiv_mul_negativ_is_negativ}
-    For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$. 
+    For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$.
 \end{axiom}
 
 \begin{axiom}\label{reals_negativ_mul_is_negativ}
-    For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$. 
+    For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$.
 \end{axiom}
 
 
@@ -603,12 +603,12 @@ Laws of the order on the reals
 
 %\begin{abbreviation}\label{gcd}
 %    $g$ is greatest common divisor of $\{a,b\}$ iff
-%    $g$ is a integral divisor of $a$ 
-%    and $g$ is a integral divisor of $b$ 
+%    $g$ is a integral divisor of $a$
+%    and $g$ is a integral divisor of $b$
 %    and for all $g'$ such that $g'$ is a integral divisor of $a$
 %    and $g'$ is a integral divisor of $b$ we have $g' \leq g$.
 %\end{abbreviation}
-% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, 
+% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung,
 
 
 \subsection{Order on the reals}
@@ -664,8 +664,8 @@ Laws of the order on the reals
 
 \begin{lemma}\label{order_reals_lemma1}
     Let $x,y,z \in \reals$.
-    Suppose $\zero < x$. 
-    Suppose $y < z$. 
+    Suppose $\zero < x$.
+    Suppose $y < z$.
     Then $(y \rmul x) < (z \rmul x)$.
 \end{lemma}
 \begin{proof}
@@ -675,15 +675,15 @@ Laws of the order on the reals
     %    (z \rmul x) \\
     %    &= ((y + k) \rmul x) \\
     %    &= ((y \rmul x) + (k \rmul x)) \explanation{by \cref{reals_disstro2}}
-    %\end{align*} 
-    %Then $(k \rmul x) > \zero$. 
+    %\end{align*}
+    %Then $(k \rmul x) > \zero$.
     %Therefore $(z \rmul x) > (y \rmul x)$.
 \end{proof}
 
 \begin{lemma}\label{order_reals_lemma2}
     Let $x,y,z \in \reals$.
-    Suppose $\zero < x$. 
-    Suppose $y < z$. 
+    Suppose $\zero < x$.
+    Suppose $y < z$.
     Then $(x \rmul y) < (x \rmul z)$.
 \end{lemma}
 \begin{proof}
@@ -693,8 +693,8 @@ Laws of the order on the reals
 
 \begin{lemma}\label{order_reals_lemma3}
     Let $x,y,z \in \reals$.
-    Suppose $\zero > x$. 
-    Suppose $y < z$. 
+    Suppose $\zero > x$.
+    Suppose $y < z$.
     Then $(x \rmul z) < (x \rmul y)$.
 \end{lemma}
 \begin{proof}
@@ -808,7 +808,7 @@ Laws of the order on the reals
 
 
 \begin{definition}\label{m_to_n_set}
-    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.
 \end{definition}
 
 \begin{axiom}\label{abs_behavior1}
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index cd85fbc..bfbf54d 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,8 +13,8 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
-%           In this section we want to proof Urysohns lemma. 
+\section{Urysohns Lemma Part One 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.
 %           The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$.
@@ -22,29 +22,29 @@
 
 %Chains of  sets.
 
-This is the first attempt to prove Urysohns Lemma with the usage of struct. 
+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$.
 
 %           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. 
+%           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}}$. 
+%               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{urysohnone_one_to_n_set}
-    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.
 \end{definition}
 
 
 
 %%-----------------------
 %   Idea:
-%   A sequence could be define as a family of sets, 
+%   A sequence could be define as a family of sets,
 %   together with the existence of an indexing function.
 %
 %%-----------------------
@@ -53,7 +53,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     \begin{enumerate}
         \item $\indexx$
         \item $\indexxset$
-        
+
     \end{enumerate}
     such that
     \begin{enumerate}
@@ -62,7 +62,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     \end{enumerate}
 \end{struct}
 
-% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen 
+% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen
 
 
 
@@ -74,7 +74,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 \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]$ 
+    $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}
 
@@ -85,19 +85,19 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 
 %     \begin{definition}\label{urysohnone_legal_chain}
-%         $C$ is a legal chain of subsets of $X$ iff 
-%         $C \subseteq \pow{X}$. %and 
+%         $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. 
+% 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). 
+% 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)
 % ---------------------------------------------------------------
@@ -134,17 +134,17 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
         \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_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]} }$. 
+        \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{urysohnone_legal_staircase}
     $f$ is a legal staircase function iff
-    $f$ is a staircase function and 
+    $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}
 
@@ -153,7 +153,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     $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$.    
+    such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.
 \end{abbreviation}
 
 \begin{definition}\label{urysohnone_urysohnchain}
@@ -181,7 +181,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 \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 $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}
@@ -226,7 +226,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     $\pot \in \funs{\naturals}{\naturals}$.
 \end{axiom}
 
-\begin{axiom}\label{urysohnone_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}
@@ -267,7 +267,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     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 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$.
@@ -303,37 +303,37 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     %   \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 \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 
+    %       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$.} 
+    %           \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.
@@ -344,7 +344,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     %       Omitted.
     %   \end{subproof}
 
-    
+
 \end{proof}
 
 \begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two}
@@ -367,7 +367,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 \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 
+    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}
@@ -386,13 +386,13 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
 
     % Let $m = \max{\indexxset[U]}$.
-    % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % 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{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$ 
+    %    $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}
@@ -408,8 +408,8 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     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 \indexxset[U]$ we have for all $x \in \indexx[U](n)$ 
+    Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$
+    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}
@@ -425,12 +425,12 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 
 \begin{abbreviation}\label{urysohnone_sequence_of_functions}
-    $f$ is a sequence of functions iff $f$ is a sequence 
+    $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{urysohnone_sequence_in_reals}
-    $s$ is a sequence of real numbers iff $s$ is a sequence 
+    $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}
 
@@ -445,27 +445,27 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 \end{axiom}
 
 \begin{abbreviation}\label{urysohnone_converge}
-    $s$ converges iff $s$ is a sequence of real numbers 
+    $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
     there exist $N \in \indexxset[s]$ such that
-    for all $m \in \indexxset[s]$ such that $m > N$ 
+    for all $m \in \indexxset[s]$ such that $m > N$
     we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$.
 \end{abbreviation}
 
 
 \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 
+    and $x \in \reals$ and
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
-    we have there exist $n \in \indexxset[s]$ such that 
-    for all $m \in \indexxset[s]$ such that $m > n$ 
+    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{urysohnone_existence_of_limit}
     Let $s$ be a sequence of real numbers.
-    Then $s$ converges iff there exist $x \in \reals$ 
+    Then $s$ converges iff there exist $x \in \reals$
     such that $x$ is the limit of $s$.
 \end{proposition}
 \begin{proof}
@@ -515,7 +515,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 \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$. 
+    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.
@@ -560,7 +560,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 
 
- 
+
 %\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}
@@ -591,20 +591,20 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     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}}$ 
+    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}
-    
-    There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
-    and $\indexxset[\eta] = \{\zero, 1\}$ 
+
+    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{urysohnone_urysohnchain_induction_begin}.
-    
-    We show that there exist $\zeta$ such that $\zeta$ is a sequence 
+
+    We show that there exist $\zeta$ such that $\zeta$ is a sequence
     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 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\}$.
@@ -622,8 +622,8 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
     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 
+    %    & 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
@@ -646,9 +646,9 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
         Omitted.
     \end{subproof}
 
-    
-%    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 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]$.
@@ -656,61 +656,61 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %
 %        %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 
+%        %    & 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}
 %
-%    
+%
 %
 %    %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].      
-%        
+%        (n,f) \mid
+%        n \in \naturals \mid
+%
+%        \forall n' \in \indexxset[\indexx[\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 \indexx[\indexx[\zeta](n)](n')) 
-%            \land   (f(x)= \zero) ) 
-%        
+%        % 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)    
+%
+%            (       (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)$ 
+%    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)$ 
+%
+%    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.
@@ -726,7 +726,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %        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$ 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]$.
@@ -735,29 +735,29 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %
 %
 %
-%    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$ 
+%    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} 
+%    \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}       
+%    \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]$.
@@ -772,7 +772,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %        %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}.
@@ -784,13 +784,13 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %        %Fix $x \in \dom{G}$.
 %        %Then $x \in \carrier[X]$.
 %        %\begin{byCase}
-%        %    \caseOf{$x \in A$.} 
+%        %    \caseOf{$x \in A$.}
 %        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
 %%
 %%
-%        %    \caseOf{$x \notin A$.} 
+%        %    \caseOf{$x \notin A$.}
 %        %        \begin{byCase}
-%        %            \caseOf{$x \in B$.} 
+%        %            \caseOf{$x \in B$.}
 %        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
 %%
 %        %            \caseOf{$x \notin B$.}
@@ -802,7 +802,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %
 %
 %    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
-%    \begin{subproof}        
+%    \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}$.
@@ -832,48 +832,48 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %    %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](\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 
+%    %
+%    %   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 
+%    %   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}
-%    %   
-%    %   
-%    %   
-    %   
-    %   
-    %   
-    %   
-    %   
+%    %
+%    %
+%    %
+    %
+    %
+    %
+    %
+    %
     %   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}}$ 
+    %
+    %
+    %   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$. 
+    %   We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$.
     %   \begin{subproof}
     %       Omitted.
     %   \end{subproof}
@@ -891,28 +891,28 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 
 
     %    Formalization idea of enumarted sequences:
-    %    - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
+    %    - 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} 
-    %   
+    %   \end{subproof}
+    %
     %   We show that $F$ is continuous.
     %   \begin{subproof}
     %       Omitted.
@@ -920,5 +920,5 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 \end{proof}
 %
 %\begin{theorem}\label{urysohnone_safe}
-%    Contradiction.     
+%    Contradiction.
 %\end{theorem}