[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

1 files changed, 29 insertions, 0 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}