From 050b56baf7a158bff0eb721e03263b121bdc23c3 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 4 Jun 2024 11:19:21 +0200
Subject: Some notation fixes and lemma for topo basis generats opens was
 proofed and optimizised

---
 library/topology/basis.tex | 51 ++++++++++++++++++++++++++++++++++------------
 1 file changed, 38 insertions(+), 13 deletions(-)

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

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 6fa9fbd..bd7d15a 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -56,24 +56,52 @@
     $\emptyset \in \genOpens{B}{X}$.
 \end{lemma}
 
-\begin{lemma}\label{all_is_in_genopens}
+
+
+\begin{lemma}\label{union_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    $X \in \genOpens{B}{X}$.
+    Assume $F\subseteq \genOpens{B}{X}$.
+    Then $\unions{F}\in\genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
-    $\unions{B} \in \genOpens{B}{X}$.
-    $X \subseteq \unions{B}$.
+    We have $\unions{F} \in \pow{X}$.
+
+    Show for all $x\in \unions{F}$ there exists $W \in B$
+    such that $x\in W$ and $W \subseteq \unions{F}$.
+    \begin{subproof}
+        Fix $x \in \unions{F}$.
+        There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}.
+        $V \in \genOpens{B}{X}$.
+        There exists $W \in B$ such that $x \in W \subseteq V$.
+        Then $W \subseteq \unions{F}$.
+    \end{subproof}
+    Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}.
 \end{proof}
 
-\begin{lemma}\label{union_in_genopens}
+\begin{lemma}\label{basis_is_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$.
+    $B \subseteq \genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    Omitted.
+    We show for all $V \in B$ $V \in \genOpens{B}{X}$.
+    \begin{subproof}
+        Fix $V \in B$.
+        For all $x \in V$ $x \in V \subseteq V$.
+        $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+        $V \in \pow{X}$.
+        $V \in \genOpens{B}{X}$.
+    \end{subproof}
 \end{proof}
 
+\begin{lemma}\label{all_is_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    $X \in \genOpens{B}{X}$.
+\end{lemma}
+\begin{proof}
+    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+    $\unions{B} \in \genOpens{B}{X}$.
+    $X \subseteq \unions{B}$.
+\end{proof}
 
 \begin{lemma}\label{inters_in_genopens}
     Assume $B$ is a topological basis for $X$.
@@ -92,16 +120,13 @@
         Then $x\in A,C$.
         There exists $V'  \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}.
         There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}.
-        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
+        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$ by \cref{topological_basis}.
 
         Show $W \subseteq (A\inter C)$.
         \begin{subproof}
-            %$W \subseteq v'$ and $W \subseteq V''$.
             For all $y \in W$ we have $y \in V'$ and $y \in V''$.
         \end{subproof}
     \end{subproof}
-    %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
-    %such that $x\in W$ and $W \subseteq (A\inter C)$.
 
-    $(A\inter C) \in \genOpens{B}{X}$.
+    $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}.
 \end{proof}
-- 
cgit v1.2.3


From 44d4c1c50ba6e0f12a2f4fdd204b315a15e434db Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 25 Jun 2024 00:02:44 +0200
Subject: Improvement for the ATP proof time

---
 library/set.tex            | 3 +++
 library/topology/basis.tex | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

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

diff --git a/library/set.tex b/library/set.tex
index 2fd18ea..69b9526 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -654,6 +654,9 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Suppose $(A\inter B)\union C = A\inter (B\union C)$.
     Then $C\subseteq A$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{union_upper_right,union_upper_left,subseteq_union_iff,subseteq_antisymmetric,subseteq_inter_iff}.
+\end{proof}
 
 % From Isabelle/ZF equalities theory
 \begin{proposition}\label{union_inter_crazy}
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index bd7d15a..052c551 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -64,7 +64,7 @@
     Then $\unions{F}\in\genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    We have $\unions{F} \in \pow{X}$.
+    We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}.
 
     Show for all $x\in \unions{F}$ there exists $W \in B$
     such that $x\in W$ and $W \subseteq \unions{F}$.
