diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | library/everything.tex | 8 | ||||
| -rw-r--r-- | library/numbers.tex | 26 |
3 files changed, 31 insertions, 4 deletions
@@ -41,6 +41,7 @@ premseldump/ haddocks/ stack.yaml.lock zf*.svg +check/ diff --git a/library/everything.tex b/library/everything.tex index 783679f..29b97b7 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -29,12 +29,12 @@ \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} -\import{numbers.tex} +%\import{numbers.tex} \begin{proposition}\label{trivial} $x = x$. \end{proposition} -%\begin{proposition}\label{safe} -% Contradiction. -%\end{proposition} +\begin{proposition}\label{safe} + Contradiction. +\end{proposition} diff --git a/library/numbers.tex b/library/numbers.tex index 1837ae8..f13214d 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -1,5 +1,6 @@ \import{order/order.tex} \import{relation.tex} +\import{set/suc.tex} \section{The real numbers} @@ -15,6 +16,11 @@ $x \rmul y$ is a set. \end{signature} +%Structure TODO: +% Take as may axioms as needed - Tarski Axioms of reals +%Implement Naturals -> Integer -> rationals -> reals + + \subsection{Basic axioms of the reals} \begin{axiom}\label{reals_axiom_zero_in_reals} @@ -29,6 +35,26 @@ $\zero \neq 1$. \end{axiom} +\begin{inductive}\label{naturals_subset_reals} + Define $\naturals \subseteq \reals$ inductively as follows. + \begin{enumerate} + \item $\zero \in \naturals$. + \item If $n\in \naturals$, then $\successor{n} \in \naturals$. + \end{enumerate} +\end{inductive} + +%\begin{axiom}\label{negativ_is_set} +% $\negativ{x}$ is a set. +%\end{axiom} + +%\begin{axiom}\label{negativ_of} +% $\negativ{x} \in \reals$ iff $x\in \reals$. +%\end{axiom} +% +%\begin{axiom}\label{negativ_behavior} +% $x + \negativ{x} = \zero$. +%\end{axiom} + \begin{definition}\label{reals_definition_order_def} $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$. \end{definition} |