From 0c82b10cd3ac1787838038b4b443f79cbb1612d9 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 26 Jun 2024 13:56:47 +0200
Subject: Working at the numbers.tex

---
 library/numbers.tex | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 1837ae8..f13214d 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -1,5 +1,6 @@
 \import{order/order.tex}
 \import{relation.tex}
+\import{set/suc.tex}
 
 \section{The real numbers}
 
@@ -15,6 +16,11 @@
     $x \rmul y$ is a set.
 \end{signature}
 
+%Structure TODO:
+% Take as may axioms as needed  - Tarski Axioms of reals
+%Implement Naturals -> Integer -> rationals -> reals 
+
+
 \subsection{Basic axioms of the reals}
 
 \begin{axiom}\label{reals_axiom_zero_in_reals}
@@ -29,6 +35,26 @@
     $\zero \neq 1$.
 \end{axiom}
 
+\begin{inductive}\label{naturals_subset_reals}
+    Define $\naturals \subseteq \reals$ inductively as follows.
+    \begin{enumerate}
+        \item $\zero \in \naturals$.
+        \item If $n\in \naturals$, then $\successor{n} \in \naturals$. 
+    \end{enumerate}
+\end{inductive}
+
+%\begin{axiom}\label{negativ_is_set}
+%    $\negativ{x}$ is a set.
+%\end{axiom}
+
+%\begin{axiom}\label{negativ_of}
+%    $\negativ{x} \in \reals$ iff $x\in \reals$.
+%\end{axiom}
+%
+%\begin{axiom}\label{negativ_behavior}
+%    $x + \negativ{x} = \zero$.
+%\end{axiom}
+
 \begin{definition}\label{reals_definition_order_def}
     $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$.
 \end{definition}
-- 
cgit v1.2.3


From 7e65d40f100af326adbd4ef1d32fdd0aabc92f4b Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 2 Jul 2024 11:05:31 +0200
Subject: Definition and axioms of naturals.

---
 library/numbers.tex | 191 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 135 insertions(+), 56 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index f13214d..4b5d10b 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -2,6 +2,7 @@
 \import{relation.tex}
 \import{set/suc.tex}
 
+
 \section{The real numbers}
 
 \begin{signature}
@@ -16,12 +17,47 @@
     $x \rmul y$ is a set.
 \end{signature}
 
+\begin{axiom}\label{reals_axiom_order}
+    $\lt[\reals]$ is an order on $\reals$.
+\end{axiom}
+
+\begin{abbreviation}\label{lesseq_on_reals}
+    $x \leq y$ iff $(x,y) \in \lt[\reals]$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{less_on_reals}
+    $x < y$ iff it is wrong that $y \leq x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y \leq x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff it is wrong that $x < y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{is_positiv}
+    $x$ is positiv iff $x > \zero$.
+\end{abbreviation}
+
+
 %Structure TODO:
 % Take as may axioms as needed  - Tarski Axioms of reals
 %Implement Naturals -> Integer -> rationals -> reals 
 
 
-\subsection{Basic axioms of the reals}
+\subsection{Creation of natural numbers}
+
+\subsubsection{Defenition and axioms}
+
+\begin{abbreviation}\label{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{abbreviation}\label{zero_is_emptyset}
+    $\zero = \emptyset$.
+\end{abbreviation}
 
 \begin{axiom}\label{reals_axiom_zero_in_reals}
     $\zero \in \reals$.
@@ -35,49 +71,101 @@
     $\zero \neq 1$.
 \end{axiom}
 
-\begin{inductive}\label{naturals_subset_reals}
-    Define $\naturals \subseteq \reals$ inductively as follows.
-    \begin{enumerate}
-        \item $\zero \in \naturals$.
-        \item If $n\in \naturals$, then $\successor{n} \in \naturals$. 
-    \end{enumerate}
-\end{inductive}
-
-%\begin{axiom}\label{negativ_is_set}
-%    $\negativ{x}$ is a set.
-%\end{axiom}
-
-%\begin{axiom}\label{negativ_of}
-%    $\negativ{x} \in \reals$ iff $x\in \reals$.
-%\end{axiom}
-%
-%\begin{axiom}\label{negativ_behavior}
-%    $x + \negativ{x} = \zero$.
-%\end{axiom}
-
-\begin{definition}\label{reals_definition_order_def}
-    $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$.
+\begin{axiom}\label{one_is_suc_zero}
+    $\suc{\zero} = 1$.
+\end{axiom}
+
+\begin{definition}\label{naturals}
+    $\naturals = \{ x \in \reals \mid \exists y \in \reals. \suc{y} = x \lor x = \zero \}$.
 \end{definition}
 
-%\begin{axiom}\label{reals_axiom_order}
-%    $\lt[\reals]$ is an order on $\reals$.
-%\end{axiom}
+\begin{lemma}\label{naturals_subseteq_reals}
+    $\naturals \subseteq \reals$.
+\end{lemma}
 
-%\begin{abbreviation}\label{lesseq_on_reals}
-%    $x \leq y$ iff $(x,y) \in \lt[\reals]$.
-%\end{abbreviation}
+%\begin{inductive}\label{naturals_subset_reals}
+%    Define $\naturals \subseteq \reals$ inductively as follows.
+%    \begin{enumerate}
+%        \item $\zero \in \naturals$.
+%        \item If $n\in \naturals$, then $\suc{n} \in \naturals$.   %Naproche translate this to for all n \in R \suc{n} \in R we want something like the definition before. 
+%    \end{enumerate}
+%\end{inductive}
 
-\begin{abbreviation}\label{less_on_reals}
-    $x \leq y$ iff it is wrong that $y < x$.
-\end{abbreviation}
+\begin{axiom}\label{suc_eq_plus_one}
+    For all $n \in \naturals$ we have $\suc{n} = n + 1$.
+\end{axiom}
 
-\begin{abbreviation}\label{greater_on_reals}
-    $x > y$ iff $y \leq x$.
+\begin{abbreviation}\label{is_a_natural_number}
+    $n$ is a natural number iff $n \in \naturals$.
 \end{abbreviation}
 
-\begin{abbreviation}\label{greatereq_on_reals}
-    $x \geq y$ iff it is wrong that $x < y$.
-\end{abbreviation}
+\begin{axiom}\label{naturals_addition_axiom_1}
+    For all $n \in \naturals$ $n + \zero = \zero + n = n$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_addition_axiom_2}
+    For all $n, m \in \naturals$ $n + \suc{m} = \suc{n} + m = \suc{n+m}$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_mul_axiom_1}
+    For all $n \in \naturals$ we have $n \rmul \zero = \zero$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_mul_axiom_2}
+    For all $n,m \in \naturals$ we have $\suc{n} \rmul m = (n \rmul m) + m$.
+\end{axiom}
+
+\begin{axiom}\label{addition_on_naturals}
+    If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number.
+\end{axiom}
+
+
+\subsubsection{Properties and Facts natural numbers}
+
+\begin{proposition}\label{naturals_kommu}
+    For all $n,m \in \naturals$ we have $n + m = m + n$.
+\end{proposition}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$n = \emptyset$.} Trivial.
+        \caseOf{$m = \emptyset$.} Trivial.
+        \caseOf{$n \neq \emptyset \land m \neq \emptyset$.} Omitted.
+    \end{byCase}
+\end{proof}
+    
+
+
+\begin{lemma}\label{naturals_inductive_set}
+    $\naturals$ is an inductive set.
+\end{lemma}
+
+
+\begin{lemma}\label{naturals_smallest_inductive_set}
+    Let $A$ be an inductive set.
+    Then $\naturals\subseteq A$.
+\end{lemma}
+
+
+\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+%\begin{lemma}\label{oeder_on_naturals}
+%    $\lt[\reals] \inter (\naturals \times \naturals)$ is an order on $\naturals$.
+%\end{lemma}
+
+
+
+
+
+
+\subsection{The Intergers}
+
+
+
 
 \begin{axiom}\label{reals_axiom_dense}
     For all $x,y \in \reals$ if $x < y$ then 
@@ -127,7 +215,9 @@
 \begin{proposition}\label{reals_reducion_on_addition}
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{proposition}
-
+\begin{proof}
+    Omitted.
+\end{proof}
 
 
 %\begin{signature}\label{invers_is_set}
@@ -147,9 +237,7 @@
 %    $x \rminus \addInv{x} = \zero$.
 %\end{lemma}
 
-\begin{abbreviation}\label{is_positiv}
-    $x$ is positiv iff $x > \zero$.
-\end{abbreviation}
+
 
 \begin{lemma}\label{reals_add_of_positiv}
     Let $x,y \in \reals$.
@@ -221,7 +309,9 @@
 \begin{lemma}\label{order_reals_lemma00}
     For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$.
 \end{lemma}
-
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{lemma}\label{order_reals_lemma5}
     For all $x,y \in \reals$ such that $x < y$ we have $x \leq y$.
@@ -289,24 +379,13 @@
 
 
 
-\section{The natural numbers}
 
 
-\begin{abbreviation}\label{def_suc}
-    $\successor{n} = n + 1$.
-\end{abbreviation}
 
-\begin{inductive}\label{naturals_definition_as_subset_of_reals}
-    Define $\nat \subseteq \reals$ inductively as follows.
-    \begin{enumerate}
-        \item $\zero \in \nat$.
-        \item If $n\in \nat$, then $\successor{n} \in \nat$. 
-    \end{enumerate}
-\end{inductive}
 
-\begin{lemma}\label{reals_order_suc}
-    $n < \successor{n}$.
-\end{lemma}
+
+
+
 
 %\begin{proposition}\label{safe}
 %    Contradiction.
-- 
cgit v1.2.3


From bff76c7fabb9f2c0b9dcac915dfa68e930baf4d4 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 2 Jul 2024 21:24:44 +0200
Subject: Further Formalisation of naturals. Such as induction on naturals and
 addition laws.

---
 library/numbers.tex | 177 +++++++++++++++++++++++++++++++++++++++++-----------
 library/ordinal.tex | 107 +++++++++++++++----------------
 2 files changed, 195 insertions(+), 89 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 4b5d10b..b83827a 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -1,6 +1,7 @@
 \import{order/order.tex}
 \import{relation.tex}
 \import{set/suc.tex}
+\import{ordinal.tex}
 
 
 \section{The real numbers}
@@ -75,24 +76,17 @@
     $\suc{\zero} = 1$.
 \end{axiom}
 
-\begin{definition}\label{naturals}
-    $\naturals = \{ x \in \reals \mid \exists y \in \reals. \suc{y} = x \lor x = \zero \}$.
-\end{definition}
-
-\begin{lemma}\label{naturals_subseteq_reals}
+\begin{axiom}\label{naturals_subseteq_reals}
     $\naturals \subseteq \reals$.
-\end{lemma}
+\end{axiom}
 
-%\begin{inductive}\label{naturals_subset_reals}
-%    Define $\naturals \subseteq \reals$ inductively as follows.
-%    \begin{enumerate}
-%        \item $\zero \in \naturals$.
-%        \item If $n\in \naturals$, then $\suc{n} \in \naturals$.   %Naproche translate this to for all n \in R \suc{n} \in R we want something like the definition before. 
-%    \end{enumerate}
-%\end{inductive}
+\begin{axiom}\label{naturals_inductive_set}
+    $\naturals$ is an inductive set.
+\end{axiom}
 
-\begin{axiom}\label{suc_eq_plus_one}
-    For all $n \in \naturals$ we have $\suc{n} = n + 1$.
+\begin{axiom}\label{naturals_smallest_inductive_set}
+    Let $A$ be an inductive set.
+    Then $\naturals\subseteq A$.
 \end{axiom}
 
 \begin{abbreviation}\label{is_a_natural_number}
@@ -119,33 +113,147 @@
     If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number.
 \end{axiom}
 
+\subsubsection{Natural numbers as ordinals}
 
-\subsubsection{Properties and Facts natural numbers}
 
-\begin{proposition}\label{naturals_kommu}
-    For all $n,m \in \naturals$ we have $n + m = m + n$.
-\end{proposition}
+\begin{lemma}\label{nat_is_successor_ordinal}
+    Let $n\in\naturals$.
+    Suppose $n\neq \emptyset$.
+    Then $n$ is a successor ordinal.
+\end{lemma}
 \begin{proof}
