working commit

2 files changed, 86 insertions, 22 deletions

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index d9790aa..b2e5ea9 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -382,7 +382,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             We have $a',b' \in \reals$ by assumption.
             We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}.
             Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$.
-            Then $x \in \epsBall{x'}{\epsilon'}$.
+            Then $x \in \epsBall{x'}{\epsilon'}$ by \cref{epsilon_ball}.
 
             Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
             %Then $(x_1 - \alpha) < (x_2 + \beta)$.
@@ -536,7 +536,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \begin{subproof}
             It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteLeft{a}$.
             Fix $x \in \unions{E}$.
-            Take $e \in E$ such that $x \in e$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $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$.
@@ -550,8 +550,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 Suppose not.
                 Take $y' \in e$ such that $y' > a$. 
                 $x'' < a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 Then $x'' < a < y'$.
                 Therefore $(x'' - \delta'') < a < (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_left,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq}.
                 Then $a \in e$ by \cref{epsball_are_connected_in_reals,intervalopen_infinite_left,neq_witness}.
@@ -565,7 +565,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             Trivial.
         \end{subproof}
     \end{subproof}
-    $\unions{E} \in \opens[\reals]$.
+    $\unions{E} \in \opens[\reals]$ by \cref{opens_unions,reals_is_topological_space,basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis,subset_transitive}.
 \end{proof}
 
 \begin{lemma}\label{continuous_on_basis_implies_continuous_endo}
@@ -600,7 +600,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \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$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $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$.
@@ -612,10 +612,10 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 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$. 
+                Take $y' \in e$ such that $y' < a$ by \cref{reals_order_total,intervalopen,eps_ball_implies_open_interval}. 
                 $x'' > a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 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}.
@@ -689,6 +689,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     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$.
+        Follows by \cref{union_intro_left,intervalopen_infinite_left,reals_order_total,reals_order_total2,union_iff,intervalopen_infinite_right,union_assoc,union_intro_right,intervalclosed}.
     \end{subproof}
 \end{proof}
 
@@ -697,7 +698,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     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}$.
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$ by \cref{intervalopen_infinite_left,union_intro_left,neq_witness,intervalclosed_infinite_right,union_intro_right,union_iff}.
     Trivial.
 \end{proof}
 
@@ -714,6 +715,9 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a \in \reals$.
     Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
 \end{lemma}
+\begin{proof}
+    Follows by \cref{reals_order_total,inter_lower_left,intervalopen_infinite_right,order_reals_lemma6,inter_lower_right,foundation,subseteq,intervalclosed_infinite_left}.
+\end{proof}
 
 \begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
     Suppose $a \in \reals$.
@@ -725,7 +729,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
 \end{proposition}
 \begin{proof}
-    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$.
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{intersection_of_open_closed__infinite_intervals_open_left,reals_as_union_of_open_closed_intervals2,setminus_inter,double_relative_complement,subseteq_union_setminus,subseteq_setminus,setminus_union,setminus_disjoint,setminus_partition,setminus_subseteq,setminus_emptyset,setminus_self,setminus_setminus,double_complement_union}.
 \end{proof}
 
 \begin{proposition}\label{closedinterval_infinite_left_in_closeds}
@@ -747,15 +751,17 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         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}$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{setminus,double_complement_union}.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$ by \cref{union_upper_left,subseteq,union_comm,subseteq_implies_setminus_supseteq}.
+            Follows by \cref{inter_intro}.
         \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})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ by \cref{setminus_setminus,setminus}.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$ by \cref{inter_lower_right,elem_subseteq,setminus_setminus}.
         \end{subproof}
+        Follows by \cref{setminus_union}.
     \end{subproof}
     We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
     \begin{subproof}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 83e3aa4..9990199 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -94,6 +94,9 @@
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{nat_is_transitiveset}.
+\end{proof}
 
 \begin{proposition}\label{naturals_elem_in_transitive}
     If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
@@ -119,6 +122,9 @@
 \begin{proposition}\label{zero_is_empty}
     There exists no $x$ such that $x \in \zero$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{notin_emptyset}.
+\end{proof}
 
 \begin{proposition}\label{one_is_positiv}
     $1$ is positiv.
@@ -163,6 +169,13 @@
     Omitted.
 \end{proof}
 
+\begin{proposition}\label{naturals_one_zero_or_greater}
+    For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}.
+\end{proof}
+
 \begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
     For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
 \end{proposition}
@@ -184,7 +197,7 @@
             \end{subproof}
         \caseOf{$n = 1$.}
             Fix $m$.
-            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
+            For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
             Then $\zero + 1 = 1$.
         \caseOf{$n > 1$.} 
             Take $l \in \naturals$ such that $\suc{l} = n$.
@@ -350,7 +363,7 @@
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
     Suppose $U$ is inhabited.
-    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
     Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
@@ -360,11 +373,36 @@
         \caseOf{$n \neq \zero$.}
             Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
             We have $\dom{U} \subseteq \naturals$.
-            $\dom{U}$ is inhabited.
+            $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}.
+            $\dom{U}$ has cardinality $\suc{k}$.
             We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             \begin{subproof}
-                Omitted.
+                For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+                We have $\dom{U} \subseteq \naturals$.
+                $\dom{U}$ is inhabited.
+                Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
+                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                \begin{subproof}
+                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                    \begin{subproof}
+                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                        Fix $y \in \seq{\emptyset}{k'}$.
+                        Then $y \leq k'$.
+                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
+                        Therefore $y \in \suc{k}$.
+                        Therefore $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                    \begin{subproof}
+                        Fix $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                \end{subproof}
             \end{subproof}
+            Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
             Define $V : N \to M$ such that $V(n)=
@@ -374,11 +412,31 @@
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                We show that $V$ is a chain of subsets in $X$.
+                \begin{subproof}
+                    It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}.
+                    It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $n \in \dom{V}$.
+                    Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                    It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                    Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                \end{subproof}
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V} \land n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
-            We show that $F$ is consistent on $U$ to $V$.
+            We show that $F$ is consistent on $V$ to $U$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}.
+                $F$ is a bijection from $\dom{V}$ to $\dom{U}$.
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
             $V$ is normal ordered.
     \end{byCase}