From 3dca719ba8f9a59471f2c761cf8846cf597eae97 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 23:24:08 +0200
Subject: Topo Space Real Verfication

---
 library/topology/real-topological-space.tex | 200 +++++++++++++++++++++++++---
 1 file changed, 185 insertions(+), 15 deletions(-)

(limited to 'library/topology/real-topological-space.tex')

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index b3efa20..e5e17ef 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -580,28 +580,198 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$.
 \end{proposition}
 \begin{proof}
-    Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
-    Let $f(x) = \neg{x}$ for $x \in \reals$.
-    $f$ is a function from $\reals$ to $\reals$.
-    We show that $f$ is continuous.
+    Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteRight{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta}  \}$.
+    We show that for all $x \in \intervalopenInfiniteRight{a}$ we have there exists $e \in E$ such that $x \in e$.
     \begin{subproof}
-        It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
-        Fix $b \in \topoBasisReals$.
-        Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
-        Let $y = \neg{x}$.
-        It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
-        It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
-        Follows by set extensionality.
+        Fix $x \in \intervalopenInfiniteRight{a}$.
+        Then $a < x$.
+        Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$.
+        $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_right}.
+        $a \notin \epsBall{x}{\delta'}$.
+        $\epsBall{x}{\delta'} \in E$.
     \end{subproof}
-    $\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
-    We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    $E \subseteq \topoBasisReals$.
+    We show that $\unions{E} = \intervalopenInfiniteRight{a}$.
     \begin{subproof}
-        Omitted.
+        We show that $\unions{E} \subseteq \intervalopenInfiniteRight{a}$.
+        \begin{subproof}
+            It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$.
+            Fix $x \in \unions{E}$.
+            Take $e \in E$ such that $x \in e$.
+            $x \in \reals$.
+            Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
+            $\epsBall{x'}{\delta'} \in E$.
+            We show that for all $y \in e$ we have $y > a$.
+            \begin{subproof}
+                Fix $y \in e$.
+                Then $y \in \epsBall{x'}{\delta'}$.
+                $e = \epsBall{x'}{\delta'}$.
+                There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Suppose not.
+                Take $y' \in e$ such that $y' < a$. 
+                $x'' > a$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                Then $x'' > a > y'$.
+                Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}.
+                Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}.
+                Contradiction.
+            \end{subproof}
+            $x > a$.
+            Then $x \in \intervalopenInfiniteRight{a}$.
+        \end{subproof}
+        We show that $\intervalopenInfiniteRight{a} \subseteq \unions{E}$.
+        \begin{subproof}
+            Trivial.
+        \end{subproof}
     \end{subproof}
-    Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+    $\unions{E} \in \opens[\reals]$.
+
+    %Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
+    %Let $f(x) = \neg{x}$ for $x \in \reals$.
+    %$f$ is a function from $\reals$ to $\reals$.
+    %We show that $f$ is continuous.
+    %\begin{subproof}
+    %    It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
+    %    Fix $b \in \topoBasisReals$.
+    %    Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
+    %    Let $y = \neg{x}$.
+    %    It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
+    %    It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    $\preimg{f}{\epsBall{x}{\epsilon}} \subseteq \reals$.
+    %    $\epsBall{y}{\epsilon} \subseteq \reals$ by \cref{intervalopen,subseteq,minus,epsilon_ball}.
+    %    %It suffices to show that for all $x \in \reals$ we have $x \in \epsBall{y}{\epsilon}$ iff $x \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    %Fix $x \in \reals$.
+    %    Let $u = (y - \epsilon)$.
+    %    Let $v = (y + \epsilon)$.
+    %    $u = \neg{(x - \epsilon)}$.
+    %    $v = \neg{(x + \epsilon)}$.
+    %    %$v - u = \epsilon + \epsilon$.
+    %    We show that for all $z \in \epsBall{y}{\epsilon}$ we have $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    \begin{subproof}
+    %        Fix $z \in \epsBall{y}{\epsilon}$.
+    %        Then $u < z < v$.
+    %        Let $z' = z - u$.
+    %        Then $z = u + z'$.
+    %        Suppose not.
+    %        Let $h = \neg{z}$.
+    %        $\neg{h} = \neg{\neg{z}}$.
+    %        $\neg{h} = z$.
+    %        Then $f(h) = \neg{h}$.
+    %        $f(h) = z$.
+    %        Then $z \in \preimg{f}{\{h\}}$.
+%
+    %    \end{subproof}
+    %    We show that for all $z \in \preimg{f}{\epsBall{x}{\epsilon}}$ we have $z \in \epsBall{y}{\epsilon}$.
+    %    \begin{subproof}
+    %        Fix $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %        Take $h \in \epsBall{x}{\epsilon}$ such that $f(h) = z$.
+    %    \end{subproof}
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %$\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+    %We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+    %Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals1}
+    Suppose $a,b \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+\end{lemma}
+\begin{proof}
+    We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$.
+    \begin{subproof}
+        Fix $x \in \reals$.
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals2}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals3}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteRight{a} \union \intervalclosedInfiniteLeft{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalclosedInfiniteLeft{a}$ or $x \in \intervalopenInfiniteRight{a}$.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_right}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
+\end{lemma}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteLeft{a} \inter \intervalclosedInfiniteRight{a} = \emptyset$.
+\end{lemma}
+
+\begin{proposition}\label{closedinterval_infinite_right_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_infinite_left_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteLeft{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteLeft{a} = \reals \setminus \intervalopenInfiniteRight{a}$.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_eq_openintervals_setminus_reals}
+    Suppose $a,b \in \reals$.
+    Then $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$.
+\end{proposition}
+\begin{proof}
+    We have $\intervalclosed{a}{b} \subseteq \reals$.
+    We show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+    \begin{subproof}
+        We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$.
+        \end{subproof}
+        We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$.
+        \end{subproof}
+    \end{subproof}
+    We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
+    \begin{subproof}
+        For all $x \in \intervalclosedInfiniteRight{a}$ we have $x \geq a$.
+        For all $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ we have $x \geq a$.
+        Follows by set extensionality.
+    \end{subproof}
+    $\reals \setminus \intervalopenInfiniteRight{b} = \intervalclosedInfiniteLeft{b}$.
+    It suffices to show that $\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a} = \intervalclosed{a}{b}$.
+    For all $x \in \intervalclosed{a}{b}$ we have $a \leq x \leq b$.
+    For all $x \in (\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a})$ we have $a \leq x \leq b$.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{closedinterval_is_closed}
     Suppose $a,b \in \reals$.
     Then $\intervalclosed{a}{b} \in \closeds{\reals}$.
 \end{proposition}
+\begin{proof}
+    We have $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+    It suffices to show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$ by \cref{closeds,setminus_subseteq,powerset_intro,closed_minus_open_is_closed,opens_type,subseteq_refl,union_open,is_closed_in,reals_carrier_reals,setminus_self,emptyset_open,reals_is_topological_space,openinterval_infinite_left_in_opens,openinterval_infinite_right_in_opens}.
+\end{proof}
-- 
cgit v1.2.3

