diff options
| -rw-r--r-- | latex/naproche.sty | 5 | ||||
| -rw-r--r-- | latex/stdlib.tex | 1 | ||||
| -rw-r--r-- | library/everything.tex | 1 | ||||
| -rw-r--r-- | library/nat.tex | 41 | ||||
| -rw-r--r-- | library/numbers.tex | 140 | ||||
| -rw-r--r-- | library/topology/order-topology.tex | 7 |
6 files changed, 175 insertions, 20 deletions
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} |