From 3502f06c933df7e6177634a519d8c17c2a4d2d57 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 4 Jun 2024 15:49:18 +0200
Subject: Proof of teetwo_space_is_teeone_space

---
 library/topology/separation.tex | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'library')

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index f055495..530a51f 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -99,10 +99,6 @@
         For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$.
         Follows by set extensionality.
     \end{subproof}
-
-
-
-
     % Let $U_{y} \in \opens[X]$ such that $x \neq y \in X$.          Error: unexpected '{' expecting digit
     %For all $y$ there exists $U$ such that $x \neq y$ and $y \in U$ and $U \in \opens[X]$.
 
@@ -149,5 +145,13 @@
     Then $X$ is a \teeone-space.
 \end{proposition}
 \begin{proof}
-    Omitted. % TODO
+    We show that for all $x,y\in\carrier[X]$ such that $x\neq y$
+    there exist $U, V\in\opens[X]$ such that
+    $U\ni x\notin V$ and $V\ni y\notin U$.
+    \begin{subproof}
+        $X$ is hausdorff.
+        For all $x,y\in\carrier[X]$ such that $x\neq y$
+        there exist $U, V\in\opens[X]$ such that
+        $x\in U$ and $y\in V$ and $U$ is disjoint from $V$.
+    \end{subproof}
 \end{proof}
-- 
cgit v1.2.3