-    \begin{byCase}
-        \caseOf{$n = \emptyset$.} Trivial.
-        \caseOf{$m = \emptyset$.} Trivial.
-        \caseOf{$n \neq \emptyset \land m \neq \emptyset$.} Omitted.
-    \end{byCase}
+    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
+    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
+    Now $M\subseteq \naturals\subseteq M$
+        by \cref{subseteq,naturals_smallest_inductive_set}.
+    Thus $M = \naturals$.
+    Follows by \cref{subseteq}.
 \end{proof}
-    
 
+\begin{lemma}\label{nat_is_transitiveset}
+    $\naturals$ is \in-transitive.
+\end{lemma}
+\begin{proof}
+    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
+    $\emptyset\in M$.
+    For all $n\in M$ we have $\suc{n}\in M$
+        by \cref{naturals_inductive_set,suc}.
+    Thus $M$ is an inductive set.
+    Now $M\subseteq \naturals\subseteq M$
+        by \cref{subseteq,naturals_smallest_inductive_set}.
+    Hence $\naturals = M$.
+\end{proof}
 
-\begin{lemma}\label{naturals_inductive_set}
-    $\naturals$ is an inductive set.
+\begin{lemma}\label{natural_number_is_ordinal}
+    Every natural number is an ordinal.
 \end{lemma}
+\begin{proof}
+    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
+\end{proof}
 
+\begin{lemma}\label{omega_is_an_ordinal}
+    $\naturals$ is an ordinal.
+\end{lemma}
+\begin{proof}
+    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
+\end{proof}
 
-\begin{lemma}\label{naturals_smallest_inductive_set}
-    Let $A$ be an inductive set.
-    Then $\naturals\subseteq A$.
+\begin{lemma}\label{omega_is_a_limit_ordinal}
+    $\naturals$ is a limit ordinal.
 \end{lemma}
+\begin{proof}
+    $\emptyset\precedes \naturals$.
+    If $n\in \naturals$, then $\suc{n}\in\naturals$.
+\end{proof}
 
 
+\subsubsection{Properties and Facts natural numbers}
+
+\begin{theorem}\label{induction_principle}
+    Let $P$ be a set.
+    Suppose $P \subseteq \naturals$.
+    Suppose $\zero \in P$.
+    Suppose $\forall n \in P. \suc{n} \in P$.
+    Then $P = \naturals$.
+\end{theorem}
+\begin{proof}
+    Trivial.
+\end{proof}
+
+\begin{proposition}\label{existence_of_suc}
+    Let $n \in \naturals$.
+    Suppose $n \neq \zero$.
+    Then there exist $n' \in \naturals$ such that $\suc{n'} = n$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{transitiveset,nat_is_transitiveset,suc_intro_self,successor_ordinal,nat_is_successor_ordinal}.
+\end{proof}
+
+\begin{proposition}\label{suc_eq_plus_one}
+    Let $n \in \naturals$.
+    Then $\suc{n} = n + 1$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid n + 1 = 1 + n  \}$.
+    $\zero \in P$.
+    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
+\end{proof}
+
+\begin{proposition}\label{naturals_1_kommu}
+    Let $n \in \naturals$.
+    Then $1 + n = n + 1$.
+\end{proposition}
+
+\begin{proposition}\label{naturals_add_kommu}
+    For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$.
+\end{proposition}
+\begin{proof}
+    Fix $n \in \naturals$.
+    Let $P = \{ m \in \naturals \mid m + n = n + m \}$.
+    It suffices to show that $P = \naturals$.
+    $P \subseteq \naturals$.
+    $\zero \in P$.
+    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
+\end{proof}
+
+\begin{proposition}\label{naturals_add_assoc}
+    Suppose $n,m,k \in \naturals$.
+    Then $n + (m + k) = (n + m) + k$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ k \in \naturals \mid \text{for all $n',m' \in \naturals$ we have $n' + (m' + k) = (n' + m') + k$}\}$.
+    $P \subseteq \naturals$.
+    We show that $P = \naturals$.
+    \begin{subproof}
+        $\zero \in P$.
+        It suffices to show that for all $k \in P$ we have $\suc{k} \in P$.
+        Fix $k \in P$.
+        \begin{align*}
+            (n + m) + \suc{k} \\
+            &= \suc{(n+m) + k} \\
+            &= \suc{n + (m + k)} \\
+            &= n + \suc{(m + k)} \\
+            &= n + (m + \suc{k})
+        \end{align*}
+        For all $n,m \in \naturals$ we have $(n + m) + \suc{k} = n + (m + \suc{k})$.
+    \end{subproof}
+\end{proof}
+
+\begin{proposition}\label{naturals_rmul_one}
+    For all $n \in \naturals$ we have $n \rmul 1 = n$.
+\end{proposition}
+
+
+\begin{proposition}\label{naturals_mul_kommu}
+    Let $n, m \in \naturals$.
+    Then $n \rmul m = m \rmul n$.
+\end{proposition}
+
+\begin{proposition}\label{naturals_rmul_assoc}
+    Suppose $n,m,k \in \naturals$.
+    Then $n \rmul (m \rmul k) = (n \rmul m) \rmul k$.
+\end{proposition}
+
 \begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
     $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
 \end{lemma}
@@ -153,9 +261,6 @@
     Omitted.
 \end{proof}
 
-%\begin{lemma}\label{oeder_on_naturals}
-%    $\lt[\reals] \inter (\naturals \times \naturals)$ is an order on $\naturals$.
-%\end{lemma}
 
 
 
@@ -387,9 +492,9 @@
 
 
 
-%\begin{proposition}\label{safe}
-%    Contradiction.
-%\end{proposition}
+\begin{proposition}\label{safe}
+    Contradiction.
+\end{proposition}
 
 \section{The integers}
 
diff --git a/library/ordinal.tex b/library/ordinal.tex
index 3063162..6f924c1 100644
--- a/library/ordinal.tex
+++ b/library/ordinal.tex
@@ -3,7 +3,7 @@
 \import{set/powerset.tex}
 \import{set/regularity.tex}
 \import{set/suc.tex}
-\import{nat.tex}
+%\import{nat.tex}
 
 
 \section{Transitive sets}
@@ -584,55 +584,56 @@ Then $\alpha\subseteq\beta$.
     Follows by \cref{subseteq_antisymmetric}.
 \end{proof}
 
-
-\subsection{Natural numbers as ordinals}
-
-\begin{lemma}\label{nat_is_successor_ordinal}
-    Let $n\in\naturals$.
-    Suppose $n\neq \emptyset$.
-    Then $n$ is a successor ordinal.
-\end{lemma}
-\begin{proof}
-    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
-    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
-    Now $M\subseteq \naturals\subseteq M$
-        by \cref{subseteq,naturals_smallest_inductive_set}.
-    Thus $M = \naturals$.
-    Follows by \cref{subseteq}.
-\end{proof}
-
-\begin{lemma}\label{nat_is_transitiveset}
-    $\naturals$ is \in-transitive.
-\end{lemma}
-\begin{proof}
-    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
-    $\emptyset\in M$.
-    For all $n\in M$ we have $\suc{n}\in M$
-        by \cref{naturals_inductive_set,suc}.
-    Thus $M$ is an inductive set.
-    Now $M\subseteq \naturals\subseteq M$
-        by \cref{subseteq,naturals_smallest_inductive_set}.
-    Hence $\naturals = M$.
-\end{proof}
-
-\begin{lemma}\label{natural_number_is_ordinal}
-    Every natural number is an ordinal.
-\end{lemma}
-\begin{proof}
-    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
-\end{proof}
-
-\begin{lemma}\label{omega_is_an_ordinal}
-    $\naturals$ is an ordinal.
-\end{lemma}
-\begin{proof}
-    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
-\end{proof}
-
-\begin{lemma}\label{omega_is_a_limit_ordinal}
-    $\naturals$ is a limit ordinal.
-\end{lemma}
-\begin{proof}
-    $\emptyset\precedes \naturals$.
-    If $n\in \naturals$, then $\suc{n}\in\naturals$.
-\end{proof}
+%
+%\subsection{Natural numbers as ordinals}
+%
+%\begin{lemma}\label{nat_is_successor_ordinal}
+%    Let $n\in\naturals$.
+%    Suppose $n\neq \emptyset$.
+%    Then $n$ is a successor ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
+%    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
+%    Now $M\subseteq \naturals\subseteq M$
+%        by \cref{subseteq,naturals_smallest_inductive_set}.
+%    Thus $M = \naturals$.
+%    Follows by \cref{subseteq}.
+%\end{proof}
+%
+%\begin{lemma}\label{nat_is_transitiveset}
+%    $\naturals$ is \in-transitive.
+%\end{lemma}
+%\begin{proof}
+%    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
+%    $\emptyset\in M$.
+%    For all $n\in M$ we have $\suc{n}\in M$
+%        by \cref{naturals_inductive_set,suc}.
+%    Thus $M$ is an inductive set.
+%    Now $M\subseteq \naturals\subseteq M$
+%        by \cref{subseteq,naturals_smallest_inductive_set}.
+%    Hence $\naturals = M$.
+%\end{proof}
+%
+%\begin{lemma}\label{natural_number_is_ordinal}
+%    Every natural number is an ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
+%\end{proof}
+%
+%\begin{lemma}\label{omega_is_an_ordinal}
+%    $\naturals$ is an ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
+%\end{proof}
+%
+%\begin{lemma}\label{omega_is_a_limit_ordinal}
+%    $\naturals$ is a limit ordinal.
+%\end{lemma}
+%\begin{proof}
+%    $\emptyset\precedes \naturals$.
+%    If $n\in \naturals$, then $\suc{n}\in\naturals$.
+%\end{proof}
+%
\ No newline at end of file
-- 
cgit v1.2.3


From c580901e967c6bf0b012017a868a2c360e25370a Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Fri, 5 Jul 2024 10:42:24 +0200
Subject: Proof of 1 is identity on the naturals and begin of Disstributiv law
 naturals proof

---
 library/numbers.tex | 68 +++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 66 insertions(+), 2 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index b83827a..113aadb 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -102,7 +102,7 @@
 \end{axiom}
 
 \begin{axiom}\label{naturals_mul_axiom_1}
-    For all $n \in \naturals$ we have $n \rmul \zero = \zero$.
+    For all $n \in \naturals$ we have $n \rmul \zero = \zero = \zero \rmul n$.
 \end{axiom}
 
 \begin{axiom}\label{naturals_mul_axiom_2}
@@ -203,6 +203,9 @@
     Let $n \in \naturals$.
     Then $1 + n = n + 1$.
 \end{proposition}
+\begin{proof}
+    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}
     For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$.
@@ -240,14 +243,75 @@
 \end{proof}
 
 \begin{proposition}\label{naturals_rmul_one}
-    For all $n \in \naturals$ we have $n \rmul 1 = n$.
+    For all $n \in \naturals$ we have $1 \rmul n = n$.
 \end{proposition}
+\begin{proof}
+    Fix $n \in \naturals$.
+    \begin{align*}
+        1 \rmul n  \\
+        &= \suc{\zero} \rmul n \\
+        &= (\zero \rmul n) + n \\
+        &= (\zero) + n \\
+        &= n
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_add_remove_brakets}
+    Suppose $n,m,k \in \naturals$.
+    Then $(n + m) + k = n + m + k$.    
+\end{proposition}
+
+\begin{proposition}\label{natural_disstro}
+    Suppose $n,m,k \in \naturals$.
+    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$.
+    $\zero \in P$.
+    $P \subseteq \naturals$.
+    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+    Fix $n \in P$.
+    It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul (m + k) = (\suc{n} \rmul m) + (\suc{n} \rmul k)$.
+    Fix $m \in \naturals$.
+    It suffices to show that for all $k \in \naturals$ we have $\suc{n} \rmul (m + k) = (\suc{n} \rmul m) + (\suc{n} \rmul k)$.
+    Fix $k \in \naturals$.
+    \begin{align*}
+        \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}}\\
+        &= ((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_assoc}}\\
+        &= (\suc{n} \rmul m) + (\suc{n} \rmul k) \explanation{by \cref{naturals_mul_axiom_2}}
+    \end{align*}
+\end{proof}
 
 
 \begin{proposition}\label{naturals_mul_kommu}
     Let $n, m \in \naturals$.
     Then $n \rmul m = m \rmul n$.
 \end{proposition}
