From 3d6ce5e9d5e63a5e5ed833516c62ad056e506775 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 4 Jun 2024 15:29:13 +0200
Subject: Proof of teeone_implies_singletons_closed

The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing.
---
 library/topology/separation.tex | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

(limited to 'library/topology/separation.tex')

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index f70cb50..f055495 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -73,10 +73,39 @@
 
 \begin{proposition}\label{teeone_implies_singletons_closed}
     Let $X$ be a \teeone-space.
-    Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$.
+    Assume $x \in \carrier[X]$.
+    Then $\{x\}$ is closed in $X$.
+    %Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. Ambigus Phrase. if Omitted is ereased.
 \end{proposition}
 \begin{proof}
-    Omitted.
+    %Omitted.
+    %Fix $x \in X$.
+    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}
+
+
+
+
+    % 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]$.
+
     % TODO
     % Choose for every y distinct from x and open subset U_y containing y but not x.
     % The union U of all the U_y is open.
-- 
cgit v1.2.3


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/topology/separation.tex')

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


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/separation.tex        |  10 ---
 library/topology/topological-space.tex | 136 ++++++++++++++++++++++++++++++++-
 2 files changed, 135 insertions(+), 11 deletions(-)

(limited to 'library/topology/separation.tex')

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 530a51f..535a51f 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -75,11 +75,8 @@
     Let $X$ be a \teeone-space.
     Assume $x \in \carrier[X]$.
     Then $\{x\}$ is closed in $X$.
-    %Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. Ambigus Phrase. if Omitted is ereased.
 \end{proposition}
 \begin{proof}
-    %Omitted.
-    %Fix $x \in X$.
     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$.
@@ -99,13 +96,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]$.
-
-    % TODO
-    % Choose for every y distinct from x and open subset U_y containing y but not x.
-    % The union U of all the U_y is open.
-    % {x} is the complement of U in \carrier[X].
 \end{proof}
 %
 % Conversely, if \{x\} is open, then for any y distinct from x we can use
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 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/separation.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 6839f79e775d8ffa36d421f4e3c08528323eaf17 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 20 Jun 2024 12:59:41 +0200
Subject: [Report] Task failed and was proven in the same time.

The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following:

time stack exec zf -- --log library/topology/separation.tex -t 30  --dump ./dump
[Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)).
[Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU).
[Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))).
[Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))).
[Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).
[Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))).
[Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)).
[Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))).
[Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))).
Verification failed: prover found countermodel
fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))).
fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))).
fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)).
fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))).
fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)).
fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)).
fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))).
fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)).
fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)).
fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)).

real    0m14.914s
user    0m37.867s
sys     0m1.956s
---
 library/topology/separation.tex | 101 +++++++++++++++++++++++++++++++++-------
 1 file changed, 85 insertions(+), 16 deletions(-)

(limited to 'library/topology/separation.tex')

diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 3268bb9..c53b6a8 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,5 +1,5 @@
 \import{topology/topological-space.tex}
-
+\import{set.tex}
 
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
@@ -146,28 +146,65 @@
     \end{subproof}
 \end{proof}
 
-\begin{definition}\label{regular}
+\begin{definition}\label{is_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}
+\begin{abbreviation}\label{regular_space}
     $X$ is a regular space iff $X$ is a topological space and $X$ is regular.
-\end{definition}
+\end{abbreviation}
 
 
-\begin{definition}\label{teethree}
+\begin{abbreviation}\label{teethree}
     $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ .
-\end{definition}
+\end{abbreviation}
 
-\begin{definition}\label{teethree_space}
+\begin{abbreviation}\label{teethree_space}
     $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ .
-\end{definition}
+\end{abbreviation}
+
+\begin{proposition}\label{eqvilance_teethree_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}
+
+    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{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}$.
+    \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\ .    
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+\end{proof}
+
+
+
 
 \begin{proposition}\label{teethree_space_is_teetwo_space}
     Let $X$ be a \teethree-space.
+    Suppose $X$ is inhabited.
     Then $X$ is a \teetwo-space.
 \end{proposition}
 \begin{proof}
+    Omitted.
+\end{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$.
@@ -175,16 +212,48 @@
     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.
+        There exist $C' \in \closeds{X}$ such that $x \in \carrier[X]$ and $x \notin C' \in \closeds{X}$ and there exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$.
+        There exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$.
+        $U'$ is disjoint from $V'$.
+        $x \in U'$.
+        $x \notin C' \subseteq V'$.
+        $U',V' \in \opens[X]$.
+        $C' \in \closeds{X}$.
+        We show that there exist $K \in \closeds{X}$ such that $x \notin K \ni y$.
+        \begin{subproof}
+            $X$ is Kolmogorov.
+            For all $x',y'\in\carrier[X]$ such that $x'\neq y'$ there exist $H\in\opens[X]$ such that $x'\in H\not\ni y'$ or $x'\notin H\ni y'$.
+            we show that there exist $H \in \opens[X]$ such that $x \notin H \ni y$ or $y \notin H \ni x$.
+            \begin{subproof}
+                Omitted.
+            \end{subproof}
+            $H \subseteq \carrier[X]$ by \cref{opens_type,subseteq}.
+            Since $\carrier[X] \ni x \notin H$ or $\carrier[X] \ni y \notin H$, we have there exist $c \in H$. 
+            Then $H \neq \carrier[X]$.
+            Since $y \in H$ or $x \in H$, we have $H \neq \emptyset$.
+            Let $K = \carrier[X] \setminus H$.
+            $K$ is inhabited.
+            $K \in \closeds{X}$ by \cref{complement_of_open_is_closed}.
+            $x \notin K \ni y$ or $y \notin K \ni x$.
+            \begin{byCase}
+                \caseOf{$y \in K$.} Trivial.
+                \caseOf{$y \notin K$.}
+                Then there exist $U'',V'' \in \opens[X]$ such that $x \in U''$ and $K \subseteq V''$ and $U'' \inter V'' = \emptyset$ by \cref{is_regular}.
+                Let $K' = \carrier[X] \setminus U''$.
+                $x \in K'$.
+                $K' \in \closeds{X}$.
+            \end{byCase}
+
+
+        \end{subproof}
+
+        Follows by assumption.
     \end{subproof}
-    $y \in V$.
+    $y \in V$ by assumption.
     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
+    
+%\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/separation.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/separation.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

