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/metric-space.tex | 77 --------------------------------------- 1 file changed, 77 deletions(-) (limited to 'library/topology/metric-space.tex') diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 1c6a0ca..bcc5b8c 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -21,44 +21,16 @@ -%\begin{definition}\label{induced_topology} -% $O$ is the induced topology of $d$ in $M$ iff -% $O \subseteq \pow{M}$ and -% $d$ is a metric on $M$ and -% for all $x,r,A,B,C$ -% such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$ -% we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$. -%\end{definition} - -%\begin{definition} -% $\projcetfirst{A} = \{a \mid \exists x \in X \text{there exist $x \i } \}$ -%\end{definition} - \begin{definition}\label{set_of_balls} $\balls{d}{M} = \{ O \in \pow{M} \mid \text{there exists $x,r$ such that $r \in \reals$ and $x \in M$ and $O = \openball{r}{x}{d}$ } \}$. \end{definition} -%\begin{definition}\label{toindsas} -% $\metricopens{d}{M} = \{O \in \pow{M} \mid \text{ -% $d$ is a metric on $M$ and -% for all $x,r,A,B,C$ -% such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$ -% we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$. -% } \}$. -% -%\end{definition} - \begin{definition}\label{metricopens} $\metricopens{d}{M} = \genOpens{\balls{d}{M}}{M}$. \end{definition} -\begin{theorem} - Let $d$ be a metric on $M$. - $M$ is a topological space. -\end{theorem} - @@ -93,13 +65,6 @@ \end{lemma} -%\begin{definition}\label{lenght_of_interval} %TODO: take minus if its implemented -% $\lenghtinterval{x}{y} = r$ -%\end{definition} - - - - \begin{lemma}\label{metric_implies_topology} @@ -108,45 +73,3 @@ \end{lemma} - - - -%\begin{struct}\label{metric_space} -% A metric space $M$ is a onesorted structure equipped with -% \begin{enumerate} -% \item $\metric$ -% \end{enumerate} -% such that -% \begin{enumerate} -% \item \label{metric_space_d} $\metric[M]$ is a function from $M \times M$ to $\reals$. -% \item \label{metric_space_distence_of_a_point} $\metric[M](x,x) = \zero$. -% \item \label{metric_space_positiv} for all $x,y \in M$ if $x \neq y$ then $\zero < \metric[M](x,y)$. -% \item \label{metric_space_symetrie} $\metric[M](x,y) = \metric[M](y,x)$. -% \item \label{metric_space_triangle_equation} for all $x,y,z \in M$ $\metric[M](x,y) < \metric[M](x,z) + \metric[M](z,y)$ or $\metric[M](x,y) = \metric[M](x,z) + \metric[M](z,y)$. -% \item \label{metric_space_topology} $M$ is a topological space. -% \item \label{metric_space_opens} for all $x \in M$ for all $r \in \reals$ $\{z \in M \mid \metric[M](x,z) < r\} \in \opens$. -% \end{enumerate} -%\end{struct} - -%\begin{definition}\label{open_ball} -% $\openball{r}{x}{M} = \{z \in M \mid \metric(x,z) < r\}$. -%\end{definition} - -%\begin{proposition}\label{open_ball_is_open} -% Let $M$ be a metric space,let $r \in \reals $, let $x$ be an element of $M$. -% Then $\openball{r}{x}{M} \in \opens[M]$. -%\end{proposition} - - - - - - -%TODO: - Basis indudiert topology lemma -% - Offe Bälle sind basis - -% Was danach kommen soll bleibt offen, vll buch oder in proof wiki -% Trennungsaxiom, - -% Notaionen aufräumen damit das gut gemercht werden kann. - -- cgit v1.2.3 From b298295ac002785672a8b16dd09f9692d73f7a80 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sun, 15 Sep 2024 15:07:36 +0200 Subject: Issue at Fixing. In Line 49 in real-topological-space.tex the Fix can't be processed. --- library/numbers.tex | 19 ++++++++ library/topology/metric-space.tex | 2 +- library/topology/real-topological-space.tex | 73 +++++++++++++++++++++++++++-- library/topology/urysohn2.tex | 73 ++++++++++++++++++++++++----- 4 files changed, 149 insertions(+), 18 deletions(-) (limited to 'library/topology/metric-space.tex') diff --git a/library/numbers.tex b/library/numbers.tex index cb3d5cf..b7de307 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -245,12 +245,31 @@ Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$. \end{proposition} +%\begin{proposition}\label{natural_disstro_oneline} +% Suppose $n,m,k \in \naturals$. +% Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. +%\end{proposition} +%\begin{proof} +% Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. +% $\zero \in P$. +% $P \subseteq \naturals$. +% It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. +% Fix $n \in P$. +% It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +% Fix $m' \in \naturals$. +% Fix $k' \in \naturals$. +% $n \in \naturals$. +% $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + m' + k' = (((n \rmul m') + (n \rmul k')) + m') + k' = (m' + ((n \rmul m') + (n \rmul k'))) + k' = ((m' + (n \rmul m')) + (n \rmul k')) + k' = (((n \rmul m') + m') + (n \rmul k')) + k' = ((n \rmul m') + m') + ((n \rmul k') + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +%\end{proof} + \begin{proposition}\label{natural_disstro} Suppose $n,m,k \in \naturals$. Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. \end{proposition} \begin{proof} + %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$. + $\zero \in P$. $P \subseteq \naturals$. It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index bcc5b8c..0ed7bab 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -7,7 +7,7 @@ \section{Metric Spaces} \begin{definition}\label{metric} - $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and + $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ 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 239965c..db46732 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -17,10 +17,73 @@ $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. \end{definition} -\begin{theorem}\label{reals_as_topo_space} - Suppose $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$. - Then $\reals$ is a topological space. +\begin{axiom}\label{reals_carrier_reals} + $\carrier[\reals] = \reals$. +\end{axiom} + +\begin{theorem}\label{topological_basis_reals_is_prebasis} + $\topoBasisReals$ is a topological prebasis for $\reals$. \end{theorem} \begin{proof} - Omitted. -\end{proof} \ No newline at end of file + We show that $\unions{\topoBasisReals} \subseteq \reals$. + \begin{subproof} + It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$. + Fix $x \in \unions{\topoBasisReals}$. + \end{subproof} + We show that $\reals \subseteq \unions{\topoBasisReals}$. + \begin{subproof} + It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$. + Fix $x \in \reals$. + \end{subproof} +\end{proof} + +\begin{theorem}\label{topological_basis_reals_is_basis} + $\topoBasisReals$ is a topological basis for $\reals$. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}. + Let $B = \topoBasisReals$. + It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$. + Fix $U \in B$. + Fix $V \in B$. + Fix $x \in U, V$. +\end{proof} + +\begin{axiom}\label{topological_space_reals} + $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$. +\end{axiom} + +\begin{theorem}\label{reals_is_topological_space} + $\reals$ is a topological space. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological basis for $\reals$. + Let $B = \topoBasisReals$. + We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$. + \begin{subproof} + It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$. + Fix $A \in \opens[\reals]$. + Follows by \cref{powerset_elim,topological_space_reals,genopens}. + \end{subproof} + We show that $\reals \in\opens[\reals]$. + \begin{subproof} + $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $\unions{B} \in \genOpens{B}{\reals}$. + $\reals \subseteq \unions{B}$. + \end{subproof} + We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,inters_in_genopens}. + \end{subproof} + We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,union_in_genopens}. + \end{subproof} + $\carrier[\reals] = \reals$. + Follows by \cref{topological_space}. +\end{proof} + +\begin{proposition}\label{open_interval_is_open} + Suppose $a,b \in \reals$. + Then $\intervalopen{a}{b} \in \opens[\reals]$. +\end{proposition} \ No newline at end of file diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 396255e..838b121 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -152,16 +152,23 @@ \begin{proposition}\label{no_natural_between_n_and_suc_n} For all $n,m \in \naturals$ we have not $n < m < \suc{n}$. \end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_is_zero_one_or_greater} + $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$. +\end{proposition} +\begin{proof} + Omitted. +\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} \begin{proof}[Proof by \in-induction on $n$] Assume $n \in \naturals$. - We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$. - \begin{subproof} - Trivial. - \end{subproof} + \begin{byCase} \caseOf{$n = \zero$.} @@ -196,9 +203,17 @@ We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$. \begin{subproof}[Proof by \in-induction on $m$] Assume $m \in \naturals$. - %\begin{byCase} - % - %\end{byCase} + \begin{byCase} + \caseOf{$\suc{m}=n$.} + \caseOf{$\suc{m}\neq n$.} + \begin{byCase} + \caseOf{$n = \zero$.} + \caseOf{$n \neq \zero$.} + Take $l \in \naturals$ such that $\suc{l} = n$. + Omitted. + + \end{byCase} + \end{byCase} \end{subproof} \end{subproof} @@ -323,17 +338,51 @@ For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$. \end{proposition} +\begin{proposition}\label{bijection_naturals_order} + 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)$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + \begin{proposition}\label{existence_normal_ordered_urysohn} Let $X$ be a urysohn space. Suppose $U$ is a urysohnchain of $X$. Suppose $\dom{U}$ is finite. - Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered. + 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. \end{proposition} \begin{proof} - Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}. - There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$. - - + Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}. + \begin{byCase} + \caseOf{$n = \zero$.} + Omitted. + \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. + 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. + \end{subproof} + Let $N = \seq{\zero}{k}$. + Let $M = \pow{X}$. + Define $V : N \to M$ such that $V(n)=$ + \begin{cases} + &\at{U}{F(n)} & \text{if} n \in N + \end{cases} + $\dom{V} = \seq{\zero}{k}$. + We show that $V$ is a urysohnchain of $X$. + \begin{subproof} + Trivial. + \end{subproof} + We show that $F$ is consistent on $U$ to $V$. + \begin{subproof} + Trivial. + \end{subproof} + $V$ is normal ordered. + \end{byCase} + \end{proof} -- 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/metric-space.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