+\begin{proof}
+    Let $P = \{n \in \naturals \mid \forall m \in \naturals. n \rmul m = m \rmul n\}$.
+    $\zero \in P$.
+    $P \subseteq \naturals$.
+    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+    Fix $n \in P$.
+    It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul m = m \rmul \suc{n}$.
+    Fix $m \in \naturals$.
+    $n \rmul m = m \rmul n$.
+
+    \begin{align*}
+        \suc{n} \rmul m \\
+        &= (n \rmul m) + m \\
+        &= (m \rmul n) + m \\
+        &= m + (m \rmul n) \\
+        &= m \rmul \suc{n} \\
+    \end{align*}
+\end{proof}
 
 \begin{proposition}\label{naturals_rmul_assoc}
     Suppose $n,m,k \in \naturals$.
-- 
cgit v1.2.3


From 698bc0ec8128889aae37a766130e9b193c399b9c Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 6 Jul 2024 17:55:36 +0200
Subject: Finished the formalization of naturals.

---
 library/numbers.tex | 119 ++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 84 insertions(+), 35 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 113aadb..a185940 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -113,6 +113,14 @@
     If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number.
 \end{axiom}
 
+\begin{axiom}\label{naturals_rmul_is_closed_in_n}
+    For all $n,m \in \naturals$ we have $(n \rmul m) \in \naturals$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_add_is_closed_in_n}
+    For all $n,m \in \naturals$ we have $(n + m) \in \naturals$.
+\end{axiom}
+
 \subsubsection{Natural numbers as ordinals}
 
 
@@ -226,23 +234,22 @@
 \begin{proof}
     Let $P = \{ k \in \naturals \mid \text{for all $n',m' \in \naturals$ we have $n' + (m' + k) = (n' + m') + k$}\}$.
     $P \subseteq \naturals$.
-    We show that $P = \naturals$.
-    \begin{subproof}
-        $\zero \in P$.
-        It suffices to show that for all $k \in P$ we have $\suc{k} \in P$.
-        Fix $k \in P$.
-        \begin{align*}
-            (n + m) + \suc{k} \\
-            &= \suc{(n+m) + k} \\
-            &= \suc{n + (m + k)} \\
-            &= n + \suc{(m + k)} \\
-            &= n + (m + \suc{k})
-        \end{align*}
-        For all $n,m \in \naturals$ we have $(n + m) + \suc{k} = n + (m + \suc{k})$.
-    \end{subproof}
+    $\zero \in P$.
+    It suffices to show that for all $k \in P$ we have $\suc{k} \in P$.
+    Fix $k \in P$.
+    It suffices to show that for all $n' \in \naturals$ we have for all $m' \in \naturals$ we have $n' + (m' + \suc{k}) = (n' + m') + \suc{k}$.
+    Fix $n' \in \naturals$.
+    Fix $m' \in \naturals$.
+    \begin{align*}
+        (n' + m') + \suc{k}    \\
+        &= \suc{(n' + m') + k}   \\
+        &= \suc{n' + (m' + k)} \\
+        &= n' + \suc{(m' + k)} \\
+        &= n' + (m' + \suc{k})
+    \end{align*}
 \end{proof}
 
-\begin{proposition}\label{naturals_rmul_one}
+\begin{proposition}\label{naturals_rmul_one_left}
     For all $n \in \naturals$ we have $1 \rmul n = n$.
 \end{proposition}
 \begin{proof}
@@ -258,7 +265,12 @@
 
 \begin{proposition}\label{naturals_add_remove_brakets}
     Suppose $n,m,k \in \naturals$.
-    Then $(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}
+    Suppose $n,m,k,l \in \naturals$.
+    Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.    
 \end{proposition}
 
 \begin{proposition}\label{natural_disstro}
@@ -271,26 +283,43 @@
     $P \subseteq \naturals$.
     It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
     Fix $n \in P$.
-    It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul (m + k) = (\suc{n} \rmul m) + (\suc{n} \rmul k)$.
-    Fix $m \in \naturals$.
-    It suffices to show that for all $k \in \naturals$ we have $\suc{n} \rmul (m + k) = (\suc{n} \rmul m) + (\suc{n} \rmul k)$.
-    Fix $k \in \naturals$.
+
+    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+    Fix $m' \in \naturals$.
+    Fix $k' \in \naturals$.
+    $n \in \naturals$.
     \begin{align*}
-        \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}}\\
-        &= ((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_assoc}}\\
-        &= (\suc{n} \rmul m) + (\suc{n} \rmul k) \explanation{by \cref{naturals_mul_axiom_2}}
+        \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}}\\
+        &= ((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_assoc}}\\
+        &= (\suc{n} \rmul m') + (\suc{n} \rmul k')   %\explanation{by \cref{naturals_mul_axiom_2}}
     \end{align*}
 \end{proof}
 
+\begin{proposition}\label{naturals_rmul_one_kommu}
+    For all $n \in \naturals$ we have $n \rmul 1 = n$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid n \rmul 1 = n\}$.
+    $1 \in P$.
+    It suffices to show that for all $n' \in P$ we have $\suc{n'} \in P$.
+    Fix $n' \in P$.
+    It suffices to show that $\suc{n'} \rmul 1 = \suc{n'}$.
+    \begin{align*}
+        \suc{n'} \rmul 1 \\
+        &=  n' \rmul 1 + 1 \\
+        &=  n' + 1 \\
+        &= \suc{n'}
+    \end{align*}
+\end{proof}
 
-\begin{proposition}\label{naturals_mul_kommu}
+\begin{proposition}\label{naturals_rmul_kommu}
     Let $n, m \in \naturals$.
     Then $n \rmul m = m \rmul n$.
 \end{proposition}
@@ -303,12 +332,13 @@
     It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul m = m \rmul \suc{n}$.
     Fix $m \in \naturals$.
     $n \rmul m = m \rmul n$.
-
     \begin{align*}
         \suc{n} \rmul m \\
         &= (n \rmul m) + m \\
         &= (m \rmul n) + m \\
         &= m + (m \rmul n) \\
+        &= (m \rmul 1) + (m \rmul n) \\
+        &= m \rmul (1 + n) \\
         &= m \rmul \suc{n} \\
     \end{align*}
 \end{proof}
@@ -317,13 +347,32 @@
     Suppose $n,m,k \in \naturals$.
     Then $n \rmul (m \rmul k) = (n \rmul m) \rmul k$.
 \end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m \rmul k) = (n \rmul m) \rmul k$ }\}$.