-- 
cgit v1.2.3


From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 03:05:41 +0200
Subject: Abgabe

---
 library/algebra/group.tex                   |  2 +-
 library/algebra/monoid.tex                  |  2 +-
 library/cardinal.tex                        |  2 +-
 library/numbers.tex                         |  2 +-
 library/topology/basis.tex                  |  2 +-
 library/topology/continuous.tex             |  2 ++
 library/topology/metric-space.tex           |  4 ++--
 library/topology/real-topological-space.tex |  2 +-
 library/topology/separation.tex             |  2 ++
 library/topology/topological-space.tex      |  2 +-
 library/topology/urysohn.tex                |  4 ++--
 library/topology/urysohn2.tex               | 18 ++++++++++++++----
 12 files changed, 29 insertions(+), 15 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 7de1051..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index 06fcb50..3249a93 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -1,5 +1,5 @@
 \import{algebra/semigroup.tex}
-\section{Monoid}
+\section{Monoid}\label{form_sec_monoid}
 
 \begin{struct}\label{monoid}
     A monoid $A$ is a semigroup equipped with
diff --git a/library/cardinal.tex b/library/cardinal.tex
index 044e5d1..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,4 +1,4 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \import{set.tex}
 \import{ordinal.tex}
diff --git a/library/numbers.tex b/library/numbers.tex
index ac0a683..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,7 +4,7 @@
 \import{ordinal.tex}
 
 
-\section{The real numbers}
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 052c551..f0f77e4 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -2,7 +2,7 @@
 \import{set.tex}
 \import{set/powerset.tex}
 
-\subsection{Topological basis}
+\subsection{Topological basis}\label{form_sec_topobasis}
 
 \begin{abbreviation}\label{covers}
     $C$ covers $X$ iff
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index a9bc58e..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -3,6 +3,8 @@
 \import{function.tex}
 \import{set.tex}
 
+\subsection{Continuous}\label{form_sec_continuous}
+
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
 \end{definition}
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 0ed7bab..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,10 +4,10 @@
 \import{set/powerset.tex}
 \import{topology/basis.tex}
 
-\section{Metric Spaces}
+\section{Metric Spaces}\label{form_sec_metric}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index c76fd46..db7ee94 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{Topology Reals}
+\section{Topology Reals}\label{form_sec_toporeals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 0c68290..aaa3907 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,6 +1,8 @@
 \import{topology/topological-space.tex}
 \import{set.tex}
 
+\subsection{Separation}\label{form_sec_separation}
+
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
     $X$ is Kolmogorov iff
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index f8bcb93..409e107 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -2,7 +2,7 @@
 \import{set/powerset.tex}
 \import{set/cons.tex}
 
-\section{Topological spaces}
+\section{Topological spaces}\label{form_sec_topospaces}
 
 \begin{struct}\label{topological_space}
     A topological space $X$ is a onesorted structure equipped with
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ae03273..cd85fbc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,7 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
 %           In this section we want to proof Urysohns lemma. 
 %           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
 %           The Idea is to construct staircase functions as a chain.
@@ -22,7 +22,7 @@
 
 %Chains of  sets.
 
-The first tept will be a formalisation of chain constructions.
+This is the first attempt to prove Urysohns Lemma with the usage of struct. 
 
 \subsection{Chains of sets}
 %           Assume $A,B$ are subsets of a topological space $X$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 08841da..a1a3ba0 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,7 +15,7 @@
 \import{topology/real-topological-space.tex}
 \import{set/equinumerosity.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma}\label{form_sec_urysohn}
 
 
 
@@ -891,15 +891,25 @@
             \begin{byCase}
                 \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
                     Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
-                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                     Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
-                    Then $g(x) = 1$ .
+                    We show that $g(x) = 1$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                 \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
                     \begin{byCase}
                         \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
-                            $g(x) = \zero$.
+                            We show that $g(x) = \zero$.
+                            \begin{subproof}
+                                Omitted.
+                            \end{subproof}
                         \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
                             Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                            Omitted.
                     \end{byCase}
             \end{byCase}
 
-- 
cgit v1.2.3

