From 3795588d157864a411baf2fc3afb31f9f5184d93 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 7 May 2024 14:41:15 +0200 Subject: Formalization of metric spaces and some cleaning of numbers.tex Formalization of metric spaces: Therefore we introduced the predicate metric and its axiomatization. Then we introduced the term metric space in dependence of a metric function. This metric space is automatically a a topological space. --- library/topology/metric-space.tex | 80 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) create mode 100644 library/topology/metric-space.tex (limited to 'library/topology/metric-space.tex') diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex new file mode 100644 index 0000000..7021a60 --- /dev/null +++ b/library/topology/metric-space.tex @@ -0,0 +1,80 @@ +\import{topology/topological-space.tex} +\import{numbers.tex} +\import{function.tex} + +\section{Metric Spaces} + +\begin{abbreviation}\label{metric} + $f$ is a metric iff $f$ is a function to $\reals$. +\end{abbreviation} + +\begin{axiom}\label{metric_axioms} + $f$ is a metric iff $\dom{f} = A \times A$ and + for all $x,y,z \in A$ we have + $f(x,x) = \zero$ and + $f(x,y) = f(y,x)$ and + $f(x,y) \leq f(x,z) + f(z,y)$ and + if $x \neq y$ then $\zero < f(x,y)$. +\end{axiom} + +\begin{definition}\label{open_ball} + $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric and $\dom{f} = M \times M$ and $f(x,z) Date: Tue, 7 May 2024 18:08:04 +0200 Subject: formalisation mertic optimized --- library/numbers.tex | 18 ++++++++++------- library/topology/metric-space.tex | 41 ++++++++++++++++++++++++++------------- 2 files changed, 38 insertions(+), 21 deletions(-) (limited to 'library/topology/metric-space.tex') diff --git a/library/numbers.tex b/library/numbers.tex index df47d81..a0e2211 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -10,7 +10,7 @@ %\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher %\cdot für multiklikation verwenden. %< für die relation benutzen. - +% sup und inf einfügen \begin{signature} $\reals$ is a set. @@ -92,7 +92,7 @@ \begin{axiom}\label{reals_axiom_mul_invers} - For all $x \in \reals$ there exist $y \in \reals$ such that $x \neq \zero$ and $x \times y = 1$. + For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$. \end{axiom} \begin{axiom}\label{reals_axiom_disstro1} @@ -107,7 +107,10 @@ For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{proposition} - +\begin{axiom}\label{reals_axiom_dedekind_complete} + For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$ + such that $x < z < y$. +\end{axiom} \begin{lemma}\label{order_reals_lemma1} @@ -129,14 +132,15 @@ then $(x \times z) < (x \times y)$. \end{lemma} -\begin{lemma}\label{a} +\begin{lemma}\label{o4rder_reals_lemma} For all $x,y \in \reals$ if $x > y$ then $x \geq y$. \end{lemma} -\begin{lemma}\label{aa} +\begin{lemma}\label{order_reals_lemma5} For all $x,y \in \reals$ if $x < y$ then $x \leq y$. \end{lemma} -\begin{lemma}\label{aaa} +\begin{lemma}\label{order_reals_lemma6} For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. -\end{lemma} \ No newline at end of file +\end{lemma} + diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 7021a60..2a31d95 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -4,23 +4,22 @@ \section{Metric Spaces} -\begin{abbreviation}\label{metric} - $f$ is a metric iff $f$ is a function to $\reals$. -\end{abbreviation} - -\begin{axiom}\label{metric_axioms} - $f$ is a metric iff $\dom{f} = A \times A$ and - for all $x,y,z \in A$ we have +\begin{definition}\label{metric} + $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 $f(x,y) \leq f(x,z) + f(z,y)$ and if $x \neq y$ then $\zero < f(x,y)$. -\end{axiom} +\end{definition} \begin{definition}\label{open_ball} - $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric and $\dom{f} = M \times M$ and $f(x,z) Date: Tue, 14 May 2024 16:55:40 +0200 Subject: work on metric spaces --- library/numbers.tex | 49 +++++++++++++++++++++++++++++++++++++++ library/topology/metric-space.tex | 45 +++++++++++++++++++++++++++++++++-- 2 files changed, 92 insertions(+), 2 deletions(-) (limited to 'library/topology/metric-space.tex') diff --git a/library/numbers.tex b/library/numbers.tex index a0e2211..5dd06da 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -144,3 +144,52 @@ For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. \end{lemma} +\begin{axiom}\label{reals_axiom_minus} + For all $x \in \reals$ $x - x = \zero$. +\end{axiom} + +\begin{lemma}\label{reals_minus} + Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$. +\end{lemma} + +%\begin{definition}\label{reasl_supremum} %expaction "there exists" after \mid +% $\rsup{X} = \{z \mid \text{ $z \in \reals$ and for all $x,y$ such that $x \in X$ and $y,x \in \reals$ and $x < y$ we have $z \leq y$ }\}$. +%\end{definition} + +\begin{definition}\label{upper_bound} + $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$. +\end{definition} + +\begin{definition}\label{least_upper_bound} + $x$ is a least upper bound of $X$ iff $x$ is an upper bound of $X$ and for all $y$ such that $y$ is an upper bound of $X$ we have $x \leq y$. +\end{definition} + +\begin{lemma}\label{supremum_unique} + %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$. + If $x$ is a least upper bound of $X$ and $y$ is a least upper bound of $X$ then $x = y$. +\end{lemma} + +\begin{definition}\label{supremum_reals} + $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$. +\end{definition} + + + + +\begin{definition}\label{lower_bound} + $x$ is an lower bound of $X$ iff for all $y \in X$ we have $x < y$. +\end{definition} + +\begin{definition}\label{greatest_lower_bound} + $x$ is a greatest lower bound of $X$ iff $x$ is an lower bound of $X$ and for all $y$ such that $y$ is an lower bound of $X$ we have $x \geq y$. +\end{definition} + +\begin{lemma}\label{infimum_unique} + %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$. + If $x$ is a greatest lower bound of $X$ and $y$ is a greatest lower bound of $X$ then $x = y$. +\end{lemma} + +\begin{definition}\label{infimum_reals} + $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$. +\end{definition} + diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 2a31d95..8ec83f7 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -1,6 +1,7 @@ \import{topology/topological-space.tex} \import{numbers.tex} \import{function.tex} +\import{set/powerset.tex} \section{Metric Spaces} @@ -17,7 +18,46 @@ $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric on $M$ and $f(x,z) < r$ } \}$. \end{definition} -%TODO: \metric_opens{d} = {hier die construction für topology} + + +\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$ we have $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{theorem}\label{metric_induce_a_topology} + + + +\end{theorem} + + + + +%TODO: \metric_opens{d} = {hier die construction für topology} DONE. %TODO: Die induzierte topology definieren und dann in struct verwenden. @@ -44,7 +84,7 @@ \begin{lemma}\label{union_of_open_balls_is_open} Let $M$ be a metric space. - For all $U,V \subseteq M$ if $U$ is an open ball in $M$ and $V$ is an open ball in $M$ then $U \union V$ is open in $M$. + For all $U,V \subseteq M$ if $U$, $V$ are open balls in $M$ then $U \union V$ is open in $M$. \end{lemma} @@ -56,6 +96,7 @@ + \begin{lemma}\label{metric_implies_topology} Let $M$ be a set, and let $f$ be a metric on $M$. Then $M$ is a metric space. -- cgit v1.2.3 From ecfb1a66f2159e078199e54edf8a80004c28195a Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 28 May 2024 15:33:45 +0200 Subject: proofing some lammes about topological basis --- .gitignore | 2 ++ library/topology/basis.tex | 75 +++++++++++++++++++++++++++++++++++++-- library/topology/metric-space.tex | 60 ++++++++++++++++++++----------- 3 files changed, 113 insertions(+), 24 deletions(-) (limited to 'library/topology/metric-space.tex') diff --git a/.gitignore b/.gitignore index ddb98c3..49c3120 100644 --- a/.gitignore +++ b/.gitignore @@ -42,3 +42,5 @@ haddocks/ stack.yaml.lock zf*.svg Anmerkungen.txt +vampire-taks-with-not-expacted-behavoir/ + diff --git a/library/topology/basis.tex b/library/topology/basis.tex index bca42f0..61a358f 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -1,4 +1,6 @@ \import{topology/topological-space.tex} +\import{set.tex} +\import{set/powerset.tex} \subsection{Topological basis} @@ -44,7 +46,74 @@ there exists $W\in B$ such that $x\in W\subseteq U, V$. \end{definition} -\begin{definition}\label{genOpens} - $\genOpens{B}{X} = \{ U\in\pow{X} \mid for all $x\in U$ there exists $V\in B$ - such that $x\in V\subseteq U$\}$. +\begin{definition}\label{genopens} + $\genOpens{B}{X} = \{ U\in\pow{X} \mid \text{for all $x\in U$ there exists $V\in B$ + such that $x\in V\subseteq U$} \}$. \end{definition} + +\begin{lemma}\label{emptyset_in_genopens} + Assume $B$ is a topological basis for $X$. + $\emptyset \in \genOpens{B}{X}$. +\end{lemma} + +\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{union_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}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + + +\begin{lemma}\label{inters_in_genopens} + Assume $B$ is a topological basis for $X$. + %For all $A, C$ + If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$. +\end{lemma} +\begin{proof} + + Show $(A \inter C) \in \pow{X}$. + \begin{subproof} + $(A \inter C) \subseteq X$ by assumption. + \end{subproof} + Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$. + + + Show for all $x\in (A\inter C)$ there exists $W \in B$ + such that $x\in W$ and $W \subseteq (A\inter C)$. + \begin{subproof} + Fix $x \in (A\inter C)$. + There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption. %TODO: Warum muss hier by assumtion hin? + There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption. + There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption. + + 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''$ by assumption. + \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}$ by assumption. + + +\end{proof} + + + + + diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 8ec83f7..1c6a0ca 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -2,6 +2,7 @@ \import{numbers.tex} \import{function.tex} \import{set/powerset.tex} +\import{topology/basis.tex} \section{Metric Spaces} @@ -20,38 +21,42 @@ -\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}\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$ we have $O = \openball{r}{x}{d}$ } \}$. + $\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{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{theorem}\label{metric_induce_a_topology} - +\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} @@ -70,7 +75,7 @@ \begin{enumerate} \item \label{metric_space_metric} $\metric[M]$ is a metric on $M$. \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$ $\openball{r}{x}{\metric[M]} \in \opens[M]$. + \item \label{metric_space_opens} $\metricopens{ \metric[M] }{M} = \opens[M]$. \end{enumerate} \end{struct} @@ -132,3 +137,16 @@ % 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