diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | latex/naproche.sty | 3 | ||||
| -rw-r--r-- | latex/stdlib.tex | 3 | ||||
| -rw-r--r-- | library/algebra/group.tex | 83 | ||||
| -rw-r--r-- | library/algebra/monoid.tex | 19 | ||||
| -rw-r--r-- | library/everything.tex | 3 | ||||
| -rw-r--r-- | library/nat.tex | 45 | ||||
| -rw-r--r-- | library/numbers.tex | 195 | ||||
| -rw-r--r-- | library/order/order.tex | 1 | ||||
| -rw-r--r-- | library/topology/basis.tex | 69 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 152 | ||||
| -rw-r--r-- | library/topology/order-topology.tex | 33 |
12 files changed, 606 insertions, 3 deletions
@@ -41,3 +41,6 @@ premseldump/ haddocks/ stack.yaml.lock zf*.svg +Anmerkungen.txt +vampire-taks-with-not-expacted-behavoir/ + diff --git a/latex/naproche.sty b/latex/naproche.sty index 00ddf9a..476d3dd 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -129,6 +129,9 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} +\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 3673801..dba42a2 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,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/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 9b85f83..61bccb2 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -20,12 +20,15 @@ \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{numbers.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/nat.tex b/library/nat.tex index 529ba54..ac9a141 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,46 @@ \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{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} + + + + + + + + + + + + + diff --git a/library/numbers.tex b/library/numbers.tex new file mode 100644 index 0000000..5dd06da --- /dev/null +++ b/library/numbers.tex @@ -0,0 +1,195 @@ +\import{nat.tex} +\import{order/order.tex} +\import{relation.tex} + +\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. +% sup und inf einfügen + +\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$. +\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$ then + there exist $z \in \reals$ such that $x < z$ and $z < y$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_order_def} + $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$. +\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_zero} + For all $x \in \reals$ $x + \zero = x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_one} + 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} + + +\begin{axiom}\label{reals_axiom_mul_invers} + 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} + 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{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} + 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$ + 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$ + if $y < z$ + then $(x \times z) < (x \times y)$. +\end{lemma} + +\begin{lemma}\label{o4rder_reals_lemma} + For all $x,y \in \reals$ if $x > y$ then $x \geq y$. +\end{lemma} + +\begin{lemma}\label{order_reals_lemma5} + For all $x,y \in \reals$ if $x < y$ then $x \leq y$. +\end{lemma} + +\begin{lemma}\label{order_reals_lemma6} + 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/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} diff --git a/library/topology/basis.tex b/library/topology/basis.tex index d8cfeaf..15910f9 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} @@ -48,3 +50,70 @@ $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$ \\ such that $x\in V\subseteq U$}\right\}$. \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 new file mode 100644 index 0000000..1c6a0ca --- /dev/null +++ b/library/topology/metric-space.tex @@ -0,0 +1,152 @@ +\import{topology/topological-space.tex} +\import{numbers.tex} +\import{function.tex} +\import{set/powerset.tex} +\import{topology/basis.tex} + +\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 + 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{definition} + +\begin{definition}\label{open_ball} + $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric on $M$ and $f(x,z) < r$ } \}$. +\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$ 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} + + + + +%TODO: \metric_opens{d} = {hier die construction für topology} DONE. +%TODO: Die induzierte topology definieren und dann in struct verwenden. + + +\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_metric} $\metric[M]$ is a metric on $M$. + \item \label{metric_space_topology} $M$ is a topological space. + \item \label{metric_space_opens} $\metricopens{ \metric[M] }{M} = \opens[M]$. + \end{enumerate} +\end{struct} + +\begin{abbreviation}\label{descriptive_syntax_for_openball1} + $U$ is an open ball in $M$ of $x$ with radius $r$ iff $x \in M$ and $M$ is a metric space and $U = \openball{r}{x}{\metric[M]}$. +\end{abbreviation} + +\begin{abbreviation}\label{descriptive_syntax_for_openball2} + $U$ is an open ball in $M$ iff there exist $x \in M$ such that there exist $r \in \reals$ such that $U$ is an open ball in $M$ of $x$ with radius $r$. +\end{abbreviation} + +\begin{lemma}\label{union_of_open_balls_is_open} + Let $M$ be a metric space. + For all $U,V \subseteq M$ if $U$, $V$ are open balls in $M$ then $U \union V$ is open in $M$. +\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} + Let $M$ be a set, and let $f$ be a metric on $M$. + Then $M$ is a metric space. +\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. + diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex new file mode 100644 index 0000000..2dd026d --- /dev/null +++ b/library/topology/order-topology.tex @@ -0,0 +1,33 @@ +\import{topology/topological-space.tex} +\import{order/order.tex} + +\section{Order Topology} + +\begin{abbreviation}\label{open_interval} + $z \in \oointervalof{x}{y}$ iff $x \mathrel{R} y$ and $x \mathrel{R} z$ and $z \mathrel{R} y$. + %$\oointervalof{x}{y}{X} = \{ z \mid x \in X, y \in X, z \in X x \mathrel{R} y \wedge x \mathrel{R} z \wedge z \mathrel{R} y\}$. +\end{abbreviation} + +\begin{struct}\label{order_topology} + A ordertopology space $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $<$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{order_topology_1} $<$ is a strict order on $X$ + \item \label{order_topology_2} + \item \label{order_topology_3} + \item \label{order_topology_4} + \item \label{order_topology} + \item \label{order_topology} + \item \label{order_topology} + \end{enumerate} +\end{struct} + + + +%\begin{definition}\label{order_topology} +% $X$ has the order topology iff for all $x,y \in X$ $X$ has a strict order $R$ and $\oointervalof{x}{y}{X} \in \opens[X]$ and $X$ is a topological space. +% %$O$ is the order Topology on $X$ iff for all $x,y \in X$ $X$ has a strict order $R$ and $(x,y) \in O$ and $O$ is . +%\end{definition} |