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/topology/real-topological-space.tex | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 library/topology/real-topological-space.tex

(limited to 'library/topology/real-topological-space.tex')

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
-- 
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/topology/real-topological-space.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/topology/real-topological-space.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 640fe16eaab00ea29046ef18e6f751571d923eaa Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 02:12:06 +0200
Subject: Missmatched Assume Error found. not fixed

In line 137 and 140 of real-topological-space.tex
Line 140 wont get parsed and line 140 will get parsed.

Case matching in Checking.hs is not working as intended.
Case phi@(Atomic p args) ->    in line 960 in checking.hs
is not reached in checking of the Fixing with a symbol

Error Massage shows that < will be interpreted as a Term symbol there
not as a predicate.

Error Massage:
zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "<"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "c"),TermSymbol (SymbolMixfix [Just (Command "epsBall"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "x"),TermVar (NamedVar "epsilon")]]))
---
 library/topology/real-topological-space.tex | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'library/topology/real-topological-space.tex')

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 8757ffb..1c5e4cb 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -132,9 +132,17 @@
 \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)$.
+
+
+    %It suffices to show that for all $c$ such that $c \rless x$ we have $c \in \epsBall{x}{\epsilon}$.
+    %Fix $c$ such that $c \rless x$.
+%
+    %It suffices to show that for all $c$ such that $c < x$ we have $c \in \epsBall{x}{\epsilon}$.
+    %Fix $c$ such that $c < x$.
+
+
+    It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+    Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$.
     %Suppose $(x - \epsilon) < c < (x + \epsilon)$.
 \end{proof}
 
-- 
cgit v1.2.3


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

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

(limited to 'library/topology/real-topological-space.tex')

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


From 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/topology/real-topological-space.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/topology/real-topological-space.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/topology/real-topological-space.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/topology/real-topological-space.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 a9785eb4cac6b8c237173f7e14367babd79e92e1 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 17 Sep 2024 03:39:23 +0200
Subject: working commit

---
 library/topology/real-topological-space.tex | 36 +++++++++------
 library/topology/urysohn2.tex               | 72 ++++++++++++++++++++++++++---
 2 files changed, 86 insertions(+), 22 deletions(-)

(limited to 'library/topology/real-topological-space.tex')

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index d9790aa..b2e5ea9 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -382,7 +382,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             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'}$.
+            Then $x \in \epsBall{x'}{\epsilon'}$ by \cref{epsilon_ball}.
 
             Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
             %Then $(x_1 - \alpha) < (x_2 + \beta)$.
@@ -536,7 +536,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \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$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $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$.
@@ -550,8 +550,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 Suppose not.
                 Take $y' \in e$ such that $y' > a$. 
                 $x'' < a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 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}.
@@ -565,7 +565,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             Trivial.
         \end{subproof}
     \end{subproof}
-    $\unions{E} \in \opens[\reals]$.
+    $\unions{E} \in \opens[\reals]$ by \cref{opens_unions,reals_is_topological_space,basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis,subset_transitive}.
 \end{proof}
 
 \begin{lemma}\label{continuous_on_basis_implies_continuous_endo}
@@ -600,7 +600,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \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$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $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$.
@@ -612,10 +612,10 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 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$. 
+                Take $y' \in e$ such that $y' < a$ by \cref{reals_order_total,intervalopen,eps_ball_implies_open_interval}. 
                 $x'' > a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 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}.
@@ -689,6 +689,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     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$.
+        Follows by \cref{union_intro_left,intervalopen_infinite_left,reals_order_total,reals_order_total2,union_iff,intervalopen_infinite_right,union_assoc,union_intro_right,intervalclosed}.
     \end{subproof}
 \end{proof}
 
@@ -697,7 +698,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     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}$.
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$ by \cref{intervalopen_infinite_left,union_intro_left,neq_witness,intervalclosed_infinite_right,union_intro_right,union_iff}.
     Trivial.
 \end{proof}
 