+    $\zero \in P$.
+    It suffices to show that for all $n' \in P$ we have $ \suc{n'} \in P$.
+    Fix $n' \in P$.
+    It suffices to show that for all $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n'} \rmul (m' \rmul k') = (\suc{n'} \rmul m') \rmul k'$.
+    Fix $m' \in \naturals$.
+    Fix $k' \in \naturals$.
+    \begin{align*}
+        \suc{n'} \rmul (m' \rmul k')                \\
+        &=(n' \rmul (m' \rmul k')) + (m' \rmul k')  \\
+        &=((n' \rmul m') \rmul k') + (m' \rmul k')  \\
+        &=(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'              
+    \end{align*}
+\end{proof}
 
 \begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
     $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
 \end{lemma}
-\begin{proof}
-    Omitted.
-\end{proof}
+
+
+
+
 
 
 
-- 
cgit v1.2.3


From b71f135d5762f2a12bf08c71ecdcd221ed87cff0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 6 Jul 2024 19:22:03 +0200
Subject: Formalisation of integers.

---
 library/numbers.tex      | 123 ++++++++++++++++++++++++++++++++++++++---------
 source/Syntax/Lexicon.hs |   1 +
 2 files changed, 101 insertions(+), 23 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index a185940..08cbc70 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -371,19 +371,18 @@
 \end{lemma}
 
 
+\subsection{Axioms of the reals Part One}
+We seen before that we can proof the common behavior of the naturals.
+Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals.
+Such that we can introduce the integers and raitionals as smooth as possible.
 
+\begin{axiom}\label{reals_rmul}
+    For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$.
+\end{axiom}
 
-
-
-
-
-
-
-
-\subsection{The Intergers}
-
-
-
+\begin{axiom}\label{reals_add}
+    For all $n,m \in \reals$ we have $(n + m) \in \reals$.
+\end{axiom}
 
 \begin{axiom}\label{reals_axiom_dense}
     For all $x,y \in \reals$ if $x < y$ then 
@@ -423,20 +422,104 @@
     such that $x < z < y$.
 \end{axiom}
 
-\begin{proposition}\label{reals_disstro2}
+\begin{axiom}\label{reals_disstro2}
     For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
-\end{proposition}
+\end{axiom}
+
+
+\begin{axiom}\label{reals_reducion_on_addition}
+    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
+\end{axiom}
+
+
+
+
+
+
+
+\subsection{The Intergers}
+
+
+\begin{axiom}\label{neg}
+    For all $n \in \reals$ we have $\neg{n} \in \reals$ and $n + \neg{n} = \zero$.
+\end{axiom}
+
+\begin{axiom}\label{neg_of_zero}
+    $\neg{\zero} = \zero$.
+\end{axiom}
+
+\begin{definition}\label{minus}
+    $n - m = n + \neg{m}$.
+\end{definition}
+
+\begin{lemma}\label{minus_in_reals}
+    Suppose $n,m \in \reals$.
+    Then $n - m \in \reals$.
+\end{lemma}
 \begin{proof}
-    Omitted.
+    \begin{byCase}
+        \caseOf{$m = \zero$.} Trivial.%Follows by \cref{neg_of_zero,minus,neg,reals_add}.
+        \caseOf{$m \neq \zero$.} Trivial.% Follows by \cref{neg_of_zero,minus,neg,reals_add}.
+    \end{byCase}
 \end{proof}
 
-\begin{proposition}\label{reals_reducion_on_addition}
-    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
+\begin{proposition}\label{negation_of_negation_is_id}
+    For all $r \in \reals$ we have $\neg{\neg{r}} = r$.
 \end{proposition}
 \begin{proof}
-    Omitted.
+    Fix $r \in \reals$.
+    $r + \neg{r} = \zero$.
+    $\neg{r} + \neg{\neg{r}} = \zero$.
+    Follows by \cref{reals_reducion_on_addition,neg,reals_axiom_kommu}.
 \end{proof}
 
+\begin{definition}\label{integers}
+    $\integers = \{ z \in \reals \mid \exists n \in \naturals. z \in \naturals \lor  n + z = \zero\}$.
+\end{definition}
+
+\begin{lemma}\label{n_subset_z}
+    $\naturals \subseteq \integers$.
+\end{lemma}
+
+\begin{lemma}\label{neg_of_naturals_in_integers}
+    For all $n \in \naturals$ we have $\neg{n} \in \integers$.
+\end{lemma}
+
+\begin{lemma}\label{integers_eq_naturals_and_negativ_naturals}
+    $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
+\end{lemma}
+\begin{proof}
+    Let $P = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
+    \begin{byCase}
+        \caseOf{$\integers \subseteq P$.} Trivial.
+        \caseOf{$P \subseteq \integers$.} Trivial.
+    \end{byCase}
+\end{proof}
+
+
+
+
+\subsection{The Rationals}
+
+%\begin{definition}
+%    $\inv{x} 
+%\end{definition}
+%
+%\begin{axiom}
+%    For all $x,y \in \reals$ we have $\rfrac{x}{y} \in \reals$.
+%\end{axiom}
+%
+%\begin{definition}
+%    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \integers. q = \rfrac{z}{n} \}$.
+%\end{definition}
+
+
+
+
+
+
+
+
 
 %\begin{signature}\label{invers_is_set}
 %    $\addInv{y}$ is a set.
@@ -608,9 +691,3 @@
 \begin{proposition}\label{safe}
     Contradiction.
 \end{proposition}
-
-\section{The integers}
-
-%\begin{definition}
-%    $\integers = \{z \in \reals \mid z = \zero or \} $.
-%\end{definition}
\ No newline at end of file
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index 463dd18..65072ee 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>)
         builtinIdentifiers = identifier <$>
             [ "emptyset"
             , "naturals"
+            , "integers"
             , "rationals"
             , "reals"
             , "unit"
-- 
cgit v1.2.3


From 36e03142465e482f2b5506cd35dab5ef9cc9fd66 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 6 Jul 2024 19:53:50 +0200
Subject: Formalisation of rationals.

---
 library/numbers.tex      | 66 +++++++++++++++++++++++++-----------------------
 source/Syntax/Lexicon.hs |  1 +
 2 files changed, 35 insertions(+), 32 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 08cbc70..4ccba67 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -431,7 +431,14 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{axiom}
 
+\begin{axiom}\label{zero_less_one}
+    $\zero < 1$.
+\end{axiom}
 
+\begin{axiom}\label{reals_axiom_order_def}
+    Suppose $x,y,z,w \in \reals$.
+    If $x + y < z + w$ then $x < z \lor y < w$.
+\end{axiom}
 
 
 
@@ -501,42 +508,37 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 \subsection{The Rationals}
 
-%\begin{definition}
-%    $\inv{x} 
-%\end{definition}
-%
-%\begin{axiom}
-%    For all $x,y \in \reals$ we have $\rfrac{x}{y} \in \reals$.
-%\end{axiom}
-%
-%\begin{definition}
-%    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \integers. q = \rfrac{z}{n} \}$.
-%\end{definition}
-
-
-
-
+\begin{axiom}\label{invers_reals}
+    For all $q \in \reals$ we have $\inv{q} \rmul q = 1$.
+\end{axiom}
 
+\begin{abbreviation}\label{rfrac}
+    $\rfrac{x}{y} = x \rmul \inv{y}$.
+\end{abbreviation}
 
+\begin{abbreviation}\label{naturalsplus}
+    $\naturalsPlus = \naturals \setminus \{\zero\}$.
+\end{abbreviation}
 
+\begin{definition}\label{rationals}
+    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
+\end{definition}
 
 
-%\begin{signature}\label{invers_is_set}
-%    $\addInv{y}$ is a set.
-%\end{signature}
 
-%\begin{definition}\label{add_inverse}
-%    $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$.
-%\end{definition}
-    
+\subsection{Order on the reals}
 
-%\begin{definition}\label{add_inverse_natural_language}
-%    $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. 
-%\end{definition}
+\begin{lemma}\label{plus_one_order}
+    For all $r\in \reals$ we have $ r < r + 1$.
+\end{lemma}
+\begin{proof}
+    %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}.
+\end{proof}
 
-%\begin{lemma}\label{rminus}
-%    $x \rminus \addInv{x} = \zero$.
-%\end{lemma}
+\begin{lemma}\label{negation_and_order}
+    Suppose $r \in \reals$.
+    $r \leq \zero$ iff $\zero \leq \neg{r}$.
+\end{lemma}
 
 
 
@@ -546,7 +548,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     Then $x + y$ is positiv.
 \end{lemma}
 \begin{proof}
-    Omitted.
+    
 \end{proof}
 
 \begin{lemma}\label{reals_mul_of_positiv}
@@ -688,6 +690,6 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 
 
-\begin{proposition}\label{safe}
-    Contradiction.
-\end{proposition}
+%\begin{proposition}\label{safe}
+%    Contradiction.
+%\end{proposition}
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index 65072ee..de6d966 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -111,6 +111,7 @@ prefixOps =
     , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd"))
     , ([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"))
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
-- 
cgit v1.2.3


From cbac8ca4a5bf8ff38af3e512956ea1e468965194 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 21 Jul 2024 12:26:20 +0200
Subject: Further Formalisation on numbers

---
 latex/naproche.sty     |   1 +
 library/everything.tex |   2 +-
 library/numbers.tex    | 165 ++++++++++++++++++++++++++++++++-----------------
 3 files changed, 110 insertions(+), 58 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 476d3dd..7ef2359 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -132,6 +132,7 @@
 \newcommand{\integers}{\mathcal{Z}}
 \newcommand{\zero}{0}
 \newcommand{\one}{1}
+\newcommand{\rmul}{\cdot}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/library/everything.tex b/library/everything.tex
index 29b97b7..b966197 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -29,7 +29,7 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
-%\import{numbers.tex}
+\import{numbers.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/numbers.tex b/library/numbers.tex
index 4ccba67..0bfae2d 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -18,34 +18,6 @@
     $x \rmul y$ is a set.
 \end{signature}
 
-\begin{axiom}\label{reals_axiom_order}
-    $\lt[\reals]$ is an order on $\reals$.
-\end{axiom}
-
-\begin{abbreviation}\label{lesseq_on_reals}
-    $x \leq y$ iff $(x,y) \in \lt[\reals]$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{less_on_reals}
-    $x < y$ iff it is wrong that $y \leq x$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{greater_on_reals}
-    $x > y$ iff $y \leq x$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{greatereq_on_reals}
-    $x \geq y$ iff it is wrong that $x < y$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{is_positiv}
-    $x$ is positiv iff $x > \zero$.
-\end{abbreviation}
-
-
-%Structure TODO:
-% Take as may axioms as needed  - Tarski Axioms of reals
-%Implement Naturals -> Integer -> rationals -> reals 
 
 
 \subsection{Creation of natural numbers}
@@ -384,14 +356,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $n,m \in \reals$ we have $(n + m) \in \reals$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_dense}
-    For all $x,y \in \reals$ if $x < y$ then 
-    there exist $z \in \reals$ such that $x < z$ and $z < y$.
-\end{axiom}
 
-\begin{axiom}\label{reals_axiom_assoc}
-    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
-\end{axiom}
 
 \begin{axiom}\label{reals_axiom_kommu}
     For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$.
@@ -417,31 +382,72 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_dedekind_complete}
-    For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
-    such that $x < z < y$.
-\end{axiom}
-
 \begin{axiom}\label{reals_disstro2}
     For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
 \end{axiom}
 
-
 \begin{axiom}\label{reals_reducion_on_addition}
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{axiom}
 
-\begin{axiom}\label{zero_less_one}
-    $\zero < 1$.
+\begin{abbreviation}\label{rless}
+    $x < y$ iff $x \rless y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{less_on_reals}
+    $x \leq y$ iff it is wrong that $y < x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y \leq x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff it is wrong that $x < y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{is_positiv}
+    $x$ is positiv iff $x > \zero$.
+\end{abbreviation}
+
+
+
+
+
+\begin{axiom}\label{tarski1}
+    For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$.
+\end{axiom}
+
+\begin{axiom}\label{tarski2}
+    For all $x,y \in \reals$ if $x < y$ then 
+    there exist $z \in \reals$ such that $x < z$ and $z < y$.
+\end{axiom}
+
+\begin{axiom}\label{tarski3}
+    For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
+    such that $x < z < y$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_order_def}
-    Suppose $x,y,z,w \in \reals$.
-    If $x + y < z + w$ then $x < z \lor y < w$.
+\begin{axiom}\label{tarski4}
+    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
+\end{axiom}
+
+\begin{axiom}\label{tarski5}
+    For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$.
 \end{axiom}
 
 
+\begin{axiom}\label{tarski8}
+    $\zero < 1$.
+\end{axiom}
+
+\begin{axiom}\label{labelordersossss}
+    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
+\end{axiom}
 
+\begin{axiom}\label{nocheinschoeneslabel}
+    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
+\end{axiom}
 
 
 \subsection{The Intergers}
@@ -465,8 +471,8 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 \end{lemma}
 \begin{proof}
     \begin{byCase}
-        \caseOf{$m = \zero$.} Trivial.%Follows by \cref{neg_of_zero,minus,neg,reals_add}.
-        \caseOf{$m \neq \zero$.} Trivial.% Follows by \cref{neg_of_zero,minus,neg,reals_add}.
+        \caseOf{$m = \zero$.} Trivial.
+        \caseOf{$m \neq \zero$.} Trivial.
     \end{byCase}
 \end{proof}
 
@@ -496,16 +502,31 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
 \end{lemma}
 \begin{proof}
-    Let $P = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
-    \begin{byCase}
-        \caseOf{$\integers \subseteq P$.} Trivial.
-        \caseOf{$P \subseteq \integers$.} Trivial.
-    \end{byCase}
+    Omitted.
 \end{proof}
 
+\begin{abbreviation}\label{positiv_real_number}
+    $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$.
+\end{abbreviation}
 
 
 
+\begin{proposition}\label{integers_negativ_times_negativ_is_positiv}
+    Suppose $n,m \in \integers$.
+    Suppose $n < \zero$ and $m < \zero$.
+    Then $n \rmul m > \zero$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+    %$n \neq \zero$ and $m \neq \zero$.
+    %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$.
+    %There exists $n' \in \reals$ such that $n' + n = \zero$.
+    %There exists $m' \in \reals$ such that $m' + m = \zero$.
+\end{proof}
+
+%TODO: negativ * negativ = positiv.
+
+
 \subsection{The Rationals}
 
 \begin{axiom}\label{invers_reals}
@@ -520,26 +541,56 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $\naturalsPlus = \naturals \setminus \{\zero\}$.
 \end{abbreviation}
 
-\begin{definition}\label{rationals}
+\begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen
     $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
 \end{definition}
 
+\begin{abbreviation}\label{nominator}
+    $z$ is nominator of $q$ iff there exists $n \in \naturalsPlus$ such that $q = \rfrac{z}{n}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{denominator}
+    $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$.
+\end{abbreviation}
+
+%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal}
+%    Suppose $p,q \in \rationals$.
+%    Suppose $z \in \naturals$.
+%    Suppose $p$ is positiv.
+%    Suppose $q$ is positiv.
+%    Suppose $z$ is nominator of $p$.
+%    Suppose $z$ is nominator of $p$.
+%    Suppose $p'$ is denominator of $p$.
+%    Suppose $q'$ is denominator of $q$.
+%    Then $p \leq q$ iff $p' \geq q'$.
+%\end{proposition}
+
+
+%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
+%    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
+%\end{theorem}
+
+% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, 
 
 
 \subsection{Order on the reals}
 
+
+
 \begin{lemma}\label{plus_one_order}
     For all $r\in \reals$ we have $ r < r + 1$.
 \end{lemma}
 \begin{proof}
-    %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}.
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{negation_and_order}
     Suppose $r \in \reals$.
     $r \leq \zero$ iff $\zero \leq \neg{r}$.
 \end{lemma}
-
+\begin{proof}
+    Omitted.
+\end{proof}
 
 
 \begin{lemma}\label{reals_add_of_positiv}
@@ -548,7 +599,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     Then $x + y$ is positiv.
 \end{lemma}
 \begin{proof}
-    
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{reals_mul_of_positiv}
-- 
cgit v1.2.3


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/numbers.tex             | 131 ++++++++++---------
 library/topology/continuous.tex |  14 +-
 library/topology/urysohn.tex    | 274 ++++++++++++++++++++++++++++++++++++++++
 source/Api.hs                   |  17 +++
 source/CommandLine.hs           |  60 ++++++---
 source/Provers.hs               |   4 +-
 source/Test/Golden.hs           |   1 +
 7 files changed, 422 insertions(+), 79 deletions(-)
 create mode 100644 library/topology/urysohn.tex

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 0bfae2d..7d1b058 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -348,6 +348,9 @@ We seen before that we can proof the common behavior of the naturals.
 Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals.
 Such that we can introduce the integers and raitionals as smooth as possible.
 
+
+
+The operations Multiplication and addition is closed in the reals
 \begin{axiom}\label{reals_rmul}
     For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$.
 \end{axiom}
@@ -358,10 +361,16 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 
 
+
+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}
   
+
+
+
+Existence of  one and Zero
 \begin{axiom}\label{reals_axiom_zero}
     For all $x \in \reals$ $x + \zero = x$. 
 \end{axiom}
@@ -370,6 +379,9 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x \in \reals$ we have $x \rmul 1 = x$.
 \end{axiom}
 
+
+
+The Existence of Inverse of both operations
 \begin{axiom}\label{reals_axiom_add_invers}
     For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$.
 \end{axiom}
@@ -378,6 +390,9 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$.
 \end{axiom}
 
+
+
+Disstrubitiv Laws of the reals
 \begin{axiom}\label{reals_axiom_disstro1}
     For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$.
 \end{axiom}
@@ -386,10 +401,9 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
 \end{axiom}
 
-\begin{axiom}\label{reals_reducion_on_addition}
-    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
-\end{axiom}
 
+
+Definition of the order symbols
 \begin{abbreviation}\label{rless}
     $x < y$ iff $x \rless y$.
 \end{abbreviation}
@@ -406,50 +420,50 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $x \geq y$ iff it is wrong that $x < y$.
 \end{abbreviation}
 
+
+
+Laws of the order on the reals
 \begin{abbreviation}\label{is_positiv}
     $x$ is positiv iff $x > \zero$.
 \end{abbreviation}
 
-
-
-
-
-\begin{axiom}\label{tarski1}
+\begin{axiom}\label{reals_order}
     For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$.
 \end{axiom}
 
