[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

3 files changed, 103 insertions, 41 deletions

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}