From 9a89974f293aa53451cad42f07e54e5bca14af4f Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 25 Jun 2024 00:00:38 +0200 Subject: definition of equivalence_from_partition can proof false in everything.tex --- library/everything.tex | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'library/everything.tex') diff --git a/library/everything.tex b/library/everything.tex index 61bccb2..783679f 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -16,12 +16,13 @@ \import{relation/uniqueness.tex} \import{function.tex} \import{ordinal.tex} -%\import{nat.tex} +\import{nat.tex} \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} @@ -33,3 +34,7 @@ \begin{proposition}\label{trivial} $x = x$. \end{proposition} + +%\begin{proposition}\label{safe} +% Contradiction. +%\end{proposition} -- cgit v1.2.3 From 0c82b10cd3ac1787838038b4b443f79cbb1612d9 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Wed, 26 Jun 2024 13:56:47 +0200 Subject: Working at the numbers.tex --- .gitignore | 1 + library/everything.tex | 8 ++++---- library/numbers.tex | 26 ++++++++++++++++++++++++++ 3 files changed, 31 insertions(+), 4 deletions(-) (limited to 'library/everything.tex') diff --git a/.gitignore b/.gitignore index cd7aa0f..656e54b 100644 --- a/.gitignore +++ b/.gitignore @@ -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} -- cgit v1.2.3 From cbac8ca4a5bf8ff38af3e512956ea1e468965194 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sun, 21 Jul 2024 12:26:20 +0200 Subject: Further Formalisation on numbers --- latex/naproche.sty | 1 + library/everything.tex | 2 +- library/numbers.tex | 165 ++++++++++++++++++++++++++++++++----------------- 3 files changed, 110 insertions(+), 58 deletions(-) (limited to 'library/everything.tex') diff --git a/latex/naproche.sty b/latex/naproche.sty index 476d3dd..7ef2359 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -132,6 +132,7 @@ \newcommand{\integers}{\mathcal{Z}} \newcommand{\zero}{0} \newcommand{\one}{1} +\newcommand{\rmul}{\cdot} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/library/everything.tex b/library/everything.tex index 29b97b7..b966197 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -29,7 +29,7 @@ \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} -%\import{numbers.tex} +\import{numbers.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/numbers.tex b/library/numbers.tex index 4ccba67..0bfae2d 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -18,34 +18,6 @@ $x \rmul y$ is a set. \end{signature} -\begin{axiom}\label{reals_axiom_order} - $\lt[\reals]$ is an order on $\reals$. -\end{axiom} - -\begin{abbreviation}\label{lesseq_on_reals} - $x \leq y$ iff $(x,y) \in \lt[\reals]$. -\end{abbreviation} - -\begin{abbreviation}\label{less_on_reals} - $x < y$ iff it is wrong that $y \leq x$. -\end{abbreviation} - -\begin{abbreviation}\label{greater_on_reals} - $x > y$ iff $y \leq x$. -\end{abbreviation} - -\begin{abbreviation}\label{greatereq_on_reals} - $x \geq y$ iff it is wrong that $x < y$. -\end{abbreviation} - -\begin{abbreviation}\label{is_positiv} - $x$ is positiv iff $x > \zero$. -\end{abbreviation} - - -%Structure TODO: -% Take as may axioms as needed - Tarski Axioms of reals -%Implement Naturals -> Integer -> rationals -> reals \subsection{Creation of natural numbers} @@ -384,14 +356,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $n,m \in \reals$ we have $(n + m) \in \reals$. \end{axiom} -\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_assoc} - For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. -\end{axiom} \begin{axiom}\label{reals_axiom_kommu} For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$. @@ -417,31 +382,72 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$. \end{axiom} -\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{axiom}\label{reals_disstro2} For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$. \end{axiom} - \begin{axiom}\label{reals_reducion_on_addition} For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{axiom} -\begin{axiom}\label{zero_less_one} - $\zero < 1$. +\begin{abbreviation}\label{rless} + $x < y$ iff $x \rless y$. +\end{abbreviation} + +\begin{abbreviation}\label{less_on_reals} + $x \leq y$ iff it is wrong that $y < x$. +\end{abbreviation} + +\begin{abbreviation}\label{greater_on_reals} + $x > y$ iff $y \leq x$. +\end{abbreviation} + +\begin{abbreviation}\label{greatereq_on_reals} + $x \geq y$ iff it is wrong that $x < y$. +\end{abbreviation} + +\begin{abbreviation}\label{is_positiv} + $x$ is positiv iff $x > \zero$. +\end{abbreviation} + + + + + +\begin{axiom}\label{tarski1} + For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$. +\end{axiom} + +\begin{axiom}\label{tarski2} + 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{tarski3} + 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{axiom}\label{reals_axiom_order_def} - Suppose $x,y,z,w \in \reals$. - If $x + y < z + w$ then $x < z \lor y < w$. +\begin{axiom}\label{tarski4} + For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. +\end{axiom} + +\begin{axiom}\label{tarski5} + For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$. \end{axiom} +\begin{axiom}\label{tarski8} + $\zero < 1$. +\end{axiom} + +\begin{axiom}\label{labelordersossss} + For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$. +\end{axiom} +\begin{axiom}\label{nocheinschoeneslabel} + For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. +\end{axiom} \subsection{The Intergers} @@ -465,8 +471,8 @@ Such that we can introduce the integers and raitionals as smooth as possible. \end{lemma} \begin{proof} \begin{byCase} - \caseOf{$m = \zero$.} Trivial.%Follows by \cref{neg_of_zero,minus,neg,reals_add}. - \caseOf{$m \neq \zero$.} Trivial.% Follows by \cref{neg_of_zero,minus,neg,reals_add}. + \caseOf{$m = \zero$.} Trivial. + \caseOf{$m \neq \zero$.} Trivial. \end{byCase} \end{proof} @@ -496,16 +502,31 @@ Such that we can introduce the integers and raitionals as smooth as possible. $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$. \end{lemma} \begin{proof} - Let $P = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$. - \begin{byCase} - \caseOf{$\integers \subseteq P$.} Trivial. - \caseOf{$P \subseteq \integers$.} Trivial. - \end{byCase} + Omitted. \end{proof} +\begin{abbreviation}\label{positiv_real_number} + $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$. +\end{abbreviation} +\begin{proposition}\label{integers_negativ_times_negativ_is_positiv} + Suppose $n,m \in \integers$. + Suppose $n < \zero$ and $m < \zero$. + Then $n \rmul m > \zero$. +\end{proposition} +\begin{proof} + Omitted. + %$n \neq \zero$ and $m \neq \zero$. + %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$. + %There exists $n' \in \reals$ such that $n' + n = \zero$. + %There exists $m' \in \reals$ such that $m' + m = \zero$. +\end{proof} + +%TODO: negativ * negativ = positiv. + + \subsection{The Rationals} \begin{axiom}\label{invers_reals} @@ -520,26 +541,56 @@ Such that we can introduce the integers and raitionals as smooth as possible. $\naturalsPlus = \naturals \setminus \{\zero\}$. \end{abbreviation} -\begin{definition}\label{rationals} +\begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$. \end{definition} +\begin{abbreviation}\label{nominator} + $z$ is nominator of $q$ iff there exists $n \in \naturalsPlus$ such that $q = \rfrac{z}{n}$. +\end{abbreviation} + +\begin{abbreviation}\label{denominator} + $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$. +\end{abbreviation} + +%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal} +% Suppose $p,q \in \rationals$. +% Suppose $z \in \naturals$. +% Suppose $p$ is positiv. +% Suppose $q$ is positiv. +% Suppose $z$ is nominator of $p$. +% Suppose $z$ is nominator of $p$. +% Suppose $p'$ is denominator of $p$. +% Suppose $q'$ is denominator of $q$. +% Then $p \leq q$ iff $p' \geq q'$. +%\end{proposition} + + +%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one} +% For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$. +%\end{theorem} + +% TODO: Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, \subsection{Order on the reals} + + \begin{lemma}\label{plus_one_order} For all $r\in \reals$ we have $ r < r + 1$. \end{lemma} \begin{proof} - %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}. + Omitted. \end{proof} \begin{lemma}\label{negation_and_order} Suppose $r \in \reals$. $r \leq \zero$ iff $\zero \leq \neg{r}$. \end{lemma} - +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{reals_add_of_positiv} @@ -548,7 +599,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. Then $x + y$ is positiv. \end{lemma} \begin{proof} - + Omitted. \end{proof} \begin{lemma}\label{reals_mul_of_positiv} -- cgit v1.2.3 From b8cc467735054bb3c38bf37b5e29877ba756c4b5 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 27 Aug 2024 20:20:46 +0200 Subject: working commit --- library/everything.tex | 1 + library/topology/urysohn2.tex | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+) (limited to 'library/everything.tex') diff --git a/library/everything.tex b/library/everything.tex index b966197..94dd6d8 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -30,6 +30,7 @@ \import{topology/disconnection.tex} \import{topology/separation.tex} \import{numbers.tex} +\import{topology/urysohn2.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index ea49a6c..a64fa7e 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -16,6 +16,22 @@ \section{Urysohns Lemma} +\begin{definition}\label{one_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + +\begin{struct}\label{sequence} + A sequence $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\index$ + \item $\indexset$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \end{enumerate} +\end{struct} \begin{abbreviation}\label{urysohnspace} $X$ is a urysohn space iff @@ -33,6 +49,7 @@ + \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -52,6 +69,8 @@ % & x ,x \in X <- will result in technicly ambigus parse \end{cases} + + $U_1$ Trivial. -- cgit v1.2.3