-\begin{axiom}\label{tarski2}
+\begin{axiom}\label{reals_dense}
     For all $x,y \in \reals$ if $x < y$ then 
     there exist $z \in \reals$ such that $x < z$ and $z < y$.
 \end{axiom}
 
-\begin{axiom}\label{tarski3}
+\begin{axiom}\label{reals_is_eta_zero_set}
     For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
     such that $x < z < y$.
 \end{axiom}
 
-\begin{axiom}\label{tarski4}
-    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
+\begin{axiom}\label{reals_one_bigger_zero}
+    $\zero < 1$.
 \end{axiom}
 
-\begin{axiom}\label{tarski5}
-    For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$.
+\begin{axiom}\label{reals_order_behavior_with_addition}
+    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
 \end{axiom}
 
-
-\begin{axiom}\label{tarski8}
-    $\zero < 1$.
+\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)$. 
 \end{axiom}
 
-\begin{axiom}\label{labelordersossss}
-    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
+\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$. 
 \end{axiom}
 
-\begin{axiom}\label{nocheinschoeneslabel}
-    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
+\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)$. 
 \end{axiom}
 
 
+
+
 \subsection{The Intergers}
 
 
@@ -480,10 +494,11 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $r \in \reals$ we have $\neg{\neg{r}} = r$.
 \end{proposition}
 \begin{proof}
-    Fix $r \in \reals$.
-    $r + \neg{r} = \zero$.
-    $\neg{r} + \neg{\neg{r}} = \zero$.
-    Follows by \cref{reals_reducion_on_addition,neg,reals_axiom_kommu}.
+    Omitted.
+%    Fix $r \in \reals$.
+%    $r + \neg{r} = \zero$.
+%    $\neg{r} + \neg{\neg{r}} = \zero$.
+%    Follows by \cref{neg,reals_axiom_kommu}.
 \end{proof}
 
 \begin{definition}\label{integers}
@@ -511,22 +526,6 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 
 
-\begin{proposition}\label{integers_negativ_times_negativ_is_positiv}
-    Suppose $n,m \in \integers$.
-    Suppose $n < \zero$ and $m < \zero$.
-    Then $n \rmul m > \zero$.
-\end{proposition}
-\begin{proof}
-    Omitted.
-    %$n \neq \zero$ and $m \neq \zero$.
-    %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$.
-    %There exists $n' \in \reals$ such that $n' + n = \zero$.
-    %There exists $m' \in \reals$ such that $m' + m = \zero$.
-\end{proof}
-
-%TODO: negativ * negativ = positiv.
-
-
 \subsection{The Rationals}
 
 \begin{axiom}\label{invers_reals}
@@ -542,7 +541,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 \end{abbreviation}
 
 \begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen
-    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
+    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in (\integers \setminus \{\zero\}). q = \rfrac{z}{n} \}$.
 \end{definition}
 
 \begin{abbreviation}\label{nominator}
@@ -553,23 +552,41 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$.
 \end{abbreviation}
 
-%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal}
-%    Suppose $p,q \in \rationals$.
-%    Suppose $z \in \naturals$.
-%    Suppose $p$ is positiv.
-%    Suppose $q$ is positiv.
-%    Suppose $z$ is nominator of $p$.
-%    Suppose $z$ is nominator of $p$.
-%    Suppose $p'$ is denominator of $p$.
-%    Suppose $q'$ is denominator of $q$.
-%    Then $p \leq q$ iff $p' \geq q'$.
-%\end{proposition}
+\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
+    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{lemma}\label{fraction_kuerzung} %TODO: Englischen namen rausfinden
+    For all $n,m,k \in \reals$ we have $\rfrac{n \rmul k}{m \rmul k} = \rfrac{n}{m}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
-%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
-%    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
-%\end{theorem}
+\begin{lemma}\label{fraction_swap}
+    For all $n,m,k,l \in \reals$ we have $\rfrac{\rfrac{n}{m}}{\rfrac{k}{l}}=\rfrac{n \rmul l}{m \rmul k}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{definition}\label{divisor}
+    $g$ is a integral divisor of $a$ iff $g \in \naturals$ and there exist $b \in \integers$ such that $g \rmul b = a$.
+\end{definition}
+
+
+
+
+%\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$ 
+%    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, 
 
 
@@ -652,7 +669,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 \begin{lemma}\label{order_reals_lemma3}
     Let $x,y,z \in \reals$.
-    Suppose $\zero < x$. 
+    Suppose $\zero > x$. 
     Suppose $y < z$. 
     Then $(x \rmul z) < (x \rmul y)$.
 \end{lemma}
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index 6a32353..a9bc58e 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -1,5 +1,7 @@
 \import{topology/topological-space.tex}
 \import{relation.tex}
+\import{function.tex}
+\import{set.tex}
 
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
@@ -8,18 +10,25 @@
 \begin{proposition}\label{continuous_definition_by_closeds}
     Let $X$ be a topological space.
     Let $Y$ be a topological space.
+    Let $f \in \funs{X}{Y}$.
     Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
 \end{proposition}
 \begin{proof}
     Omitted.
-    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
+    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ we have $\preimg{f}{U} \in \closeds{X}$.
     %\begin{subproof}
     %    Suppose $f$ is continuous.
     %    Fix $U \in \closeds{Y}$.
     %    $\carrier[Y] \setminus U$ is open in $Y$.
     %    Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$.
     %    Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$.
-    %    $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    \begin{subproof}
+    %        It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$.
+    %        Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
+    %        Take $y \in \carrier[Y]$ such that $f(x)=y$.
+    %        It suffices to show that $y \in U$.
+    %    \end{subproof}
     %    $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
     %\end{subproof}
     %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous.
@@ -27,3 +36,4 @@
     %    Omitted.
     %\end{subproof}
 \end{proof}
+
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}
diff --git a/source/Api.hs b/source/Api.hs
index 95d5c8c..f597153 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -17,6 +17,7 @@ module Api
     , dumpTask
     , verify, ProverAnswer(..), VerificationResult(..)
     , exportMegalodon
+    , showFailedTask
     , WithCache(..)
     , WithFilter(..)
     , WithOmissions(..)
@@ -29,6 +30,7 @@ module Api
     , WithParseOnly(..)
     , Options(..)
     , WithDumpPremselTraining(..)
+    , WithFailList(..)
     ) where
 
 
@@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token)
 import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment
+import Syntax.Abstract (Formula)
 
 -- | Follow all @\\import@ statements recursively and build a theory graph from them.
 -- The @\\import@ statements should be on their own separate line and precede all
@@ -285,6 +288,17 @@ exportMegalodon file = do
     pure (Megalodon.encodeBlocks lexicon blocks)
 
 
+
+-- | 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 (_, _) = Text.putStrLn "Error!"
+
+
 -- | Should we use caching?
 data WithCache = WithoutCache | WithCache deriving (Show, Eq)
 
@@ -312,6 +326,8 @@ pattern WithoutDump = WithDump ""
 
 data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq)
 
+data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq)
+
 
 data Options = Options
     { inputPath :: FilePath
@@ -327,4 +343,5 @@ data Options = Options
     , withVersion :: WithVersion
     , withMegalodon :: WithMegalodon
     , withDumpPremselTraining :: WithDumpPremselTraining
+    , withFailList :: WithFailList
     }
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index a9fb00d..47efe22 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -18,7 +18,7 @@ import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment (lookupEnv)
 import System.FilePath.Posix
-
+import qualified Tptp.UnsortedFirstOrder as Syntax.Internal
 
 runCommandLine :: IO ()
 runCommandLine = do
@@ -69,23 +69,42 @@ run = do
                     WithDefaultProver -> Provers.vampire vampirePathPath
             let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts)
             result <- verify proverInstance (inputPath opts)
-            liftIO case result of
-                VerificationSuccess -> (Text.putStrLn "Verification successful.")
-                VerificationFailure [] -> error "Empty verification fail"
-                VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
-                    Yes ->
-                        skip
-                    No tptp -> do
-                        putStrLn "Verification failed: prover found countermodel"
-                        Text.hPutStrLn stderr tptp
-                    ContradictoryAxioms tptp -> do
-                        putStrLn "Verification failed: contradictory axioms"
-                        Text.hPutStrLn stderr tptp
-                    Uncertain tptp -> do
-                        putStrLn "Verification failed: out of resources"
-                        Text.hPutStrLn stderr tptp
-                    Error err ->
-                        Text.hPutStrLn stderr err
+            case withFailList opts of
+                WithoutFailList -> liftIO case result of
+                    VerificationSuccess -> putStrLn "Verification successful."
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
+                        Yes ->
+                            skip
+                        No tptp -> do
+                            putStrLn "Verification failed: prover found countermodel"
+                            Text.hPutStrLn stderr tptp
+                        ContradictoryAxioms tptp -> do
+                            putStrLn "Verification failed: contradictory axioms"
+                            Text.hPutStrLn stderr tptp
+                        Uncertain tptp -> do
+                            putStrLn "Verification failed: out of resources"
+                            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."
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure fails -> do
+                        putStrLn "Following task couldn't be solved by the ATP: "
+                        traverse_ showFailedTask fails
+                        Text.hPutStrLn stderr "Don't give up!"
+
+
+
+
+
+
+
 
 
 
@@ -104,6 +123,7 @@ parseOptions = do
     withVersion <- withVersionParser
     withMegalodon <- withMegalodonParser
     withDumpPremselTraining <- withDumpPremselTrainingParser
+    withFailList <- withFailListParser
     pure Options{..}
 
 withTimeLimitParser :: Parser Provers.TimeLimit
@@ -160,3 +180,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump
 withMegalodonParser :: Parser WithMegalodon
 withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.")
     <|> pure WithoutMegalodon -- Default to using the cache.
+
+withFailListParser :: Parser WithFailList
+withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.")
+    <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file
diff --git a/source/Provers.hs b/source/Provers.hs
index 203ee82..37e02ca 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -110,7 +110,7 @@ data ProverAnswer
     | No Text
     | ContradictoryAxioms Text
     | Uncertain Text
-    | Error Text
+    | Error Text Text Text
     deriving (Show, Eq)
 
 nominalDiffTimeToText :: NominalDiffTime -> Text
@@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr =
         | saidNo -> No tptp
         | doesNotKnow -> Uncertain tptp
         | warned -> ContradictoryAxioms tptp
-        | otherwise -> Error (answer <> answerErr)
+        | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task)))
diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs
index 705aaa5..c01c249 100644
--- a/source/Test/Golden.hs
+++ b/source/Test/Golden.hs
@@ -39,6 +39,7 @@ testOptions = Api.Options
     , withTimeLimit = Provers.defaultTimeLimit
     , withVersion = Api.WithoutVersion
     , withMegalodon = Api.WithoutMegalodon
+    , withFailList = Api.WithoutFailList
     }
 
 goldenTests :: IO TestTree
-- 
cgit v1.2.3


From 951dd2b195524cb2d8f125abaa4936abaf5ae582 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Fri, 9 Aug 2024 15:33:30 +0200
Subject: fixed axiomatic error

---
 library/numbers.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 7d1b058..f7f6c2c 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -409,15 +409,15 @@ Definition of the order symbols
 \end{abbreviation}
 
 \begin{abbreviation}\label{less_on_reals}
-    $x \leq y$ iff it is wrong that $y < x$.
+    $x \leq y$ iff $x < y \lor x = y$.
 \end{abbreviation}
 
 \begin{abbreviation}\label{greater_on_reals}
-    $x > y$ iff $y \leq x$.
+    $x > y$ iff $y < x$.
 \end{abbreviation}
 
 \begin{abbreviation}\label{greatereq_on_reals}
-    $x \geq y$ iff it is wrong that $x < y$.
+    $x \geq y$ iff $y \leq x$.
 \end{abbreviation}
 
 
-- 
cgit v1.2.3


From 68716d1ab46dee3dfc1b03089f941dbb6883cdcd Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 4 Sep 2024 15:17:50 +0200
Subject: Mismatched Assume in Induction

Unexpeced Mismatch in line 99 and 109  or the pair
100 and 108. Parsing works with line 99 and 108 or with
the lines 100 and 109.

zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateNoun (SgPl {sg = [Just (Word "natural"),Just (Word "number")], pl = [Just (Word "natural"),Just (Word "numbers")]}))) [TermVar (NamedVar "n")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "n"),TermSymbol (SymbolMixfix [Just (Command "naturals")]) []]) (TermSymbol (SymbolPredicate (PredicateVerb (SgPl {sg = [Just (Word "has"),Just (Word "cardinality"),Nothing], pl = [Just (Word "ha"),Just (Word "cardinality"),Nothing]}))) [TermSymbol (SymbolMixfix [Just (Command "seq"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [],TermVar (NamedVar "n")],TermSymbol (SymbolMixfix [Just (Command "suc"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "n")]]))
---
 library/numbers.tex                         |  40 +++++++++++
 library/topology/real-topological-space.tex |  26 +++++++
 library/topology/urysohn2.tex               | 108 +++++++++++++++-------------
 3 files changed, 125 insertions(+), 49 deletions(-)
 create mode 100644 library/topology/real-topological-space.tex

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index f7f6c2c..cb3d5cf 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -747,9 +747,49 @@ Laws of the order on the reals
     $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
 \end{definition}
 
+\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{m_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\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}
 
 
 
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
new file mode 100644
index 0000000..239965c
--- /dev/null
+++ b/library/topology/real-topological-space.tex
@@ -0,0 +1,26 @@
+\import{set.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+
+
+\section{The canonical topology on $\mathbbR$}
+
+\begin{definition}\label{topological_basis_reals_eps_ball}
+    $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
+\end{definition}
+
+\begin{theorem}\label{reals_as_topo_space}
+    Suppose $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
+    Then $\reals$ is a topological space.
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
\ No newline at end of file
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index dbcfc53..a3f3ea4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -12,32 +12,11 @@
 \import{set/powerset.tex}
 \import{set/fixpoint.tex}
 \import{set/product.tex}
+\import{topology/real-topological-space.tex}
 
 \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{definition}\label{sequence}
@@ -89,26 +68,6 @@
 \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}
@@ -120,10 +79,61 @@
     Then $X$ is a sequence.
 \end{proposition}
 
-\begin{definition}\label{higher_urysohn_chain}
+\begin{definition}\label{lifted_urysohn_chain}
     $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
 \end{definition}
 
+\begin{definition}\label{normal_ordered_urysohnchain}
+    $U$ is normal ordered iff there exist $n \in \naturals$ such that $\dom{U} = \seq{\zero}{n}$.
+\end{definition}
+
+\begin{definition}\label{bijection_of_urysohnchains}
+    $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{proposition}\label{naturals_in_transitive}
+    $\naturals$ is a \in-transitive set.
+\end{proposition}
+
+\begin{proposition}\label{naturals_elem_in_transitive}
+    If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+    %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+    
+\end{proposition}
+
+\begin{proposition}\label{seq_zero_to_n_isomorph_to_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+\end{proposition}
+\begin{proof} [Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    %Assume $n$ is a natural number.
+    %We show that $\seq{\zero}{\zero}$ has cardinality $1$.
+    %\begin{subproof}
+    %    It suffices to show that $1 = \seq{\zero}{\zero}$.
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$.
+    %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$.
+    %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+\end{proof}
+
+\begin{proposition}\label{existence_normal_ordered_urysohn}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $\dom{U}$ is finite.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered.
+\end{proposition}
+\begin{proof}
+    Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}.
+    There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$.
+
+
+\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}
@@ -136,9 +146,6 @@
 
 
 
-
-
-
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -159,9 +166,9 @@
     There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
 \end{theorem}
 \begin{proof}
-    $U_0$ is a urysohnchain of $X$.
-    It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
-    
+    %$U_0$ is a urysohnchain of $X$.
+    %It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
+    Omitted.
 \end{proof}
 
 
@@ -246,6 +253,9 @@
     \begin{subproof}
         Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}.
     \end{subproof}
+    Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
+
+
 
 
 
-- 
cgit v1.2.3


From b298295ac002785672a8b16dd09f9692d73f7a80 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 15 Sep 2024 15:07:36 +0200
Subject: Issue at Fixing.

In Line 49 in real-topological-space.tex the Fix can't be processed.
---
 library/numbers.tex                         | 19 ++++++++
 library/topology/metric-space.tex           |  2 +-
 library/topology/real-topological-space.tex | 73 +++++++++++++++++++++++++++--
 library/topology/urysohn2.tex               | 73 ++++++++++++++++++++++++-----
 4 files changed, 149 insertions(+), 18 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index cb3d5cf..b7de307 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -245,12 +245,31 @@
     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}
+%    Suppose $n,m,k \in \naturals$.
+%    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
+%\end{proposition}
+%\begin{proof}
+%    Let $P = \{n \in \naturals \mid \forall m,k \in \naturals .  n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
+%    $\zero \in P$.
+%    $P \subseteq \naturals$.
+%    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+%    Fix $n \in P$.
+%    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+%    Fix $m' \in \naturals$.
+%    Fix $k' \in \naturals$.
+%    $n \in \naturals$.
+%    $ \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}
     Suppose $n,m,k \in \naturals$.
     Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
 \end{proposition}
 \begin{proof}
+   %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
     Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$.
+
     $\zero \in P$.
     $P \subseteq \naturals$.
     It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index bcc5b8c..0ed7bab 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -7,7 +7,7 @@
 \section{Metric Spaces}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ 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 239965c..db46732 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -17,10 +17,73 @@
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
 \end{definition}
 
-\begin{theorem}\label{reals_as_topo_space}
-    Suppose $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
-    Then $\reals$ is a topological space.
+\begin{axiom}\label{reals_carrier_reals}
+    $\carrier[\reals] = \reals$.
+\end{axiom}
+
+\begin{theorem}\label{topological_basis_reals_is_prebasis}
+    $\topoBasisReals$ is a topological prebasis for $\reals$.
 \end{theorem}
 \begin{proof}
-    Omitted.
-\end{proof}
\ No newline at end of file
+    We show that $\unions{\topoBasisReals} \subseteq \reals$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
+        Fix $x \in \unions{\topoBasisReals}$.
+    \end{subproof}
+    We show that $\reals \subseteq \unions{\topoBasisReals}$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
+        Fix $x \in \reals$.
+    \end{subproof}
+\end{proof}
+
+\begin{theorem}\label{topological_basis_reals_is_basis}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}.
+    Let $B = \topoBasisReals$.
+    It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
+    Fix $U \in B$.
+    Fix $V \in B$.
+    Fix $x \in U, V$.
+\end{proof}
+
+\begin{axiom}\label{topological_space_reals}
+    $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
+\end{axiom}
+
+\begin{theorem}\label{reals_is_topological_space}
+    $\reals$ is a topological space.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+    Let $B = \topoBasisReals$.
+    We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$.
+    \begin{subproof}
+        It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$.
+        Fix $A \in \opens[\reals]$.
+        Follows by \cref{powerset_elim,topological_space_reals,genopens}.
+    \end{subproof}
+    We show that $\reals \in\opens[\reals]$.
+    \begin{subproof}
+        $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+        $\unions{B} \in \genOpens{B}{\reals}$.
+        $\reals \subseteq \unions{B}$.
+    \end{subproof}
+    We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,inters_in_genopens}.
+    \end{subproof}
+    We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,union_in_genopens}.
+    \end{subproof}
+    $\carrier[\reals] = \reals$.
+    Follows by \cref{topological_space}.
+\end{proof}
+
+\begin{proposition}\label{open_interval_is_open}
+    Suppose $a,b \in \reals$.
+    Then $\intervalopen{a}{b} \in \opens[\reals]$.
+\end{proposition}
\ No newline at end of file
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 396255e..838b121 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -152,16 +152,23 @@
 \begin{proposition}\label{no_natural_between_n_and_suc_n}
     For all $n,m \in \naturals$ we have not $n < m < \suc{n}$.
 \end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{naturals_is_zero_one_or_greater}
+    $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
     For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
 \end{proposition}
 \begin{proof}[Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
-    We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$.
-    \begin{subproof}
-        Trivial.
-    \end{subproof}
+    
     \begin{byCase}
         \caseOf{$n = \zero$.} 
             
@@ -196,9 +203,17 @@
         We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$.
         \begin{subproof}[Proof by \in-induction on $m$]
             Assume $m \in \naturals$.
-            %\begin{byCase}
-            %    
-            %\end{byCase}
+            \begin{byCase}
+                \caseOf{$\suc{m}=n$.}
+                \caseOf{$\suc{m}\neq n$.}  
+                      \begin{byCase}
+                        \caseOf{$n = \zero$.}
+                        \caseOf{$n \neq \zero$.}
+                            Take $l \in \naturals$ such that $\suc{l} = n$.
+                            Omitted.
+
+                      \end{byCase}
+            \end{byCase}
         \end{subproof}
     \end{subproof}
     
@@ -323,17 +338,51 @@
     For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
 \end{proposition}
 
+\begin{proposition}\label{bijection_naturals_order}
+    For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
-    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered.
+    Suppose $U$ is inhabited.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
-    Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}.
-    There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$.
-
-
+    Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Omitted.
+        \caseOf{$n \neq \zero$.}
+            Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
+            We have $\dom{U} \subseteq \naturals$.
+            $\dom{U}$ is inhabited.
+            We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
+            \begin{subproof}
+                Omitted.
+            \end{subproof}
+            Let $N = \seq{\zero}{k}$.
+            Let $M = \pow{X}$.
+            Define $V : N \to M$ such that $V(n)=$
+            \begin{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}
+                Trivial.
+            \end{subproof}
+            We show that $F$ is consistent on $U$ to $V$.
+            \begin{subproof}
+                Trivial.
+            \end{subproof}
+            $V$ is normal ordered.
+    \end{byCase}
+    
 \end{proof}
 
 
-- 
cgit v1.2.3


From 3ef20da08eda23db76d763a2c6c7ee416348a021 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 15 Sep 2024 19:05:25 +0200
Subject: Fix Assume Issue

At line 137 in real-topological-space.tex
Can't use Fix at this point.
---
 library/numbers.tex                         |   4 +-
 library/topology/real-topological-space.tex | 143 +++++++++++++++++++++++++++-
 2 files changed, 143 insertions(+), 4 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index b7de307..73eefc8 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -718,7 +718,7 @@ Laws of the order on the reals
 \end{proof}
 
 \begin{lemma}\label{reals_minus}
-    Assume $x,y \in \reals$. If $x \rminus y = \zero$ then $x=y$.
+    Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -803,7 +803,7 @@ Laws of the order on the reals
 \end{definition}
 
 \begin{definition}\label{realsplus}
-    $\realsplus = \reals \setminus \realsminus$.
+    $\realsplus = \{r \in \reals \mid r > \zero\}$.
 \end{definition}
 
 \begin{definition}\label{epsilon_ball}
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index db46732..8757ffb 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -21,6 +21,123 @@
     $\carrier[\reals] = \reals$.
 \end{axiom}
 
+\begin{lemma}\label{intervals_are_connected_in_reals}
+    Suppose $a,b \in \reals$.
+    Then for all $c \in \reals$ such that $a < c < b$ we have $c \in \intervalopen{a}{b}$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subset_reals_elem}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{intervalopen_iff}
+    Suppose $a,b,c \in \reals$.
+    Suppose $a < b$.
+    $c \in \intervalopen{a}{b}$ iff $a < c < b$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subseteq_reals_set}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} \subseteq \reals$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subset_reals_set}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} \subset \reals$.
+\end{lemma}
+
+\begin{lemma}\label{reals_order_minus_positiv}
+    Suppose $x,y \in \reals$.
+    Suppose $\zero < y$.
+    $x - y < x$.
+\end{lemma}
+
+\begin{lemma}\label{realsplus_bigger_zero}
+    For all $x \in \realsplus$ we have $\zero < x$.
+\end{lemma}
+
+\begin{lemma}\label{realsplus_in_reals}
+    For all $x \in \realsplus$ we have $x \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_inhabited}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon}$ is inhabited.
+\end{lemma}
+\begin{proof}
+    $x < x + \epsilon$.
+    $x - \epsilon < x$.
+    $x \in \epsBall{x}{\epsilon}$.
+\end{proof}
+
+\begin{lemma}\label{reals_elem_inbetween}
+    For all $a,b \in \reals$ such that $a < b$ we have there exists $c \in \reals$ such that $a < c < b$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_equal_openinterval}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} = \intervalopen{x - \epsilon}{x + \epsilon}$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior1}
+    For all $x \in \reals$ we have $x - x = \zero$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior2}
+    For all $x \in \reals$ we have $x + \neg{x} = \zero$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior3}
+    For all $x \in \reals$ we have $\neg{x} = \zero - x$.
+\end{lemma}
+
+\begin{lemma}\label{reals_order_is_addition_with_positiv_number}
+    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$.
+\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{lemma}\label{reals_order_plus_minus}
+    Suppose $a,b \in \reals$.
+    Suppose $\zero < b$.
+    Then $(a-b) < (a+b)$.
+\end{lemma}
+\begin{proof}
+    We show that $a < (a+b)$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    We show that $(a-b) < a$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{epsball_are_connected_in_reals}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then for all $c \in \reals$ such that $(x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+\end{lemma}
+\begin{proof}
+    $x - \epsilon \in \reals$.
+    $x + \epsilon \in \reals$.
+   
+    It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+    %Fix $c$ such that $c \in \reals \land (x - \epsilon) < c < (x + \epsilon)$.
+    %Suppose $(x - \epsilon) < c < (x + \epsilon)$.
+\end{proof}
+
 \begin{theorem}\label{topological_basis_reals_is_prebasis}
     $\topoBasisReals$ is a topological prebasis for $\reals$.
 \end{theorem}
@@ -29,11 +146,21 @@
     \begin{subproof}
         It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
         Fix $x \in \unions{\topoBasisReals}$.
+        \begin{byCase}
+            \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$.
+
+        \end{byCase}
     \end{subproof}
     We show that $\reals \subseteq \unions{\topoBasisReals}$.
     \begin{subproof}
         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}$.
     \end{subproof}
 \end{proof}
 
