From 9563a18e455469bc64a9a8f61a95fb33f506bed0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 18 Jun 2024 17:07:15 +0200
Subject: Definition of T3 and regular spaces.

---
 library/topology/topological-space.tex | 26 +++++++-------------------
 1 file changed, 7 insertions(+), 19 deletions(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 7ff588d..c40aba4 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -239,18 +239,12 @@
     Then $A \subseteq \unions{F}$.
 \end{proposition}
 \begin{proof}
-    \begin{byCase}
-        %\caseOf{$F$ is empty.} 
-           %For all $X$ we have $X \notin F$.
-        %If $X \in F$ and $A \in X$ then $A \in F$.
-        %Contradiction by assumption.
-        %Omitted.
-        \caseOf{$F$ is inhabited.}
-        There exist $X \in F$ such that $X \subseteq \unions{F}$.
-        $A \subseteq X \subseteq \unions{F}$.
-    \end{byCase}
+    There exist $X \in F$ such that $X \subseteq \unions{F}$.
+    $A \subseteq X \subseteq \unions{F}$.
 \end{proof}
 
+
+
 \begin{proposition}\label{subseteq_inters_iff_to_left} 
     Let $A,F$ be sets.
     Suppose $F$ is inhabited.    % TODO:Remove!!
@@ -379,10 +373,6 @@
             Then $a \notin \unions{F'}$.
             Therefore $a \in \carrier[X] \setminus (\unions{F'})$.
         \end{subproof}
-
-        
-
-
         We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$.
         \begin{subproof}
             \begin{byCase}
@@ -426,17 +416,15 @@
     \end{byCase}
 \end{proof}
 
-\begin{definition}\label{set_of_closeds}
-    $\closeds[X] = \{ Y \in \pow{\carrier[X]} \mid \text{$Y$ is closed in $X$}\}$.
-\end{definition}
+
 
 \begin{proposition}\label{closure_is_minimal_closed_set}
     Let $X$ be a topological space.
     Suppose $A \subseteq \carrier[X]$.
-    For all $Y \in \closeds[X]$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$.  
+    For all $Y \in \closeds{X}$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$.  
 \end{proposition}
 \begin{proof}
-    Follows by \cref{closure,set_of_closeds,inters_subseteq_elem,closures}.
+    Follows by \cref{closure,closeds,inters_subseteq_elem,closures}.
 \end{proof}
 
 \begin{proposition}\label{complement_interior_eq_closure_complement}
-- 
cgit v1.2.3