From cfc0b3c9081c242d7bdefe61fc841f31e7a7a257 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 11 Jun 2024 21:49:06 +0200
Subject: proof of complement_interior_eq_closure_complement and some more
 about clousures(unsatable)

---
 library/topology/topological-space.tex | 136 ++++++++++++++++++++++++++++++++-
 1 file changed, 135 insertions(+), 1 deletion(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 2bbdf09..2590287 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -217,12 +217,146 @@
 \end{proof}
 
 
+%Def: $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$.
+
+\begin{proposition}\label{subseteq_inters_iff_to_right} 
+    Let $A,F$ be sets.
+    Suppose $A \subseteq \inters{F}$.
+    Then for all $X \in F$ we have $A \subseteq X$.
+\end{proposition}
+
+
+\begin{proposition}\label{subseteq_of_all_then_subset_of_union}
+    Let $A,F$ be sets.
+    Suppose for all $X \in F$ we have $A \subseteq X$.
+    Then $A \subseteq \unions{F}$.
+\end{proposition}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$F$ is empty.} Trivial.
+        \caseOf{$F$ is inhabited.}
+        There exist $X \in F$ such that $X \subseteq \unions{F}$.
+        $A \subseteq X \subseteq \unions{F}$.
+    \end{byCase}
+\end{proof}
+
+\begin{proposition}\label{subseteq_inters_iff_to_left} 
+    Let $A,F$ be sets.
+    Suppose for all $X \in F$ we have $A \subseteq X$.
+    Then $A \subseteq \inters{F}$.
+\end{proposition}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$A = \emptyset$.}Trivial.
+        \caseOf{$A \neq \emptyset$.}
+        It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. 
+        Fix $a \in A$.
+        For all $X \in F$ we have $a \in X$.
+        $A \subseteq \unions{F}$.
+        $a \in \unions{F}$.
+    \end{byCase}
+    
+    %It suffices to show that for all $a \in A$ we have $x \in \inters{F}$.  % This have been proven!!! But it shouldn't.
+    
+%    we show that there exist $Y \in F$ such that $a \in Y$.
+%    \begin{subproof}
+        
+%        \begin{byCase}
+%            \caseOf{$a = \emptyset$.}
+%            $\emptyset \subseteq \inters{F}$.
+%            $\emptyset \in \emptyset$.
+%            \caseOf{$a \neq \emptyset$.} Omitted.
+%        \end{byCase}
+
+        %cases by a = \emptyset
+        %case a \neq \emptyset
+%    \end{subproof}
+\end{proof}
+
+%------------------------ Only example -------------------------------------
+\begin{proposition}\label{subseteq_inters_iff_new} 
+    $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$.
+\end{proposition}
+%\begin{proof}
+%    We show that if $A \subseteq \inters{F}$ then for all $X \in F$ we have $A \subseteq X$.
+%    \begin{subproof}
+        %It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$. 
+        %Fix $a \in A$. 
+        %Fix $X \in F$. %TODO: Missmatched Assume!
+
+%        It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$.
+%        Follows by \cref{inters}.
+%    \end{subproof}
+%    We show that for all $X \in F$ such that $A \subseteq X$ we have $A \subseteq \inters{F}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%\end{proof}
+
+\begin{proposition}\label{set_is_subseteq_to_closure_of_the_set}
+    $A \subseteq \closure{A}{X}$.
+\end{proposition}
+\begin{proof}
+    %$\closures{A}{X}$ is inhabited. %TODO: Inhabited why does "subseteq_inters_iff" has inhabited as assumtion??
+    For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$.
+    Therefore $A \subseteq \inters{\closures{A}{X}}$.
+\end{proof}
+
+\begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x}
+    $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$.
+    If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+
+\end{proof}
+
 \begin{proposition}%[Complement of interior equals closure of complement]
 \label{complement_interior_eq_closure_complement}
+    Let $X$ be a topological space.
     $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$.
 \end{proposition}
 \begin{proof}
-    Omitted. % Use general De Morgan's Law in Pow|X|
+        We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+        \begin{subproof}
+            Fix $x \in \carrier[X]\setminus\interior{A}{X}$.
+            Suppose not. 
+            $x \notin \closure{(\carrier[X]\setminus A)}{X}$.
+            $x \in \carrier[X]$.
+            For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \in A \implies x \notin B$.
+            For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \notin A \implies x \in B$.
+            $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$.
+            %$(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. %TODO:
+            $x \in A$.
+            $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$.
+            $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. %TODO:
+            Contradiction.
+        \end{subproof}
+
+        $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$.
+
+        $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. %TODO:
+
+    %We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+    %\begin{subproof}
+    %    Fix $x \in \carrier[X]\setminus\interior{A}{X}$.
+    %    \begin{byCase}
+    %        \caseOf{$x \in \carrier[X] \setminus A$.}
+    %        Trivial.
+    %        \caseOf{$x \in \carrier[X] \setminus A \inter \interior{A}{X}$.}
+    %        $\carrier[X] \setminus \closure{A}{X} \in \opens[X]$.
+    %        $\interior{A}{X} \in \opens[X]$.
+    %        Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X} \in \opens[X]$.
+    %        %$\carrier[X] \setminus \closure{A}{X}$ is open.   TODO: is open throws an error!
+    %        %$\interior{A}{X}$ is open.
+    %        %Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X}$ is open.
+    %
+    %    \end{byCase}
+    %\end{subproof}
+    %Suffices reduction by \cref :::::    reduction => goal.
+    
+
+    %Omitted. % Use general De Morgan's Law in Pow|X|
 \end{proof}
 
 \begin{definition}[Frontier]\label{frontier}