@@ -46,7 +173,15 @@
     It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
     Fix $U \in B$.
     Fix $V \in B$.
-    Fix $x \in U, V$.
+    It suffices to show that for all $x \in U \inter V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
+    Fix $x \in U \inter V$.
+    \begin{byCase}
+        \caseOf{$U \inter V = \emptyset$.}
+            Trivial.
+        \caseOf{$U \inter V \neq \emptyset$.}
+            Then $U \inter V$ is inhabited.
+            %It suffices to show that 
+    \end{byCase}
 \end{proof}
 
 \begin{axiom}\label{topological_space_reals}
@@ -86,4 +221,8 @@
 \begin{proposition}\label{open_interval_is_open}
     Suppose $a,b \in \reals$.
     Then $\intervalopen{a}{b} \in \opens[\reals]$.
-\end{proposition}
\ No newline at end of file
+\end{proposition}
+
+\begin{lemma}\label{safetwo}
+    Contradiction.
+\end{lemma}
\ No newline at end of file
-- 
cgit v1.2.3


From 13d7b11c23f8862c9f214c46ee05fad314e9e698 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 16:19:36 +0200
Subject: Finished proof of topological basis

---
 library/numbers.tex                         |   4 +-
 library/topology/real-topological-space.tex | 164 ++++++++++++++++++++++++++--
 2 files changed, 157 insertions(+), 11 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 73eefc8..98339ad 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -386,7 +386,9 @@ Commutivatiy of the standart operations
     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}
 
 
 Existence of  one and Zero
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index ffdf46e..428ee24 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -193,7 +193,7 @@
 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}
+\begin{lemma}\label{realsplus_in_reals_plus}
     For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$.
 \end{lemma}
 
@@ -207,6 +207,36 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
 \end{lemma}
 
+\begin{lemma}\label{reals_existence_addition_reverse}
+    For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+\end{lemma}
+\begin{proof}
+    Fix $\delta \in \reals$.
+    Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
+\end{proof}
+
+\begin{lemma}\label{reals_addition_minus_behavior1}
+    For all $a,b,c \in \reals$ such that $a = b + c$ we have $b = a - c$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $a \in \reals$ for all $b \in \reals$ for all $c \in \reals$ if $a = b + c$ then $b = a - c$.
+    Fix $a \in \reals$.
+    Fix $b \in \reals$.
+    Fix $c \in \reals$.
+    Suppose $a = b + c$.
+    Then $a + \neg{c} = b + c + \neg{c}$.
+    Therefore $a - c = b + c + \neg{c}$.
+    $a - c = (b + c) - c$.
+    $(b + c) - c = (b + c) + \neg{c}$.
+    $(b + c) + \neg{c} = b + (c + \neg{c})$.
+    $b + (c + \neg{c}) = b + (\zero)$.
+    $a - c = b$.
+\end{proof}
+
+\begin{lemma}\label{reals_addition_minus_behavior2}
+    For all $a,b,c \in \reals$ such that $a = b - c$ we have $b = c + a$.
+\end{lemma}
+
 \begin{lemma}\label{open_interval_eq_eps_ball}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
@@ -214,11 +244,71 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
 \end{lemma}
 \begin{proof}
     Let $\delta = (b-a)$.
-    $\delta$ is positiv by \cref{minus_}.
+    $\delta$ is positiv by \cref{minus_in_reals,minus_behavior3,reals_axiom_zero_in_reals,reals_order_behavior_with_addition,minus_behavior1,minus}.
     There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+    Let $x = a + \epsilon$.
+    $a + \delta = b$.
+    $a + \epsilon + \epsilon = b$. 
+    $x + \epsilon = b$.
+    $\epsilon \in \realsplus$ by \cref{reals_order_behavior_with_addition,reals_axiom_kommu,reals_axiom_zero,reals_order_is_transitive,reals_add,minus_behavior1,minus_behavior3,minus,reals_order_total,reals_axiom_zero_in_reals,realsplus}.
+    $a = x - \epsilon$.
+    $b = x + \epsilon$.
+    We show that $\intervalopen{a}{b} \subseteq \epsBall{x}{\epsilon}$.
+    \begin{subproof}
+        It suffices to show that for all $y \in \intervalopen{a}{b}$ we have $y \in \epsBall{x}{\epsilon}$.
+        Fix $y \in \intervalopen{a}{b}$.
+    \end{subproof}
+    We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$.
+    \begin{subproof}
+        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$.
+        Fix $y \in \epsBall{x}{\epsilon}$.
+    \end{subproof}
 
 \end{proof}
 
+\begin{lemma}\label{intersection_openinterval_inclusion_of_border}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_lower_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_upper_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_none_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    If $a \leq x < b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{b}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{reals_order_total2}
+    For all $a,b \in \reals$ we have $a < b \lor a > b \lor a = b$.
+\end{lemma}
 
 
 \begin{theorem}\label{topological_basis_reals_is_basis}
