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 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 library/topology/continuous.tex

(limited to 'library/topology/continuous.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}
-- 
cgit v1.2.3