From b64a56c6325e1c2f0876049fb2a7dda6c06dbe3a Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 28 Aug 2024 14:17:27 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index a64fa7e..40a3615 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,13 @@
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
-
+\begin{theorem}\label{urysohnsetinbeetween}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $\closure{A}{X} \subseteq \interior{B}{X}$.
+    Suppose $\carrier[X]$ is inhabited.
+    There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
+\end{theorem}
 
 
 
@@ -60,6 +66,10 @@
 \end{theorem}
 \begin{proof}
 
+    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}))\}$.
+
+
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
@@ -70,7 +80,7 @@
     \end{cases}
 
 
-    $U_1$
+    
     Trivial.
     
     
-- 
cgit v1.2.3