@@ -242,15 +332,69 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             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$.
+            Let $a = (x_1 - \alpha)$.
+            Let $b = (x_1 + \alpha)$.
+            Let $c = (x_2 - \beta)$.
+            Let $d = (x_2 + \beta)$.
+            We have $a < b$ and $a < x$ and $x < b$.
+            We have $c < d$ and $c < x$ and $x < d$.
+            We have $a \in \reals$.
+            We have $b \in \reals$.
+            We have $c \in \reals$.
+            We have $d \in \reals$.
+            We show that there exist $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
+            \begin{subproof} 
+                \begin{byCase}
+                    \caseOf{$a < c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                        \end{byCase}
+                    \caseOf{$a = c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                        \end{byCase}
+                    \caseOf{$a > c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                        \end{byCase}
+                \end{byCase}
             \end{subproof}
-            It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+
+            Take $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
+            We have $a',b' \in \reals$ by assumption.
+            We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}.
+            Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$.
+            Then $x \in \epsBall{x'}{\epsilon'}$.
+
+            Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
+            %Then $(x_1 - \alpha) < (x_2 + \beta)$.
+
+            %Therefore $U \inter V = \intervalopen{}{(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$.
-- 
cgit v1.2.3


From c021e79033abbb3fd4458304e701b3c54a284902 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 19:37:27 +0200
Subject: working commit

---
 latex/naproche.sty                          |   2 +
 library/numbers.tex                         |   8 ++
 library/topology/real-topological-space.tex | 144 ++++++++++++++++++++++++++++
 3 files changed, 154 insertions(+)

(limited to 'library/numbers.tex')

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 1a8afb6..c0fd318 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -156,6 +156,8 @@
 \newcommand{\abs}[1]{\left\lvert#1\right\rvert}
 \newcommand{\realsminus}{\reals_{-}}
 \newcommand{\at}[2]{#1(#2)}
+\newcommand{\intervalopenInfiniteLeft}[1]{(-\infty, #1)}
+\newcommand{\intervalopenInfiniteRight}[1]{(#1, \infty)}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/library/numbers.tex b/library/numbers.tex
index 98339ad..8624260 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -787,6 +787,14 @@ Laws of the order on the reals
     $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
 \end{definition}
 
+\begin{definition}\label{intervalopen_infinite_left}
+    $\intervalopenInfiniteLeft{b} = \{ x \in \reals \mid x < b\}$.
+\end{definition}
+
+\begin{definition}\label{intervalopen_infinite_right}
+    $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid a < x\}$.
+\end{definition}
+
 
 \begin{definition}\label{m_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 428ee24..b3efa20 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -461,3 +461,147 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b \in \reals$.
     Then $\intervalopen{a}{b} \in \opens[\reals]$.
 \end{proposition}
+\begin{proof}
+    If $a > b$ then $\intervalopen{a}{b} = \emptyset$.
+    If $a = b$ then $\intervalopen{a}{b} = \emptyset$.
+    It suffices to show that if $a < b$ then $\intervalopen{a}{b} \in \opens[\reals]$.
+    Suppose $a \rless b$.
+    Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+    It suffices to show that $\epsBall{x}{\epsilon} \in \opens[\reals]$.
+    $\topoBasisReals$ is a topological basis for $\reals$.
+    $\epsBall{x}{\epsilon} \in \topoBasisReals$.
+    $\topoBasisReals \subseteq \opens[\reals]$ by \cref{basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis}.
+\end{proof}
+
+\begin{lemma}\label{reals_minus_to_realsplus}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $(b - a) \in \realsplus$.
+\end{lemma}
+
+\begin{lemma}\label{existence_of_epsilon_upper_border}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. 
+\end{lemma}
+\begin{proof}
+    Let $\epsilon = b - a$.
+    Then $\epsilon \in \realsplus$.
+    It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}.
+    Suppose not.
+    Then $ b \in \epsBall{a}{\epsilon}$.
+    Therefore $ (a - \epsilon) < b < (a + \epsilon)$.
+    $b = (a + \epsilon)$.
+    Contradiction.
+\end{proof}
+
+\begin{lemma}\label{existence_of_epsilon_lower_border}
+    Suppose $a,b \in \reals$.
+    Suppose $a > b$.
+    Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. 
+\end{lemma}
+\begin{proof}
+    Let $\epsilon = a - b$.
+    Then $\epsilon \in \realsplus$.
+    It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}.
+    Suppose not.
+    Then $ b \in \epsBall{a}{\epsilon}$.
+    Therefore $ (a - \epsilon) < b < (a + \epsilon)$.
+    $b = (a - \epsilon)$.
+    Contradiction.
+\end{proof}
+
+\begin{proposition}\label{openinterval_infinite_left_in_opens}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+\end{proposition}
+\begin{proof}
+    Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteLeft{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta}  \}$.
+    We show that for all $x \in \intervalopenInfiniteLeft{a}$ we have there exists $e \in E$ such that $x \in e$.
+    \begin{subproof}
+        Fix $x \in \intervalopenInfiniteLeft{a}$.
+        Then $x < a$.
+        Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$.
+        $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_left}.
+        $a \notin \epsBall{x}{\delta'}$.
+        $\epsBall{x}{\delta'} \in E$.
+    \end{subproof}
+    $E \subseteq \topoBasisReals$.
+    We show that $\unions{E} = \intervalopenInfiniteLeft{a}$.
+    \begin{subproof}
+        We show that $\unions{E} \subseteq \intervalopenInfiniteLeft{a}$.
+        \begin{subproof}
+            It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteLeft{a}$.
+            Fix $x \in \unions{E}$.
+            Take $e \in E$ such that $x \in e$.
+            $x \in \reals$.
+            Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
+            $\epsBall{x'}{\delta'} \in E$.
+            We show that for all $y \in e$ we have $y < a$.
+            \begin{subproof}
+                Fix $y \in e$.
+                Then $y \in \epsBall{x'}{\delta'}$.
+                $e = \epsBall{x'}{\delta'}$.
+                There exists $x'' \in \intervalopenInfiniteLeft{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteLeft{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Suppose not.
+                Take $y' \in e$ such that $y' > a$. 
+                $x'' < a$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                Then $x'' < a < y'$.
+                Therefore $(x'' - \delta'') < a < (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_left,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq}.
+                Then $a \in e$ by \cref{epsball_are_connected_in_reals,intervalopen_infinite_left,neq_witness}.
+                Contradiction.
+            \end{subproof}
+            $x < a$.
+            Then $x \in \intervalopenInfiniteLeft{a}$.
+        \end{subproof}
+        We show that $\intervalopenInfiniteLeft{a} \subseteq \unions{E}$.
+        \begin{subproof}
+            Trivial.
+        \end{subproof}
+    \end{subproof}
+    $\unions{E} \in \opens[\reals]$.
+\end{proof}
+
+\begin{lemma}\label{continuous_on_basis_implies_continuous_endo}
+    Suppose $X$ is a topological space.
+    Suppose $B$ is a topological basis for $X$.
+    Suppose $f$ is a function from $X$ to $X$.
+    $f$ is continuous iff for all $b \in B$ we have $\preimg{f}{b} \in \opens[X]$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{openinterval_infinite_right_in_opens}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$.
+\end{proposition}
+\begin{proof}
+    Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
+    Let $f(x) = \neg{x}$ for $x \in \reals$.
+    $f$ is a function from $\reals$ to $\reals$.
+    We show that $f$ is continuous.
+    \begin{subproof}
+        It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
+        Fix $b \in \topoBasisReals$.
+        Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
+        Let $y = \neg{x}$.
+        It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
+        It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
+        Follows by set extensionality.
+    \end{subproof}
+    $\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+    We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_is_closed}
+    Suppose $a,b \in \reals$.
+    Then $\intervalclosed{a}{b} \in \closeds{\reals}$.
+\end{proposition}
-- 
cgit v1.2.3


From 3dca719ba8f9a59471f2c761cf8846cf597eae97 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 23:24:08 +0200
Subject: Topo Space Real Verfication

---
 library/numbers.tex                         |  10 +-
 library/topology/real-topological-space.tex | 200 +++++++++++++++++++++++++---
 2 files changed, 194 insertions(+), 16 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 8624260..406553e 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -792,7 +792,15 @@ Laws of the order on the reals
 \end{definition}
 
 \begin{definition}\label{intervalopen_infinite_right}
-    $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid a < x\}$.
+    $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid x > a\}$.
+\end{definition}
+
+\begin{definition}\label{intervalclosed_infinite_left}
+    $\intervalclosedInfiniteLeft{b} = \{ x \in \reals \mid x \leq b\}$.
+\end{definition}
+
+\begin{definition}\label{intervalclosed_infinite_right}
+    $\intervalclosedInfiniteRight{a} = \{ x \in \reals \mid x \geq a\}$.
 \end{definition}
 
 
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index b3efa20..e5e17ef 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -580,28 +580,198 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$.
 \end{proposition}
 \begin{proof}
-    Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
-    Let $f(x) = \neg{x}$ for $x \in \reals$.
-    $f$ is a function from $\reals$ to $\reals$.
-    We show that $f$ is continuous.
+    Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteRight{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta}  \}$.
+    We show that for all $x \in \intervalopenInfiniteRight{a}$ we have there exists $e \in E$ such that $x \in e$.
     \begin{subproof}
-        It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
-        Fix $b \in \topoBasisReals$.
-        Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
-        Let $y = \neg{x}$.
-        It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
-        It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
-        Follows by set extensionality.
+        Fix $x \in \intervalopenInfiniteRight{a}$.
+        Then $a < x$.
+        Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$.
+        $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_right}.
+        $a \notin \epsBall{x}{\delta'}$.
+        $\epsBall{x}{\delta'} \in E$.
     \end{subproof}
-    $\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
-    We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    $E \subseteq \topoBasisReals$.
+    We show that $\unions{E} = \intervalopenInfiniteRight{a}$.
     \begin{subproof}
-        Omitted.
+        We show that $\unions{E} \subseteq \intervalopenInfiniteRight{a}$.
+        \begin{subproof}
+            It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$.
+            Fix $x \in \unions{E}$.
+            Take $e \in E$ such that $x \in e$.
+            $x \in \reals$.
+            Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
+            $\epsBall{x'}{\delta'} \in E$.
+            We show that for all $y \in e$ we have $y > a$.
+            \begin{subproof}
+                Fix $y \in e$.
+                Then $y \in \epsBall{x'}{\delta'}$.
+                $e = \epsBall{x'}{\delta'}$.
+                There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Suppose not.
+                Take $y' \in e$ such that $y' < a$. 
+                $x'' > a$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                Then $x'' > a > y'$.
+                Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}.
+                Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}.
+                Contradiction.
+            \end{subproof}
+            $x > a$.
+            Then $x \in \intervalopenInfiniteRight{a}$.
+        \end{subproof}
+        We show that $\intervalopenInfiniteRight{a} \subseteq \unions{E}$.
+        \begin{subproof}
+            Trivial.
+        \end{subproof}
     \end{subproof}
-    Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+    $\unions{E} \in \opens[\reals]$.
+
+    %Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
+    %Let $f(x) = \neg{x}$ for $x \in \reals$.
+    %$f$ is a function from $\reals$ to $\reals$.
+    %We show that $f$ is continuous.
+    %\begin{subproof}
+    %    It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
+    %    Fix $b \in \topoBasisReals$.
+    %    Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
+    %    Let $y = \neg{x}$.
+    %    It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
+    %    It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    $\preimg{f}{\epsBall{x}{\epsilon}} \subseteq \reals$.
+    %    $\epsBall{y}{\epsilon} \subseteq \reals$ by \cref{intervalopen,subseteq,minus,epsilon_ball}.
+    %    %It suffices to show that for all $x \in \reals$ we have $x \in \epsBall{y}{\epsilon}$ iff $x \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    %Fix $x \in \reals$.
+    %    Let $u = (y - \epsilon)$.
+    %    Let $v = (y + \epsilon)$.
+    %    $u = \neg{(x - \epsilon)}$.
+    %    $v = \neg{(x + \epsilon)}$.
+    %    %$v - u = \epsilon + \epsilon$.
+    %    We show that for all $z \in \epsBall{y}{\epsilon}$ we have $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    \begin{subproof}
+    %        Fix $z \in \epsBall{y}{\epsilon}$.
+    %        Then $u < z < v$.
+    %        Let $z' = z - u$.
+    %        Then $z = u + z'$.
+    %        Suppose not.
+    %        Let $h = \neg{z}$.
+    %        $\neg{h} = \neg{\neg{z}}$.
+    %        $\neg{h} = z$.
+    %        Then $f(h) = \neg{h}$.
+    %        $f(h) = z$.
+    %        Then $z \in \preimg{f}{\{h\}}$.
+%
+    %    \end{subproof}
+    %    We show that for all $z \in \preimg{f}{\epsBall{x}{\epsilon}}$ we have $z \in \epsBall{y}{\epsilon}$.
+    %    \begin{subproof}
+    %        Fix $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %        Take $h \in \epsBall{x}{\epsilon}$ such that $f(h) = z$.
+    %    \end{subproof}
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %$\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+    %We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+    %Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals1}
+    Suppose $a,b \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+\end{lemma}
+\begin{proof}
+    We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$.
+    \begin{subproof}
+        Fix $x \in \reals$.
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals2}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals3}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteRight{a} \union \intervalclosedInfiniteLeft{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalclosedInfiniteLeft{a}$ or $x \in \intervalopenInfiniteRight{a}$.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_right}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
+\end{lemma}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteLeft{a} \inter \intervalclosedInfiniteRight{a} = \emptyset$.
+\end{lemma}
+
+\begin{proposition}\label{closedinterval_infinite_right_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_infinite_left_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteLeft{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteLeft{a} = \reals \setminus \intervalopenInfiniteRight{a}$.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_eq_openintervals_setminus_reals}
+    Suppose $a,b \in \reals$.
+    Then $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$.
+\end{proposition}
+\begin{proof}
+    We have $\intervalclosed{a}{b} \subseteq \reals$.
+    We show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+    \begin{subproof}
+        We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$.
+        \end{subproof}
+        We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$.
+        \end{subproof}
+    \end{subproof}
+    We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
+    \begin{subproof}
+        For all $x \in \intervalclosedInfiniteRight{a}$ we have $x \geq a$.
+        For all $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ we have $x \geq a$.
+        Follows by set extensionality.
+    \end{subproof}
+    $\reals \setminus \intervalopenInfiniteRight{b} = \intervalclosedInfiniteLeft{b}$.
+    It suffices to show that $\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a} = \intervalclosed{a}{b}$.
+    For all $x \in \intervalclosed{a}{b}$ we have $a \leq x \leq b$.
+    For all $x \in (\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a})$ we have $a \leq x \leq b$.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{closedinterval_is_closed}
     Suppose $a,b \in \reals$.
     Then $\intervalclosed{a}{b} \in \closeds{\reals}$.
 \end{proposition}
+\begin{proof}
+    We have $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+    It suffices to show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$ by \cref{closeds,setminus_subseteq,powerset_intro,closed_minus_open_is_closed,opens_type,subseteq_refl,union_open,is_closed_in,reals_carrier_reals,setminus_self,emptyset_open,reals_is_topological_space,openinterval_infinite_left_in_opens,openinterval_infinite_right_in_opens}.
+\end{proof}
-- 
cgit v1.2.3


From 5362771c14eccd80fd1a3ab6521c3a6ad9bb7838 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 17 Sep 2024 00:36:24 +0200
Subject: Corrected Math Env Parsing

Since Latex has a really specify syntax for
\begin{cases} ... \end{cases}
The math mode in tokenizing had to be setup correctly.
---
 library/numbers.tex                         |  3 +++
 library/topology/real-topological-space.tex | 27 +++++++++++++++------------
 source/Syntax/Concrete.hs                   |  6 +++---
 source/Syntax/Token.hs                      |  8 ++++----
 4 files changed, 25 insertions(+), 19 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 406553e..ac0a683 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -613,6 +613,9 @@ Laws of the order on the reals
 
 \subsection{Order on the reals}
 
+\begin{axiom}\label{reals_order_is_transitive}
+    For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
+\end{axiom}
 
 
 \begin{lemma}\label{plus_one_order}
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index e5e17ef..d9790aa 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -70,7 +70,7 @@
     Then $\epsBall{x}{\epsilon}$ is inhabited.
 \end{lemma}
 \begin{proof}
-    $x < x + \epsilon$.
+    $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}.
     $x - \epsilon < x$.
     $x \in \epsBall{x}{\epsilon}$.
 \end{proof}
@@ -104,12 +104,8 @@
     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$.
@@ -207,12 +203,16 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
 \end{lemma}
 
+\begin{lemma}\label{one_in_realsplus}
+    $1 \in \realsplus$.
+\end{lemma}
+
 \begin{lemma}\label{reals_existence_addition_reverse}
     For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
 \end{lemma}
 \begin{proof}
     Fix $\delta \in \reals$.
-    Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
+    Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
 \end{proof}
 
 \begin{lemma}\label{reals_addition_minus_behavior1}
@@ -260,7 +260,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     \end{subproof}
     We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$.
     \begin{subproof}
-        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$.
+        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}.
         Fix $y \in \epsBall{x}{\epsilon}$.
     \end{subproof}
 
@@ -270,7 +270,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+    Suppose $a \leq x < y \leq b$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -280,7 +281,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
+    Suppose $a = x$ and $b \leq y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -290,7 +292,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+    Suppose $a \leq x$ and $b = y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
 \end{lemma}
 \begin{proof}
     Omitted.
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 9d52995..7a89bea 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,15 +373,15 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula)
+    functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
                                     <*> (_to *> expr <* endMath <* _suchThat) 
                                     -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
                                     -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
-                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath)
-                                    <*> cases (many1 functionDefineCase)
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq )
+                                    <*> cases (many1 functionDefineCase) <* endMath <* optional _dot 
                                     <*> proof
 
 
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 52da86a..53e1e6a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,7 +189,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
                 Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
-                Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
+                --Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -205,7 +205,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
-                Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:))
+                --Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:))
                 Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:))
                 Just t -> goMath (f . (t:))
@@ -282,7 +282,7 @@ alignBegin = guardM isTextMode *> lexeme do
 casesBegin :: Lexer (Located Token)
 casesBegin = guardM isTextMode *> lexeme do
     Char.string "\\begin{cases}"
-    setMathMode
+    --setMathMode
     pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
@@ -301,7 +301,7 @@ alignEnd = guardM isMathMode *> lexeme do
 casesEnd :: Lexer (Located Token)
 casesEnd = guardM isMathMode *> lexeme do
     Char.string "\\end{cases}"
-    setTextMode
+    --setTextMode
     pure (EndEnv "cases")
 
 
-- 
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/numbers.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

