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

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

(limited to 'library/topology')

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