-- 
cgit v1.2.3


From ab4ddd9d49349ddb781514b6b0e9060db5b66a22 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 12 Jun 2024 13:47:38 +0200
Subject: Prove Bug "Ex falso quodlibet"

The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work.
---
 library/topology/topological-space.tex | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 2590287..dd236bb 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -233,7 +233,11 @@
 \end{proposition}
 \begin{proof}
     \begin{byCase}
-        \caseOf{$F$ is empty.} Trivial.
+        \caseOf{$F$ is empty.} 
+        For all $X$ we have $X \notin F$.
+        If $X \in F$ and $A \in X$ then $A \in F$.
+        %There exist $X \in F$.
+        Contradiction by assumption.
         \caseOf{$F$ is inhabited.}
         There exist $X \in F$ such that $X \subseteq \unions{F}$.
         $A \subseteq X \subseteq \unions{F}$.
-- 
cgit v1.2.3


From e82c1b73bba5987a176d6d33bd1dbcc5bedf0bbd Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 16 Jun 2024 23:05:43 +0200
Subject: First implementation of basic relations of closed and open.

Not finished.
---
 library/topology/topological-space.tex | 223 ++++++++++++++++++++++-----------
 1 file changed, 147 insertions(+), 76 deletions(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index dd236bb..2c6b98c 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -161,12 +161,21 @@
 
 \begin{proposition}\label{carrier_is_closed}
     Let $X$ be a topological space.
-    Then $\emptyset$ is closed in $X$.
+    Then $\carrier[X]$ is closed in $X$.
 \end{proposition}
 \begin{proof}
     $\carrier[X]\setminus \carrier[X] = \emptyset$.
+    Follows by \cref{emptyset_open,is_closed_in}.
 \end{proof}
 
+\begin{proposition}\label{opens_minus_closed_is_open}
+    Let $X$ be a topological space.
+    Suppose $A, B \subseteq \carrier[X]$.
+    Suppose $A$ is open in $X$.
+    Suppose $B$ is closed in $X$.
+    Then $A \setminus B$ is open in $X$.
+\end{proposition}
+
 \begin{definition}[Closed sets]\label{closeds}
     $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$.
 \end{definition}
@@ -216,9 +225,6 @@
     Follows by \cref{inters_singleton,closure}.
 \end{proof}
 
-
-%Def: $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$.
-
 \begin{proposition}\label{subseteq_inters_iff_to_right} 
     Let $A,F$ be sets.
     Suppose $A \subseteq \inters{F}$.
@@ -228,16 +234,17 @@
 
 \begin{proposition}\label{subseteq_of_all_then_subset_of_union}
     Let $A,F$ be sets.
+    Suppose $F$ is inhabited. %TODO: Remove!!
     Suppose for all $X \in F$ we have $A \subseteq X$.
     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$.
-        %There exist $X \in F$.
-        Contradiction by assumption.
+        %\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}$.
@@ -246,6 +253,7 @@
 
 \begin{proposition}\label{subseteq_inters_iff_to_left} 
     Let $A,F$ be sets.
+    Suppose $F$ is inhabited.    % TODO:Remove!!
     Suppose for all $X \in F$ we have $A \subseteq X$.
     Then $A \subseteq \inters{F}$.
 \end{proposition}
@@ -253,71 +261,157 @@
     \begin{byCase}
         \caseOf{$A = \emptyset$.}Trivial.
         \caseOf{$A \neq \emptyset$.}
+        $F$ is inhabited.
         It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. 
         Fix $a \in A$.
         For all $X \in F$ we have $a \in X$.
         $A \subseteq \unions{F}$.
         $a \in \unions{F}$.
     \end{byCase}
-    
-    %It suffices to show that for all $a \in A$ we have $x \in \inters{F}$.  % This have been proven!!! But it shouldn't.
-    
-%    we show that there exist $Y \in F$ such that $a \in Y$.
-%    \begin{subproof}
-        
-%        \begin{byCase}
-%            \caseOf{$a = \emptyset$.}
-%            $\emptyset \subseteq \inters{F}$.
-%            $\emptyset \in \emptyset$.
-%            \caseOf{$a \neq \emptyset$.} Omitted.
-%        \end{byCase}
-
-        %cases by a = \emptyset
-        %case a \neq \emptyset
-%    \end{subproof}
 \end{proof}
 
