From 6129ebdf0d8549f3e4d23aa771f2c06020182b7e Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 7 Aug 2024 15:28:45 +0200
Subject: Created first urysohn formalization

---
 library/topology/continuous.tex | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

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

diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index 6a32353..a9bc58e 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -1,5 +1,7 @@
 \import{topology/topological-space.tex}
 \import{relation.tex}
+\import{function.tex}
+\import{set.tex}
 
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
@@ -8,18 +10,25 @@
 \begin{proposition}\label{continuous_definition_by_closeds}
     Let $X$ be a topological space.
     Let $Y$ be a topological space.
+    Let $f \in \funs{X}{Y}$.
     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}$.
+    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ 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}$.
+    %    We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    \begin{subproof}
+    %        It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$.
+    %        Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
+    %        Take $y \in \carrier[Y]$ such that $f(x)=y$.
+    %        It suffices to show that $y \in U$.
+    %    \end{subproof}
     %    $\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.
@@ -27,3 +36,4 @@
     %    Omitted.
     %\end{subproof}
 \end{proof}
+
-- 
cgit v1.2.3