@@ -714,6 +715,9 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a \in \reals$.
     Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
 \end{lemma}
+\begin{proof}
+    Follows by \cref{reals_order_total,inter_lower_left,intervalopen_infinite_right,order_reals_lemma6,inter_lower_right,foundation,subseteq,intervalclosed_infinite_left}.
+\end{proof}
 
 \begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
     Suppose $a \in \reals$.
@@ -725,7 +729,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
 \end{proposition}
 \begin{proof}
-    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$.
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{intersection_of_open_closed__infinite_intervals_open_left,reals_as_union_of_open_closed_intervals2,setminus_inter,double_relative_complement,subseteq_union_setminus,subseteq_setminus,setminus_union,setminus_disjoint,setminus_partition,setminus_subseteq,setminus_emptyset,setminus_self,setminus_setminus,double_complement_union}.
 \end{proof}
 
 \begin{proposition}\label{closedinterval_infinite_left_in_closeds}
@@ -747,15 +751,17 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         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}$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{setminus,double_complement_union}.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$ by \cref{union_upper_left,subseteq,union_comm,subseteq_implies_setminus_supseteq}.
+            Follows by \cref{inter_intro}.
         \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})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ by \cref{setminus_setminus,setminus}.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$ by \cref{inter_lower_right,elem_subseteq,setminus_setminus}.
         \end{subproof}
+        Follows by \cref{setminus_union}.
     \end{subproof}
     We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
     \begin{subproof}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 83e3aa4..9990199 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -94,6 +94,9 @@
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{nat_is_transitiveset}.
+\end{proof}
 
 \begin{proposition}\label{naturals_elem_in_transitive}
     If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
@@ -119,6 +122,9 @@
 \begin{proposition}\label{zero_is_empty}
     There exists no $x$ such that $x \in \zero$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{notin_emptyset}.
+\end{proof}
 
 \begin{proposition}\label{one_is_positiv}
     $1$ is positiv.
@@ -163,6 +169,13 @@
     Omitted.
 \end{proof}
 
+\begin{proposition}\label{naturals_one_zero_or_greater}
+    For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}.
+\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}
@@ -184,7 +197,7 @@
             \end{subproof}
         \caseOf{$n = 1$.}
             Fix $m$.
-            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
+            For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
             Then $\zero + 1 = 1$.
         \caseOf{$n > 1$.} 
             Take $l \in \naturals$ such that $\suc{l} = n$.
@@ -350,7 +363,7 @@
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
     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.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
     Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
@@ -360,11 +373,36 @@
         \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.
+            $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}.
+            $\dom{U}$ has cardinality $\suc{k}$.
             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.
+                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)$.
+                We have $\dom{U} \subseteq \naturals$.
+                $\dom{U}$ is inhabited.
+                Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
+                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                \begin{subproof}
+                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                    \begin{subproof}
+                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                        Fix $y \in \seq{\emptyset}{k'}$.
+                        Then $y \leq k'$.
+                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
+                        Therefore $y \in \suc{k}$.
+                        Therefore $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                    \begin{subproof}
+                        Fix $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                \end{subproof}
             \end{subproof}
+            Take $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')$.
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
             Define $V : N \to M$ such that $V(n)=
@@ -374,11 +412,31 @@
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                We show that $V$ is a chain of subsets in $X$.
+                \begin{subproof}
+                    It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}.
+                    It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $n \in \dom{V}$.
+                    Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                    It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                    Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                \end{subproof}
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V} \land n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
-            We show that $F$ is consistent on $U$ to $V$.
+            We show that $F$ is consistent on $V$ to $U$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}.
+                $F$ is a bijection from $\dom{V}$ to $\dom{U}$.
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
             $V$ is normal ordered.
     \end{byCase}
-- 
cgit v1.2.3


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

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

(limited to 'library/topology/real-topological-space.tex')

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


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

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

(limited to 'library/topology/real-topological-space.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