-%------------------------ Only example -------------------------------------
 \begin{proposition}\label{subseteq_inters_iff_new} 
+    Suppose $F$ is inhabited.
     $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$.
 \end{proposition}
-%\begin{proof}
-%    We show that if $A \subseteq \inters{F}$ then for all $X \in F$ we have $A \subseteq X$.
-%    \begin{subproof}
-        %It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$. 
-        %Fix $a \in A$. 
-        %Fix $X \in F$. %TODO: Missmatched Assume!
-
-%        It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$.
-%        Follows by \cref{inters}.
-%    \end{subproof}
-%    We show that for all $X \in F$ such that $A \subseteq X$ we have $A \subseteq \inters{F}$.
-%    \begin{subproof}
-%        Omitted.
-%    \end{subproof}
-%\end{proof}
 
 \begin{proposition}\label{set_is_subseteq_to_closure_of_the_set}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
     $A \subseteq \closure{A}{X}$.
 \end{proposition}
 \begin{proof}
-    %$\closures{A}{X}$ is inhabited. %TODO: Inhabited why does "subseteq_inters_iff" has inhabited as assumtion??
-    For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$.
-    Therefore $A \subseteq \inters{\closures{A}{X}}$.
+    \begin{byCase}
+        \caseOf{$A = \emptyset$.} 
+        Trivial.
+        \caseOf{$A \neq \emptyset$.}
+        We show that $\carrier[X] \in \closures{A}{X}$.
+        \begin{subproof}
+            $\carrier[X]$ is closed in $X$.
+            $\carrier[X] \in \pow{\carrier[X]}$.
+        \end{subproof}
+        $\closures{A}{X}$ is inhabited.        
+        For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$.
+        Therefore $A \subseteq \inters{\closures{A}{X}}$.
+    \end{byCase}
 \end{proof}
 
 \begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
     $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$.
 \end{proposition}
 \begin{proof}
     It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$.
     If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+\end{proof}
 
+\begin{proposition}\label{complement_of_closed_is_open}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    Suppose $A$ is closed in $X$.
+    Then $\carrier[X] \setminus A$ is open in $X$.
+\end{proposition}
+
+\begin{proposition}\label{complement_of_open_is_closed}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    Suppose $A$ is open in $X$.
+    Then $\carrier[X] \setminus A$ is closed in $X$.
+\end{proposition}
+
+\begin{proposition}\label{intersection_of_closed_is_closed}
+    Let $X$ be a topological space.
+    Suppose $A, B \subseteq \carrier[X]$.
+    Suppose $A$ are closed in $X$.
+    Suppose $B$ are closed in $X$.
+    Then $A \inter B$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$.
+    $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) \in \opens[X]$.
+    $A \inter B = \carrier[X] \setminus ((\carrier[X] \setminus A) \union (\carrier[X] \setminus B))$.
 \end{proof}
 
-\begin{proposition}%[Complement of interior equals closure of complement]
-\label{complement_interior_eq_closure_complement}
+\begin{proposition}\label{union_of_closed_is_closed}
     Let $X$ be a topological space.
