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

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

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