From 9abb88060e5bb6405e603dcbe499794e3e181040 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sun, 31 Mar 2024 18:57:17 +0200 Subject: Possible_Bug In File test.tex line 51 could not be proven, error massage is in the new file error.txt --- library/everything.tex | 1 + library/test.tex | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 library/test.tex (limited to 'library') diff --git a/library/everything.tex b/library/everything.tex index 9b85f83..599bc27 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -26,6 +26,7 @@ \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} +\import{test.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/test.tex b/library/test.tex new file mode 100644 index 0000000..d30bbba --- /dev/null +++ b/library/test.tex @@ -0,0 +1,54 @@ +\import{algebra/semigroup.tex} +\section{monoid} + +\begin{struct}\label{monoid} + A monoid $A$ is a semigroup equipped with + \begin{enumerate} + \item $\neutral$ + \end{enumerate} + such that + \begin{enumerate} %muss hier ein enumerate hin + \item\label{monoid_type} $\neutral[A]\in \carrier[A]$. + \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. + \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. + \end{enumerate} +\end{struct} + + +\section{Group} + +\begin{struct}\label{group} + A group $A$ is a monoid such that + \begin{enumerate} + \item\label{group_inverse} for all $a \in \carrier[A]$ there exist $b \in \carrier[A]$ such that $\mul[A](a, b) =\neutral[A]$. + \end{enumerate} +\end{struct} + +\begin{abbreviation}\label{cfourdot} + $a\cdot b = \mul(a,b)$. +\end{abbreviation} + +\begin{lemma}\label{neutral_is_idempotent} + Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$. +\end{lemma} + +\begin{proposition}\label{leftinverse_eq_rightinverse} + Let $G$ be a group and assume $a \in G$. + Then there exist $b\in G$ + such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$. +\end{proposition} +\begin{proof} + There exist $b \in G$ such that $a \cdot b = \neutral[G]$. + There exist $c \in G$ such that $b \cdot c = \neutral[G]$. + $a \cdot b = \neutral[G]$. + $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$. + $(a \cdot b) \cdot c = a \cdot (b \cdot c)$. + $a \cdot \neutral[G] = \neutral[G] \cdot c$. + $c = c \cdot \neutral[G]$. + $c = \neutral[G] \cdot c$. + $a \cdot \neutral[G] = c \cdot \neutral[G]$. + $a \cdot \neutral[G] = c$ by \cref{monoid_right}. + $a = c$ by \cref{monoid_right}. + $b \cdot a = b \cdot c$. + $b \cdot a = \neutral[G]$. +\end{proof} \ No newline at end of file -- cgit v1.2.3 From 15deff4df111d86c84d808f1c9cc4e30013287d0 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Thu, 11 Apr 2024 13:37:03 +0200 Subject: Formalisation of groups and monoids The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time --- Error.txt | 16 --------- latex/stdlib.tex | 3 +- library/algebra/group.tex | 83 +++++++++++++++++++++++++++++++++++++++++++++- library/algebra/monoid.tex | 19 +++++++++++ library/everything.tex | 3 +- library/test.tex | 54 ------------------------------ 6 files changed, 105 insertions(+), 73 deletions(-) delete mode 100644 Error.txt create mode 100644 library/algebra/monoid.tex delete mode 100644 library/test.tex (limited to 'library') diff --git a/Error.txt b/Error.txt deleted file mode 100644 index 7aa836a..0000000 --- a/Error.txt +++ /dev/null @@ -1,16 +0,0 @@ -stack exec zf -- library/test.tex -Verification failed: prover found countermodel -fof(leftinverse_eq_rightinverse,conjecture,fa=fc). -fof(monoid_right,axiom,![XA]:(monoid(XA)=>![Xa]:(elem(Xa,s__carrier(XA))=>apply(s__mul(XA),pair(Xa,s__neutral(XA)))=Xa))). -fof(leftinverse_eq_rightinverse1,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=fc). -fof(leftinverse_eq_rightinverse2,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(fc,s__neutral(fG)))). -fof(leftinverse_eq_rightinverse3,axiom,fc=apply(s__mul(fG),pair(s__neutral(fG),fc))). -fof(leftinverse_eq_rightinverse4,axiom,fc=apply(s__mul(fG),pair(fc,s__neutral(fG)))). -fof(leftinverse_eq_rightinverse5,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(s__neutral(fG),fc))). -fof(leftinverse_eq_rightinverse6,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(fa,apply(s__mul(fG),pair(fb,fc))))). -fof(leftinverse_eq_rightinverse7,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(s__neutral(fG),fc))). -fof(leftinverse_eq_rightinverse8,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)). -fof(leftinverse_eq_rightinverse9,axiom,apply(s__mul(fG),pair(fb,fc))=s__neutral(fG)&elem(fc,s__carrier(fG))). -fof(leftinverse_eq_rightinverse10,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)&elem(fb,s__carrier(fG))). -fof(leftinverse_eq_rightinverse11,axiom,elem(fa,s__carrier(fG))). -fof(leftinverse_eq_rightinverse12,axiom,group(fG)). \ No newline at end of file diff --git a/latex/stdlib.tex b/latex/stdlib.tex index 4921363..e545395 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -36,6 +36,8 @@ \input{../library/cardinal.tex} \input{../library/algebra/magma.tex} \input{../library/algebra/semigroup.tex} + \input{../library/algebra/monoid.tex} + \input{../library/algebra/group.tex} %\input{../library/algebra/quasigroup.tex} %\input{../library/algebra/loop.tex} \input{../library/order/order.tex} @@ -43,5 +45,4 @@ \input{../library/topology/topological-space.tex} \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} - \input{../library/test.tex} \end{document} diff --git a/library/algebra/group.tex b/library/algebra/group.tex index 48934bd..a79bd2f 100644 --- a/library/algebra/group.tex +++ b/library/algebra/group.tex @@ -1 +1,82 @@ -\section{Groups} +\import{algebra/monoid.tex} +\section{Group} + +\begin{struct}\label{group} + A group $G$ is a monoid such that + \begin{enumerate} + \item\label{group_inverse} for all $g \in \carrier[G]$ there exist $h \in \carrier[G]$ such that $\mul[G](g, h) =\neutral[G]$. + \end{enumerate} +\end{struct} + +\begin{corollary}\label{group_implies_monoid} + Let $G$ be a group. Then $G$ is a monoid. +\end{corollary} + +\begin{abbreviation}\label{cfourdot} + $g \cdot h = \mul(g,h)$. +\end{abbreviation} + +\begin{lemma}\label{neutral_is_idempotent} + Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$. +\end{lemma} + +\begin{lemma}\label{group_divison_right} + Let $G$ be a group. Let $a,b,c \in G$. + Then $a \cdot c = b \cdot c$ iff $a = b$. +\end{lemma} +\begin{proof} + Take $a,b,c \in G$ such that $a \cdot c = b \cdot c$. + There exist $c' \in G$ such that $c \cdot c' = \neutral[G]$. + Therefore $a \cdot c = b \cdot c$ iff $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$. + \begin{align*} + (a \cdot c) \cdot c' + &= a \cdot (c \cdot c') + \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\ + &= a \cdot \neutral[G] + \explanation{by \cref{group_inverse}}\\ + &= a + \explanation{by \cref{group_implies_monoid,monoid_right}} + \end{align*} + \begin{align*} + (b \cdot c) \cdot c' + &= b \cdot (c \cdot c') + \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\ + &= b \cdot \neutral[G] + \explanation{by \cref{group_inverse}}\\ + &= b + \explanation{by \cref{group_implies_monoid,monoid_right}} + \end{align*} + $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$ iff $a \cdot c = b \cdot c$ by assumption. + $a = b$ iff $a \cdot c = b \cdot c$ by assumption. +\end{proof} + + +\begin{proposition}\label{leftinverse_eq_rightinverse} + Let $G$ be a group and assume $a \in G$. + Then there exist $b\in G$ + such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$. +\end{proposition} +\begin{proof} + There exist $b \in G$ such that $a \cdot b = \neutral[G]$. + There exist $c \in G$ such that $b \cdot c = \neutral[G]$. + $a \cdot b = \neutral[G]$. + $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$. + $(a \cdot b) \cdot c = a \cdot (b \cdot c)$. + $a \cdot \neutral[G] = \neutral[G] \cdot c$. + $c = c \cdot \neutral[G]$. + $c = \neutral[G] \cdot c$. + $a \cdot \neutral[G] = c \cdot \neutral[G]$. + $a \cdot \neutral[G] = c$ by \cref{monoid_right,group_divison_right}. + $a = c$ by \cref{monoid_right,group_divison_right,neutral_is_idempotent}. + $b \cdot a = b \cdot c$. + $b \cdot a = \neutral[G]$. +\end{proof} + +\begin{definition}\label{group_abelian} + $G$ is an abelian group iff $G$ is a group and for all $g,h \in G$ $\mul[G](g,h) = \mul[G](h,g)$. +\end{definition} + + +\begin{definition}\label{group_automorphism} + Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. +\end{definition} diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex new file mode 100644 index 0000000..06fcb50 --- /dev/null +++ b/library/algebra/monoid.tex @@ -0,0 +1,19 @@ +\import{algebra/semigroup.tex} +\section{Monoid} + +\begin{struct}\label{monoid} + A monoid $A$ is a semigroup equipped with + \begin{enumerate} + \item $\neutral$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{monoid_type} $\neutral[A]\in \carrier[A]$. + \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. + \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. + \end{enumerate} +\end{struct} + +\begin{corollary}\label{monoid_implies_semigroup} + Let $A$ be a monoid. Then $A$ is a semigroup. +\end{corollary} \ No newline at end of file diff --git a/library/everything.tex b/library/everything.tex index 599bc27..a5166af 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -20,13 +20,14 @@ \import{cardinal.tex} \import{algebra/magma.tex} \import{algebra/semigroup.tex} +\import{algebra/monoid.tex} +\import{algebra/group.tex} \import{order/order.tex} %\import{order/semilattice.tex} \import{topology/topological-space.tex} \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} -\import{test.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/test.tex b/library/test.tex deleted file mode 100644 index d30bbba..0000000 --- a/library/test.tex +++ /dev/null @@ -1,54 +0,0 @@ -\import{algebra/semigroup.tex} -\section{monoid} - -\begin{struct}\label{monoid} - A monoid $A$ is a semigroup equipped with - \begin{enumerate} - \item $\neutral$ - \end{enumerate} - such that - \begin{enumerate} %muss hier ein enumerate hin - \item\label{monoid_type} $\neutral[A]\in \carrier[A]$. - \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. - \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. - \end{enumerate} -\end{struct} - - -\section{Group} - -\begin{struct}\label{group} - A group $A$ is a monoid such that - \begin{enumerate} - \item\label{group_inverse} for all $a \in \carrier[A]$ there exist $b \in \carrier[A]$ such that $\mul[A](a, b) =\neutral[A]$. - \end{enumerate} -\end{struct} - -\begin{abbreviation}\label{cfourdot} - $a\cdot b = \mul(a,b)$. -\end{abbreviation} - -\begin{lemma}\label{neutral_is_idempotent} - Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$. -\end{lemma} - -\begin{proposition}\label{leftinverse_eq_rightinverse} - Let $G$ be a group and assume $a \in G$. - Then there exist $b\in G$ - such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$. -\end{proposition} -\begin{proof} - There exist $b \in G$ such that $a \cdot b = \neutral[G]$. - There exist $c \in G$ such that $b \cdot c = \neutral[G]$. - $a \cdot b = \neutral[G]$. - $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$. - $(a \cdot b) \cdot c = a \cdot (b \cdot c)$. - $a \cdot \neutral[G] = \neutral[G] \cdot c$. - $c = c \cdot \neutral[G]$. - $c = \neutral[G] \cdot c$. - $a \cdot \neutral[G] = c \cdot \neutral[G]$. - $a \cdot \neutral[G] = c$ by \cref{monoid_right}. - $a = c$ by \cref{monoid_right}. - $b \cdot a = b \cdot c$. - $b \cdot a = \neutral[G]$. -\end{proof} \ No newline at end of file -- cgit v1.2.3 From 5c297fe2fde2ac9a926ba1911aa72d383450ce98 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Thu, 11 Apr 2024 14:39:49 +0200 Subject: Set the Headline Order for the corresponding section --- library/order/order.tex | 1 + 1 file changed, 1 insertion(+) (limited to 'library') diff --git a/library/order/order.tex b/library/order/order.tex index 339bad8..1b7692f 100644 --- a/library/order/order.tex +++ b/library/order/order.tex @@ -1,6 +1,7 @@ \import{relation.tex} \import{relation/properties.tex} \import{order/quasiorder.tex} +\section{Order} % also called "(partial) ordering" or "partial order" to contrast with connex (i.e. "total") orders. \begin{abbreviation}\label{order} -- cgit v1.2.3 From 6eea98cf3e66a07251e6370ea948898799d5055b Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 13 Apr 2024 13:01:14 +0200 Subject: first formalisation of addition on naturals We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds --- latex/naproche.sty | 2 ++ library/nat.tex | 40 ++++++++++++++++++++++++++++++++++++++-- 2 files changed, 40 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/latex/naproche.sty b/latex/naproche.sty index 9764693..d975f21 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -127,6 +127,8 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} +\newcommand{\addpair}{\mathcal{H}} +%\newcommand{\add}[2]{(#1 + #2)} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/library/nat.tex b/library/nat.tex index 529ba54..849c610 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -1,5 +1,5 @@ \import{set/suc.tex} - +\import{set.tex} \section{Natural numbers} @@ -17,5 +17,41 @@ \end{axiom} \begin{abbreviation}\label{naturalnumber} - $n$ is a natural number iff $n\in\naturals$. + $n$ is a natural number iff $n\in \naturals$. \end{abbreviation} + +\begin{lemma}\label{emptyset_in_naturals} + $\emptyset\in\naturals$. +\end{lemma} + +%\begin{abbreviation}\label{zero_is_emptyset} +% $0 = \emptyset$. +%\end{abbreviation} + +%\begin{definition}\label{additionpair} +% $x$ is an Additionpair iff $x \in ((\naturals\times \naturals)\times \naturals)$. +%\end{definition} + +%\begin{lemma}\label{zero_is_in_naturals} +% Let $n\in \naturals$. $((n, \emptyset), n)$ is an Additionpair. +%\end{lemma} + +%\begin{definition}\label{valid_additionpair} +% $x$ is a vaildaddition iff there exist $n \in \naturals$ we have $x = ((0, n), n)$. +%\end{definition} + + + +\begin{axiom}\label{addpair_set} + $\addpair$ is a set. +\end{axiom} + + + + +\begin{axiom}\label{addition_naturals} + $x \in \addpair$ iff $x \in ((\naturals\times \naturals)\times \naturals)$ and there exist $n \in \naturals$ such that $x = ((n, \emptyset), n)$. +\end{axiom} + + + -- cgit v1.2.3 From cfd5061ced34f061e84ecca2a266f8f4cd01ce36 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:26:13 +0200 Subject: Adding the first formalisation of reals --- latex/naproche.sty | 5 +- latex/stdlib.tex | 1 + library/everything.tex | 1 + library/nat.tex | 41 ++++++----- library/numbers.tex | 140 ++++++++++++++++++++++++++++++++++++ library/topology/order-topology.tex | 7 ++ 6 files changed, 175 insertions(+), 20 deletions(-) create mode 100644 library/numbers.tex create mode 100644 library/topology/order-topology.tex (limited to 'library') diff --git a/latex/naproche.sty b/latex/naproche.sty index d975f21..cb65fe7 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -127,8 +127,9 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} -\newcommand{\addpair}{\mathcal{H}} -%\newcommand{\add}[2]{(#1 + #2)} +\newcommand{\integers}{\mathcal{Z}} +\newcommand{\zero}{0} +\newcommand{\one}{1} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/latex/stdlib.tex b/latex/stdlib.tex index e545395..dba42a2 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -45,4 +45,5 @@ \input{../library/topology/topological-space.tex} \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} + \input{../library/numbers.tex} \end{document} diff --git a/library/everything.tex b/library/everything.tex index a5166af..61bccb2 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -28,6 +28,7 @@ \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} +\import{numbers.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/nat.tex b/library/nat.tex index 849c610..ac9a141 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -24,34 +24,39 @@ $\emptyset\in\naturals$. \end{lemma} -%\begin{abbreviation}\label{zero_is_emptyset} -% $0 = \emptyset$. -%\end{abbreviation} +\begin{signature}\label{addition_is_set} + $x+y$ is a set. +\end{signature} + +\begin{axiom}\label{addition_on_naturals} + $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number. +\end{axiom} + +\begin{abbreviation}\label{zero_is_emptyset} + $\zero = \emptyset$. +\end{abbreviation} + +\begin{axiom}\label{addition_axiom_1} + For all $x \in \naturals$ $x + \zero = \zero + x = x$. +\end{axiom} + +\begin{axiom}\label{addition_axiom_2} + For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$. +\end{axiom} + +\begin{lemma}\label{naturals_is_equal_to_two_times_naturals} + $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$. +\end{lemma} -%\begin{definition}\label{additionpair} -% $x$ is an Additionpair iff $x \in ((\naturals\times \naturals)\times \naturals)$. -%\end{definition} -%\begin{lemma}\label{zero_is_in_naturals} -% Let $n\in \naturals$. $((n, \emptyset), n)$ is an Additionpair. -%\end{lemma} -%\begin{definition}\label{valid_additionpair} -% $x$ is a vaildaddition iff there exist $n \in \naturals$ we have $x = ((0, n), n)$. -%\end{definition} -\begin{axiom}\label{addpair_set} - $\addpair$ is a set. -\end{axiom} -\begin{axiom}\label{addition_naturals} - $x \in \addpair$ iff $x \in ((\naturals\times \naturals)\times \naturals)$ and there exist $n \in \naturals$ such that $x = ((n, \emptyset), n)$. -\end{axiom} diff --git a/library/numbers.tex b/library/numbers.tex new file mode 100644 index 0000000..93623fa --- /dev/null +++ b/library/numbers.tex @@ -0,0 +1,140 @@ +\import{nat.tex} +\import{order/order.tex} +\import{relation.tex} + +\section{The real numbers} + +\begin{signature} + $\reals$ is a set. +\end{signature} + +\begin{signature} + $x + y$ is a set. +\end{signature} + +\begin{signature} + $x \times y$ is a set. +\end{signature} + +\begin{axiom}\label{one_in_reals} + $1 \in \reals$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_order} + $\lt[\reals]$ is an order on $\reals$. + %$\reals$ is an ordered set. +\end{axiom} + +\begin{axiom}\label{reals_axiom_strictorder} + $\lt[\reals]$ is a strict order. +\end{axiom} + +\begin{axiom}\label{reals_axiom_dense} + For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then + there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$. + + %For all $X,Y \subseteq \reals$ if for all $x,y$ $x\in X$ and $y \in Y$ such that $x \lt[\reals] y$ + %then there exist a $z \in \reals$ such that if $x \neq z$ and $y \neq z$ $x \lt[\reals] z$ and $z \lt[\reals] y$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_order_def} + $(x,y) \in \lt[\reals]$ iff there exist $z \in \reals$ such that $(\zero, z) \in \lt[\reals]$ and $x + z = y$. +\end{axiom} + +\begin{lemma}\label{reals_one_bigger_than_zero} + $(\zero,1) \in \lt[\reals]$. +\end{lemma} + + +\begin{axiom}\label{reals_axiom_assoc} + For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \times y) \times z = x \times (y \times z)$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_kommu} + For all $x,y \in \reals$ $x + y = y + x$ and $x \times y = y \times x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_zero_in_reals} + $\zero \in \reals$. +\end{axiom} + +%\begin{axiom}\label{reals_axiom_one_in_reals} +% $\one \in \reals$. +%\end{axiom} + +\begin{axiom}\label{reals_axiom_zero} + %There exist $\zero \in \reals$ such that + For all $x \in \reals$ $x + \zero = x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_one} + %There exist $1 \in \reals$ such that + For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_add_invers} + For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. +\end{axiom} + +%TODO: Implementing Notion for negativ number such as -x. + +%\begin{abbreviation}\label{reals_notion_minus} +% $y = -x$ iff $x + y = \zero$. +%\end{abbreviation} %This abbrevation result in a killed process. + +\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$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_disstro1} + For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$. +\end{axiom} + +\begin{proposition}\label{reals_disstro2} + For all $x,y,z \in \reals$ $(y + z) \times x = (y \times x) + (z \times x)$. +\end{proposition} + +\begin{proposition}\label{reals_reducion_on_addition} + For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. +\end{proposition} + +\begin{signature} + $\invers$ is a set. +\begin{signature} + +%TODO: +%x \rless y in einer signatur hinzufügen und dann axiom x+z = y und dann \rlt in def per iff +%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher +%\cdot für multiklikation verwenden. +%< für die relation benutzen. + +%\begin{signature} +% $y^{\rightarrow}$ is a function. +%\end{signature} + +%\begin{axiom}\label{notion_multi_invers} +% If $y \in \reals$ then $\invers{y} \in \reals$ and $y \times y^{\rightarrow} = 1$. +%\end{axiom} + +%\begin{abbreviation}\label{notion_fraction} +% $\frac{x}{y} = x \times y^{\rightarrow}$. +%\end{abbreviation} + +\begin{lemma}\label{order_reals_lemma1} + For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((y \times x), (z \times x)) \in \lt[\reals]$. +\end{lemma} + +\begin{lemma}\label{order_reals_lemma2} + For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((x \times y), (x \times z)) \in \lt[\reals]$. +\end{lemma} + + +\begin{lemma}\label{order_reals_lemma3} + For all $x,y,z \in \reals$ such that $(x,\zero) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((x \times z), (x \times y)) \in \lt[\reals]$. +\end{lemma} diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex new file mode 100644 index 0000000..afa8755 --- /dev/null +++ b/library/topology/order-topology.tex @@ -0,0 +1,7 @@ +\import{topology/topological-space.tex} + +\section{Order Topology} + +\begin{definition} + A +\end{definition} -- cgit v1.2.3 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/numbers.tex | 72 +++++++++++++++++---------------- library/topology/metric-space.tex | 80 +++++++++++++++++++++++++++++++++++++ library/topology/order-topology.tex | 32 +++++++++++++-- 3 files changed, 146 insertions(+), 38 deletions(-) create mode 100644 library/topology/metric-space.tex (limited to 'library') diff --git a/library/numbers.tex b/library/numbers.tex index 93623fa..afb7d3f 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -4,6 +4,14 @@ \section{The real numbers} +%TODO: Implementing Notion for negativ number such as -x. + +%TODO: +%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher +%\cdot für multiklikation verwenden. +%< für die relation benutzen. + + \begin{signature} $\reals$ is a set. \end{signature} @@ -22,19 +30,31 @@ \begin{axiom}\label{reals_axiom_order} $\lt[\reals]$ is an order on $\reals$. - %$\reals$ is an ordered set. \end{axiom} \begin{axiom}\label{reals_axiom_strictorder} $\lt[\reals]$ is a strict order. \end{axiom} +\begin{abbreviation}\label{less_on_reals} + $x < y$ iff $(x,y) \in \lt[\reals]$. +\end{abbreviation} + +\begin{abbreviation}\label{greater_on_reals} + $x > y$ iff $y < x$. +\end{abbreviation} + +\begin{abbreviation}\label{lesseq_on_reals} + $x \leq y$ iff it is wrong that $x > y$. +\end{abbreviation} + +\begin{abbreviation}\label{greatereq_on_reals} + $x \geq y$ iff it is wrong that $x < y$. +\end{abbreviation} + \begin{axiom}\label{reals_axiom_dense} For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$. - - %For all $X,Y \subseteq \reals$ if for all $x,y$ $x\in X$ and $y \in Y$ such that $x \lt[\reals] y$ - %then there exist a $z \in \reals$ such that if $x \neq z$ and $y \neq z$ $x \lt[\reals] z$ and $z \lt[\reals] y$. \end{axiom} \begin{axiom}\label{reals_axiom_order_def} @@ -57,18 +77,12 @@ \begin{axiom}\label{reals_axiom_zero_in_reals} $\zero \in \reals$. \end{axiom} - -%\begin{axiom}\label{reals_axiom_one_in_reals} -% $\one \in \reals$. -%\end{axiom} - + \begin{axiom}\label{reals_axiom_zero} - %There exist $\zero \in \reals$ such that For all $x \in \reals$ $x + \zero = x$. \end{axiom} \begin{axiom}\label{reals_axiom_one} - %There exist $1 \in \reals$ such that For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. \end{axiom} @@ -76,11 +90,6 @@ For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. \end{axiom} -%TODO: Implementing Notion for negativ number such as -x. - -%\begin{abbreviation}\label{reals_notion_minus} -% $y = -x$ iff $x + y = \zero$. -%\end{abbreviation} %This abbrevation result in a killed process. \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$. @@ -98,27 +107,8 @@ For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{proposition} -\begin{signature} - $\invers$ is a set. -\begin{signature} - -%TODO: -%x \rless y in einer signatur hinzufügen und dann axiom x+z = y und dann \rlt in def per iff -%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher -%\cdot für multiklikation verwenden. -%< für die relation benutzen. - -%\begin{signature} -% $y^{\rightarrow}$ is a function. -%\end{signature} -%\begin{axiom}\label{notion_multi_invers} -% If $y \in \reals$ then $\invers{y} \in \reals$ and $y \times y^{\rightarrow} = 1$. -%\end{axiom} -%\begin{abbreviation}\label{notion_fraction} -% $\frac{x}{y} = x \times y^{\rightarrow}$. -%\end{abbreviation} \begin{lemma}\label{order_reals_lemma1} For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ @@ -138,3 +128,15 @@ if $(y,z) \in \lt[\reals]$ then $((x \times z), (x \times y)) \in \lt[\reals]$. \end{lemma} + +\begin{lemma}\label{a} + For all $x,y \in \reals$ if $x > y$ then $x \geq y$. +\end{lemma} + +\begin{lemma}\label{aa} + For all $x,y \in \reals$ if $x < y$ then $x \leq y$. +\end{lemma} + +\begin{lemma}\label{aaa} + For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. +\end{lemma} \ No newline at end of file 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 14:50:35 +0200 Subject: Clean up of Notation in numbers.tex First notation of tupels in the relation set was swapped with the canonical <. --- library/numbers.tex | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'library') diff --git a/library/numbers.tex b/library/numbers.tex index afb7d3f..df47d81 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -53,16 +53,16 @@ \end{abbreviation} \begin{axiom}\label{reals_axiom_dense} - For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then - there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$. + For all $x,y \in \reals$ if $x < y$ then + there exist $z \in \reals$ such that $x < z$ and $z < y$. \end{axiom} \begin{axiom}\label{reals_axiom_order_def} - $(x,y) \in \lt[\reals]$ iff there exist $z \in \reals$ such that $(\zero, z) \in \lt[\reals]$ and $x + z = y$. + $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x + z = y$. \end{axiom} \begin{lemma}\label{reals_one_bigger_than_zero} - $(\zero,1) \in \lt[\reals]$. + $\zero < 1$. \end{lemma} @@ -111,22 +111,22 @@ \begin{lemma}\label{order_reals_lemma1} - For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ - if $(y,z) \in \lt[\reals]$ - then $((y \times x), (z \times x)) \in \lt[\reals]$. + For all $x,y,z \in \reals$ such that $\zero < x$ + if $y < z$ + then $(y \times x) < (z \times x)$. \end{lemma} \begin{lemma}\label{order_reals_lemma2} - For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ - if $(y,z) \in \lt[\reals]$ - then $((x \times y), (x \times z)) \in \lt[\reals]$. + For all $x,y,z \in \reals$ such that $\zero < x$ + if $y < z$ + then $(x \times y) < (x \times z)$. \end{lemma} \begin{lemma}\label{order_reals_lemma3} - For all $x,y,z \in \reals$ such that $(x,\zero) \in \lt[\reals]$ - if $(y,z) \in \lt[\reals]$ - then $((x \times z), (x \times y)) \in \lt[\reals]$. + For all $x,y,z \in \reals$ such that $x < \zero$ + if $y < z$ + then $(x \times z) < (x \times y)$. \end{lemma} \begin{lemma}\label{a} -- cgit v1.2.3 From 08019dcdaf3b13bb8ce554dfd5377690bb508c6d Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> 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') 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') 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') 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