+    Suppose $A, B \subseteq \carrier[X]$.
+    Suppose $A$ are closed in $X$.
+    Suppose $B$ are closed in $X$.
+    Then $A \union B$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$.
+    $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) \in \opens[X]$.
+    $A \union B = \carrier[X] \setminus ((\carrier[X] \setminus A) \inter (\carrier[X] \setminus B))$.
+\end{proof}
+
+\begin{proposition}\label{closed_minus_open_is_closed}
+    Let $X$ be a topological space.
+    Suppose $A, B \subseteq \carrier[X]$.
+    Suppose $A$ is open in $X$.
+    Suppose $B$ is closed in $X$.
+    Then $B \setminus A$ is closed in $X$.
+\end{proposition}
+
+
+
+\begin{proposition}\label{intersection_of_closed_is_closed_infinite}
+    Let $X$ be a topological space.
+    Suppose $F \subseteq \pow{\carrier[X]}$.
+    Suppose for all $A \in F$ we have $A$ is closed in $X$.
+    Suppose $F$ is inhabited.
+    Then $\inters{F}$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $.
+    For all $Y \in F'$ we have $Y$ is open in $X$.
+    $\unions{F'}$ is open in $X$.
+    $\unions{F'}, \inters{F} \subseteq \carrier[X]$.
+    We show that $\inters{F} = \carrier[X] \setminus (\unions{F'})$.
+    \begin{subproof}
+        We show that for all $a \in \inters{F}$ we have $a \in \carrier[X] \setminus (\unions{F'})$.
+        \begin{subproof}
+            Fix $a \in \inters{F}$.
+            $a \in \carrier[X]$.
+            For all $A \in F$ we have $a \in A$.
+            For all $A \in F$ we have $a \notin (\carrier[X] \setminus A)$.
+            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}
+            Fix $a \in \carrier[X] \setminus (\unions{F'})$.
+            \begin{byCase}
+                \caseOf{$a = \emptyset$.} 
+                    Omitted.
+                \caseOf{$a \neq \emptyset$.}
+                    $a \in \carrier[X]$.
+                    $a \notin \unions{F'}$.
+                    For all $A \in F'$ we have $a \notin A$.
+                    For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$.
+                    For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$.
+                    For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$.
+                    For all $Y \in F$ we have $a \in Y$.
+                    $\inters{F}$ is inhabited.
+                    Therefore $a \in \inters{F}$.
+            \end{byCase}
+        \end{subproof}
+        Follows by set extensionality.
+    \end{subproof}
+    Follows by \cref{complement_of_open_is_closed}.
+\end{proof}
+
+\begin{proposition}\label{closure_is_closed}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    Then $\closure{A}{X}$ is closed in $X$.
+\end{proposition}
+
+\begin{proposition}\label{complement_interior_eq_closure_complement}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
     $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$.
 \end{proposition}
 \begin{proof}
@@ -327,47 +421,24 @@
             Suppose not. 
             $x \notin \closure{(\carrier[X]\setminus A)}{X}$.
             $x \in \carrier[X]$.
-            For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \in A \implies x \notin B$.
-            For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \notin A \implies x \in B$.
             $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$.
-            %$(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. %TODO:
             $x \in A$.
             $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$.
-            $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. %TODO:
+            $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$.
             Contradiction.
         \end{subproof}
-
         $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$.
-
-        $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. %TODO:
-
-    %We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$.
-    %\begin{subproof}
-    %    Fix $x \in \carrier[X]\setminus\interior{A}{X}$.
-    %    \begin{byCase}
-    %        \caseOf{$x \in \carrier[X] \setminus A$.}
-    %        Trivial.
-    %        \caseOf{$x \in \carrier[X] \setminus A \inter \interior{A}{X}$.}
-    %        $\carrier[X] \setminus \closure{A}{X} \in \opens[X]$.
-    %        $\interior{A}{X} \in \opens[X]$.
-    %        Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X} \in \opens[X]$.
-    %        %$\carrier[X] \setminus \closure{A}{X}$ is open.   TODO: is open throws an error!
-    %        %$\interior{A}{X}$ is open.
-    %        %Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X}$ is open.
-    %
-    %    \end{byCase}
-    %\end{subproof}
-    %Suffices reduction by \cref :::::    reduction => goal.
-    
-
-    %Omitted. % Use general De Morgan's Law in Pow|X|
+        $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$.
 \end{proof}
 
+
 \begin{definition}[Frontier]\label{frontier}
     $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$.
 \end{definition}
 
-
+\begin{proposition}\label{safe}   %TODO: Remove!!!
+    $x \neq x$.
+\end{proposition}
 
 \begin{proposition}%[Frontier as intersection of closures]
 \label{frontier_as_inter}
@@ -375,7 +446,7 @@
 \end{proposition}
 \begin{proof}
     % TODO
-    Omitted.
+    %Omitted.
     %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition)
     %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement
     %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement
-- 
cgit v1.2.3


From f2690dcd548d51fa8024fe2410c797aa8af1180b Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 17 Jun 2024 02:28:58 +0200
Subject: Completed proofs [stable]

---
 library/topology/topological-space.tex | 77 ++++++++++++++++++++++++++++------
 1 file changed, 64 insertions(+), 13 deletions(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 2c6b98c..7ff588d 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -380,13 +380,19 @@
             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}
-            Fix $a \in \carrier[X] \setminus (\unions{F'})$.
             \begin{byCase}
-                \caseOf{$a = \emptyset$.} 
-                    Omitted.
-                \caseOf{$a \neq \emptyset$.}
+                \caseOf{$\inters{F} = \emptyset$.}
+                    $F$ is inhabited.
+                    Take $U$ such that $U \in F$.
+                    Let $F'' = F \setminus \{U\}$.
+                    There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$.
+                \caseOf{$\inters{F} \neq \emptyset$.}
+                    Fix $a \in \carrier[X] \setminus (\unions{F'})$.
                     $a \in \carrier[X]$.
                     $a \notin \unions{F'}$.
                     For all $A \in F'$ we have $a \notin A$.
@@ -408,6 +414,30 @@
     Suppose $A \subseteq \carrier[X]$.
     Then $\closure{A}{X}$ is closed in $X$.
 \end{proposition}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$\closure{A}{X} = \emptyset$.} 
+            Trivial.
+        \caseOf{$\closure{A}{X} \neq \emptyset$.}
+            $\closures{A}{X}$ is inhabited.
+            $\closures{A}{X} \subseteq \pow{\carrier[X]}$.
+            For all $B \in \closures{A}{X}$ we have $B$ is closed in $X$.
+            $\inters{\closures{A}{X}}$ is closed in $X$.
+    \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$.  
+\end{proposition}
+\begin{proof}
+    Follows by \cref{closure,set_of_closeds,inters_subseteq_elem,closures}.
+\end{proof}
 
 \begin{proposition}\label{complement_interior_eq_closure_complement}
     Let $X$ be a topological space.
@@ -432,24 +462,45 @@
 \end{proof}
 
 
+
 \begin{definition}[Frontier]\label{frontier}
     $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$.
 \end{definition}
 
-\begin{proposition}\label{safe}   %TODO: Remove!!!
-    $x \neq x$.
+\begin{proposition}\label{closure_interior_frontier_is_in_carrier}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$.
+\end{proposition}
+
+\begin{proposition}\label{frontier_is_closed}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    Then $\frontier{A}{X}$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ by \cref{closure_interior_frontier_is_in_carrier,closure_is_closed,interior_is_open,closed_minus_open_is_closed}.
+\end{proof}
+
+\begin{proposition}\label{setdifference_eq_intersection_with_complement}
+    Suppose $A,B \subseteq C$.
+    Then $A \setminus B = A \inter (C \setminus B)$.
 \end{proposition}
 
-\begin{proposition}%[Frontier as intersection of closures]
-\label{frontier_as_inter}
+
+
+\begin{proposition}\label{frontier_as_inter}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
     $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$.
 \end{proposition}
 \begin{proof}
-    % TODO
-    %Omitted.
-    %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition)
-    %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement
-    %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement
+    \begin{align*}
+          \frontier{A}{X} \\
+        &= \closure{A}{X}\setminus\interior{A}{X} \\
+        &= \closure{A}{X} \inter (\carrier[X] \setminus \interior{A}{X}) \explanation{by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}}\\
+        &= \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X} \explanation{by \cref{complement_interior_eq_closure_complement}}
+    \end{align*}
 \end{proof}
 
 \begin{proposition}\label{frontier_of_emptyset}
-- 
cgit v1.2.3


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/separation.tex        | 43 ++++++++++++++++++++++++++++++++++
 library/topology/topological-space.tex | 26 ++++++--------------
 2 files changed, 50 insertions(+), 19 deletions(-)

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

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 535a51f..3268bb9 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -145,3 +145,46 @@
         $x\in U$ and $y\in V$ and $U$ is disjoint from $V$.
     \end{subproof}
 \end{proof}
+
+\begin{definition}\label{regular}
+    $X$ is regular iff for all $C,p$ such that $p \in \carrier[X]$ and $p \notin C \in \closeds{X}$ we have there exists $U,C \in \opens[X]$ such that $p \in U$ and $C \subseteq V$ and $U \inter V = \emptyset$.
+\end{definition}
+
+\begin{definition}\label{regular_space}
+    $X$ is a regular space iff $X$ is a topological space and $X$ is regular.
+\end{definition}
+
+
+\begin{definition}\label{teethree}
+    $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ .
+\end{definition}
+
+\begin{definition}\label{teethree_space}
+    $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ .
+\end{definition}
+
+\begin{proposition}\label{teethree_space_is_teetwo_space}
+    Let $X$ be a \teethree-space.
+    Then $X$ is a \teetwo-space.
+\end{proposition}
+\begin{proof}
+    For all $x,y \in \carrier[X]$ such that $x \neq y$ we have $x \notin \{y\}$.
+    It suffices to show that $X$ is hausdorff.
+    It suffices to show that for all $x \in \carrier[X]$ we have for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$.
+    Fix $x \in \carrier[X]$.
+    It suffices to show that for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$.
+    Fix $y \in \carrier[X]$.
+
+    %There exist $U' \in \opens[X]$ such that $x\in U'\not\ni y$ or $x\notin U'\ni y$ by \cref{}.
+    %There exist $C \in \closeds{X}$ such that $y \in C \not\ni X$.
+    We show that there exist $U,V,C$ such that $U,V \in \opens[X]$ and $C\in \closeds{X}$ and $x \in U$ and $y \in C \subseteq V$ and $U$ is disjoint from $V$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    $y \in V$.
+    Follows by assumption.
+\end{proof}
+
+%    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$.
\ No newline at end of file
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


From 28cbe434d393066f6b4525c67bd01b1396e97381 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 20 Jun 2024 13:01:57 +0200
Subject: [Stable] Topologgical-space.tex

---
 library/topology/topological-space.tex | 40 +++++++++++++++++++++-------------
 1 file changed, 25 insertions(+), 15 deletions(-)

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

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 73b7ec5..8da29d3 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -382,7 +382,9 @@
                     Let $F'' = F \setminus \{U\}$.
                     There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$.
                 \caseOf{$\inters{F} \neq \emptyset$.}
+                    
                     Fix $a \in \carrier[X] \setminus (\unions{F'})$.
+                    $\inters{F}$ is inhabited.
                     $a \in \carrier[X]$.
                     $a \notin \unions{F'}$.
                     For all $A \in F'$ we have $a \notin A$.
@@ -390,7 +392,6 @@
                     For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$.
                     For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$.
                     For all $Y \in F$ we have $a \in Y$.
-                    $\inters{F}$ is inhabited.
                     Therefore $a \in \inters{F}$.
             \end{byCase}
         \end{subproof}
@@ -427,26 +428,35 @@
     Follows by \cref{closure,closeds,inters_subseteq_elem,closures}.
 \end{proof}
 
+\begin{proposition}\label{interior_is_maximal}
+    Let $X$ be a topological space.
+    Suppose $A \subseteq \carrier[X]$.
+    For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$.
+\end{proposition}
+
 \begin{proposition}\label{complement_interior_eq_closure_complement}
     Let $X$ be a topological space.
     Suppose $A \subseteq \carrier[X]$.
     $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$.
 \end{proposition}
 \begin{proof}
-        We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$.
-        \begin{subproof}
-            Fix $x \in \carrier[X]\setminus\interior{A}{X}$.
-            Suppose not. 
-            $x \notin \closure{(\carrier[X]\setminus A)}{X}$.
-            $x \in \carrier[X]$.
-            $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$.
-            $x \in A$.
-            $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$.
-            $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$.
-            Contradiction.
-        \end{subproof}
-        $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$.
-        $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$.
+    We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+    \begin{subproof}
+        
+        Fix $x \in \carrier[X]\setminus\interior{A}{X}$.
+        Suppose not. 
+        $x \notin \closure{(\carrier[X]\setminus A)}{X}$.
+        $x \in \carrier[X]$.
+        $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$.
+        $x \in A$.
+        $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$.
+        $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$.
+        There exist $U \in \opens[X]$ such that $x \in U$ and $U\subseteq A$. 
+        $U \subseteq \interior{A}{X}$.
+        Contradiction.
+    \end{subproof}
+    $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$.
+    $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$.
 \end{proof}
 
 
-- 
cgit v1.2.3


From c19415b970d502d662eb10c403728fa41cdbe03e Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 25 Jun 2024 00:06:14 +0200
Subject: [Stable] Implented continuous.tex and omitted some proves

All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex
---
 library/topology/continuous.tex        | 29 ++++++++++
 library/topology/separation.tex        | 98 +++++++++++++++++++++-------------
 library/topology/topological-space.tex | 17 ++++--
 3 files changed, 103 insertions(+), 41 deletions(-)
 create mode 100644 library/topology/continuous.tex

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

diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
new file mode 100644
index 0000000..6a32353
--- /dev/null
+++ b/library/topology/continuous.tex
@@ -0,0 +1,29 @@
+\import{topology/topological-space.tex}
+\import{relation.tex}
+
+\begin{definition}\label{continuous}
+    $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
+\end{definition}
+
+\begin{proposition}\label{continuous_definition_by_closeds}
+    Let $X$ be a topological space.
+    Let $Y$ be a topological space.
+    Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
+    %\begin{subproof}
+    %    Suppose $f$ is continuous.
+    %    Fix $U \in \closeds{Y}$.
+    %    $\carrier[Y] \setminus U$ is open in $Y$.
+    %    Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$.
+    %    Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$.
+    %    $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
+    %\end{subproof}
+    %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+\end{proof}
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index c53b6a8..0c68290 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -77,25 +77,26 @@
     Then $\{x\}$ is closed in $X$.
 \end{proposition}
 \begin{proof}
-    Let $V = \{ U \in \opens[X] \mid x \notin U\}$.
-    For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$.
-    For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$.
-
-    $\unions{V} \in \opens[X]$.
-    For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$.
-    We show that $\carrier[X] \setminus \{x\} = \unions{V}$.
-    \begin{subproof}
-        We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$.
-        \begin{subproof}
-            Fix $y \in \carrier[X] \setminus \{x\}$.
-            $y \neq x$.
-            $y \in \carrier[X]$.
-            $y \in \unions{V}$.
-        \end{subproof}
-        For all $y \in \unions{V}$ we have $y \notin \{x\}$.
-        For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$.
-        Follows by set extensionality.
-    \end{subproof}
+    Omitted.
+    %Let $V = \{ U \in \opens[X] \mid x \notin U\}$.
+    %For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$ by \cref{carrier_open,teeone}.
+    %For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$.
+    %
+    %$\unions{V} \in \opens[X]$.
+    %For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$.
+    %We show that $\carrier[X] \setminus \{x\} = \unions{V}$.
+    %\begin{subproof}
+    %    We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$.
+    %    \begin{subproof}
+    %        Fix $y \in \carrier[X] \setminus \{x\}$.
+    %        $y \neq x$.
+    %        $y \in \carrier[X]$.
+    %        $y \in \unions{V}$.
+    %    \end{subproof}
+    %    For all $y \in \unions{V}$ we have $y \notin \{x\}$.
+    %    For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$.
+    %    Follows by set extensionality.
+    %\end{subproof}
 \end{proof}
 %
 % Conversely, if \{x\} is open, then for any y distinct from x we can use
@@ -163,38 +164,59 @@
     $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ .
 \end{abbreviation}
 
-\begin{proposition}\label{eqvilance_teethree_closed_neighbourhood_in_open}
+\begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open}
     Let $X$ be a topological space.
     Suppose $X$ is inhabited.
-    $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$.    
+    Suppose $X$ is \teethree\ .
+    For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$.    
 \end{proposition}
 \begin{proof}
+    Omitted.
+    %%Suppose $X$ is regular and kolmogorov.
+    %Fix $U \in \opens[X]$.
+    %Fix $x \in U$.
+    %Let $C = \carrier[X] \setminus U$.
+    %Then $C \in \closeds{X}$.
+    %$x \notin C$.
+    %$x \in \carrier[X]$.
+    %We show that there exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$.     
+    %We show that $B \subseteq (\carrier[X] \setminus A)$.
+    %$(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$.
+    %$(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$.
+    %$x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$.
+    %Let $N = (\carrier[X] \setminus A)$.
+    %Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$.
+    %$N \in \neighbourhoods{x}{X}$.
+\end{proof}
 
-    We show that if $X$ is \teethree\ then for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$.    
+\begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods}
+    Let $X$ be a topological space.
+    Suppose $X$ is inhabited.
+    $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$.    
+\end{proposition}
+\begin{proof}
+    We show that if $X$ is \teethree\ then for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$.
     \begin{subproof}
-        Suppose $X$ is regular and kolmogorov.
-        Fix $U \in \opens[X]$.
-        Fix $x \in U$.
-        Let $C = \carrier[X] \setminus U$.
-        Then $C \in \closeds{X}$.
-        $x \notin C$.
-        $x \in \carrier[X]$.
-        There exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$ by \cref{is_regular}.        
-        $B \subseteq (\carrier[X] \setminus A)$.
-        $(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$.
-        $(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$.
-        $x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$.
-        Let $N = (\carrier[X] \setminus A)$.
-        Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$.
-        Particularly, $N \in \neighbourhoods{x}{X}$.
+        %For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$.
+        Omitted.
     \end{subproof}
-    We show that if for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$ then $X$ is \teethree\ .    
+
+    We show that if for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$ then $X$ is \teethree\ .
     \begin{subproof}
         Omitted.
     \end{subproof}
 \end{proof}
 
 
+\begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open}
+    Let $X$ be a topological space.
+    Suppose $X$ is inhabited.
+    $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$.    
+\end{proposition}
+\begin{proof}
+    Omitted.
+    %Follows by \cref{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods,teethree_implies_closed_neighbourhood_in_open}.
+\end{proof}
 
 
 \begin{proposition}\label{teethree_space_is_teetwo_space}
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 8da29d3..f8bcb93 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -1,5 +1,6 @@
 \import{set.tex}
 \import{set/powerset.tex}
+\import{set/cons.tex}
 
 \section{Topological spaces}
 
@@ -67,7 +68,8 @@
     such that $a\in U\subseteq A$.
 \end{proposition}
 \begin{proof}
-    Take $U\in\interiors{A}{X}$ such that $a\in U$.
+    Omitted.
+    %Take $U\in\interiors{A}{X}$ such that $a\in U$.
 \end{proof}
 
 \begin{proposition}[Interior]\label{interior_elem_iff}
@@ -175,6 +177,9 @@
     Suppose $B$ is closed in $X$.
     Then $A \setminus B$ is open in $X$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_eq_emptyset_iff_subseteq,is_closed_in,opens_inter,inter_comm_left,setminus_union,inter_assoc,inter_setminus,inter_lower_left,inter_lower_right,setminus_subseteq,double_complement,setminus_setminus,setminus_eq_inter_complement,setminus_self,setminus_inter,union_comm,emptyset_subseteq,setminus_partition}.
+\end{proof}
 
 \begin{definition}[Closed sets]\label{closeds}
     $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$.
@@ -297,7 +302,8 @@
 \end{proposition}
 \begin{proof}
     It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$.
-    If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$.
+    If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$ by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,elem_subseteq,setminus}.
+    Follows by \cref{subseteq_setminus_cons_elim,cons_absorb,double_complement_union,union_as_unions,set_is_subseteq_to_closure_of_the_set,setminus_subseteq,setminus_intro,closure,setminus_elim_left}.
 \end{proof}
 
 \begin{proposition}\label{complement_of_closed_is_open}
@@ -381,6 +387,7 @@
                     Take $U$ such that $U \in F$.
                     Let $F'' = F \setminus \{U\}$.
                     There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$.
+                    Omitted.
                 \caseOf{$\inters{F} \neq \emptyset$.}
                     
                     Fix $a \in \carrier[X] \setminus (\unions{F'})$.
@@ -389,7 +396,7 @@
                     $a \notin \unions{F'}$.
                     For all $A \in F'$ we have $a \notin A$.
                     For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$.
-                    For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$.
+                    For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$ by \cref{setminus_setminus,inter_absorb_supseteq_left,pow_iff,subseteq}.
                     For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$.
                     For all $Y \in F$ we have $a \in Y$.
                     Therefore $a \in \inters{F}$.
@@ -522,3 +529,7 @@
 \begin{definition}\label{neighbourhoods}
     $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$.
 \end{definition}
+
+\begin{definition}\label{neighbourhoods_set}
+    $\neighbourhoodsSet{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\subseteq U\subseteq N\}$.
+\end{definition}
-- 
cgit v1.2.3


From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 03:05:41 +0200
Subject: Abgabe

---
 library/algebra/group.tex                   |  2 +-
 library/algebra/monoid.tex                  |  2 +-
 library/cardinal.tex                        |  2 +-
 library/numbers.tex                         |  2 +-
 library/topology/basis.tex                  |  2 +-
 library/topology/continuous.tex             |  2 ++
 library/topology/metric-space.tex           |  4 ++--
 library/topology/real-topological-space.tex |  2 +-
 library/topology/separation.tex             |  2 ++
 library/topology/topological-space.tex      |  2 +-
 library/topology/urysohn.tex                |  4 ++--
 library/topology/urysohn2.tex               | 18 ++++++++++++++----
 12 files changed, 29 insertions(+), 15 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 7de1051..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index 06fcb50..3249a93 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -1,5 +1,5 @@
 \import{algebra/semigroup.tex}
-\section{Monoid}
+\section{Monoid}\label{form_sec_monoid}
 
 \begin{struct}\label{monoid}
     A monoid $A$ is a semigroup equipped with
diff --git a/library/cardinal.tex b/library/cardinal.tex
index 044e5d1..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,4 +1,4 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \import{set.tex}
 \import{ordinal.tex}
diff --git a/library/numbers.tex b/library/numbers.tex
index ac0a683..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,7 +4,7 @@
 \import{ordinal.tex}
 
 
-\section{The real numbers}
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 052c551..f0f77e4 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -2,7 +2,7 @@
 \import{set.tex}
 \import{set/powerset.tex}
 
-\subsection{Topological basis}
+\subsection{Topological basis}\label{form_sec_topobasis}
 
 \begin{abbreviation}\label{covers}
     $C$ covers $X$ iff
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index a9bc58e..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -3,6 +3,8 @@
 \import{function.tex}
 \import{set.tex}
 
+\subsection{Continuous}\label{form_sec_continuous}
+
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
 \end{definition}
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 0ed7bab..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,10 +4,10 @@
 \import{set/powerset.tex}
 \import{topology/basis.tex}
 
-\section{Metric Spaces}
+\section{Metric Spaces}\label{form_sec_metric}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index c76fd46..db7ee94 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{Topology Reals}
+\section{Topology Reals}\label{form_sec_toporeals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 0c68290..aaa3907 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,6 +1,8 @@
 \import{topology/topological-space.tex}
 \import{set.tex}
 
+\subsection{Separation}\label{form_sec_separation}
+
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
     $X$ is Kolmogorov iff
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index f8bcb93..409e107 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -2,7 +2,7 @@
 \import{set/powerset.tex}
 \import{set/cons.tex}
 
-\section{Topological spaces}
+\section{Topological spaces}\label{form_sec_topospaces}
 
 \begin{struct}\label{topological_space}
     A topological space $X$ is a onesorted structure equipped with
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ae03273..cd85fbc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,7 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
 %           In this section we want to proof Urysohns lemma. 
 %           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
 %           The Idea is to construct staircase functions as a chain.
@@ -22,7 +22,7 @@
 
 %Chains of  sets.
 
-The first tept will be a formalisation of chain constructions.
+This is the first attempt to prove Urysohns Lemma with the usage of struct. 
 
 \subsection{Chains of sets}
 %           Assume $A,B$ are subsets of a topological space $X$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 08841da..a1a3ba0 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,7 +15,7 @@
 \import{topology/real-topological-space.tex}
 \import{set/equinumerosity.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma}\label{form_sec_urysohn}
 
 
 
@@ -891,15 +891,25 @@
             \begin{byCase}
                 \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
                     Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
-                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                     Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
-                    Then $g(x) = 1$ .
+                    We show that $g(x) = 1$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                 \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
                     \begin{byCase}
                         \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
-                            $g(x) = \zero$.
+                            We show that $g(x) = \zero$.
+                            \begin{subproof}
+                                Omitted.
+                            \end{subproof}
                         \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
                             Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                            Omitted.
                     \end{byCase}
             \end{byCase}
 
-- 
cgit v1.2.3