diff options
36 files changed, 4426 insertions, 283 deletions
@@ -41,6 +41,7 @@ premseldump/ haddocks/ stack.yaml.lock zf*.svg +check/ diff --git a/latex/naproche.sty b/latex/naproche.sty index 476d3dd..c0fd318 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -40,6 +40,7 @@ \newtheorem{remark}[theoremcount]{Remark} \newtheorem{signature}[theoremcount]{Signature} \newtheorem{theorem}[theoremcount]{Theorem} +\newtheorem{inductive}[theoremcount]{Inductive} % Theorem environments without numbering. \newtheorem*{quotedaxiom}{Axiom} @@ -100,6 +101,7 @@ \newcommand{\memrel}[1]{{\in_{#1}}} \newcommand{\monusNat}{-_{\naturals}} \newcommand{\naturals}{\mathcal{N}} +\newcommand{\naturalsPlus}{\mathcal{N}_{+}} \newcommand{\notmeets}{\mathrel{\not\meets}} \newcommand{\pow}[1]{\fun{Pow}(#1)} \newcommand{\precedes}{<} @@ -132,6 +134,30 @@ \newcommand{\integers}{\mathcal{Z}} \newcommand{\zero}{0} \newcommand{\one}{1} +\newcommand{\rmul}{\cdot} +\newcommand{\inv}[1]{#1^{-1}} +\newcommand{\rfrac}[2]{\frac{#1}{#2}} +\newcommand{\rationals}{\mathcal{Q}} +\newcommand{\rminus}{-_{\mathcal{R}}} +\newcommand{\seq}[2]{\{#1, ... ,#2\}} +\newcommand{\indexx}[2][]{index_{#1}(#2)} +\newcommand{\indexxset}[1]{#1} +\newcommand{\topoBasisReals}{\mathbb{B}_{\mathcal{R}}} +\newcommand{\intervalopen}[2]{(#1, #2)} +\newcommand{\intervalclosed}[2]{[#1, #2]} +\newcommand{\epsBall}[2]{\mathcal{B}_{#1,#2}} +\newcommand{\realsplus}{\reals_{+}} +\newcommand{\rless}{<} +\newcommand{\two}{2} +\newcommand{\powerOfTwoSet}{\mathbb{P}_{2^{}}} +\newcommand{\pot}{\powerOfTwoSet} +\newcommand{\chain}[1]{#1} +\newcommand{\refine}{\text{ finer than }} +\newcommand{\abs}[1]{\left\lvert#1\right\rvert} +\newcommand{\realsminus}{\reals_{-}} +\newcommand{\at}[2]{#1(#2)} +\newcommand{\intervalopenInfiniteLeft}[1]{(-\infty, #1)} +\newcommand{\intervalopenInfiniteRight}[1]{(#1, \infty)} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol @@ -165,6 +191,7 @@ \newcommand{\closure}[2]{\fun{cl}_{#2}{#1}} \newcommand{\frontier}[2]{\fun{fr}_{#2}{#1}} \newcommand{\neighbourhoods}[2]{\textsf{N}_{#2}{#1}} +\newcommand{\neighbourhoodsSet}[2]{\textsf{N}_{SET #2}{#1}} \newcommand{\disconnections}[1]{\fun{Disconnections}{#1}} \newcommand{\teezero}{\ensuremath{T_0}} % Kolmogorov diff --git a/latex/stdlib.tex b/latex/stdlib.tex index dba42a2..9879708 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -46,4 +46,8 @@ \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} \input{../library/numbers.tex} + \input{../library/topology/urysohn.tex} + \input{../library/topology/urysohn2.tex} + \input{../library/topology/real-topological-space.tex} + %\input{../library/wunschzettel.tex} \end{document} diff --git a/library/algebra/group.tex b/library/algebra/group.tex index a79bd2f..449bacb 100644 --- a/library/algebra/group.tex +++ b/library/algebra/group.tex @@ -1,5 +1,5 @@ \import{algebra/monoid.tex} -\section{Group} +\section{Group}\label{form_sec_group} \begin{struct}\label{group} A group $G$ is a monoid such that @@ -80,3 +80,13 @@ \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} + +\begin{definition}\label{trivial_group} + $G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$. +\end{definition} + +\begin{theorem}\label{trivial_implies_abelian} + Let $G$ be a group. + Suppose $G$ is the trivial group. + Then $G$ is an abelian group. +\end{theorem} diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex index 06fcb50..3249a93 100644 --- a/library/algebra/monoid.tex +++ b/library/algebra/monoid.tex @@ -1,5 +1,5 @@ \import{algebra/semigroup.tex} -\section{Monoid} +\section{Monoid}\label{form_sec_monoid} \begin{struct}\label{monoid} A monoid $A$ is a semigroup equipped with diff --git a/library/cardinal.tex b/library/cardinal.tex index d0dec59..5682619 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -1,8 +1,9 @@ -\section{Cardinality} +\section{Cardinality}\label{form_sec_cardinality} \import{set.tex} \import{ordinal.tex} \import{function.tex} +\import{numbers.tex} \begin{definition}\label{finite} $X$ is finite iff there exists a natural number $k$ such that @@ -12,3 +13,10 @@ \begin{abbreviation}\label{infinite} $X$ is infinite iff $X$ is not finite. \end{abbreviation} + +\begin{definition}\label{cardinality} + $X$ has cardinality $k$ iff $k$ is a natural number and + there exists a bijection from $k$ to $X$. +\end{definition} + + diff --git a/library/everything.tex b/library/everything.tex index 61bccb2..94dd6d8 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} @@ -29,7 +30,12 @@ \import{topology/disconnection.tex} \import{topology/separation.tex} \import{numbers.tex} +\import{topology/urysohn2.tex} \begin{proposition}\label{trivial} $x = x$. \end{proposition} + +\begin{proposition}\label{safe} + Contradiction. +\end{proposition} diff --git a/library/nat.tex b/library/nat.tex index ac9a141..841ac36 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -3,48 +3,48 @@ \section{Natural numbers} -\begin{abbreviation}\label{inductive_set} +\begin{abbreviation}\label{num_inductive_set} $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$. \end{abbreviation} -\begin{axiom}\label{naturals_inductive_set} +\begin{axiom}\label{num_naturals_inductive_set} $\naturals$ is an inductive set. \end{axiom} -\begin{axiom}\label{naturals_smallest_inductive_set} +\begin{axiom}\label{num_naturals_smallest_inductive_set} Let $A$ be an inductive set. Then $\naturals\subseteq A$. \end{axiom} -\begin{abbreviation}\label{naturalnumber} +\begin{abbreviation}\label{num_naturalnumber} $n$ is a natural number iff $n\in \naturals$. \end{abbreviation} -\begin{lemma}\label{emptyset_in_naturals} +\begin{lemma}\label{num_emptyset_in_naturals} $\emptyset\in\naturals$. \end{lemma} -\begin{signature}\label{addition_is_set} +\begin{signature}\label{num_addition_is_set} $x+y$ is a set. \end{signature} -\begin{axiom}\label{addition_on_naturals} +\begin{axiom}\label{num_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} +\begin{abbreviation}\label{num_zero_is_emptyset} $\zero = \emptyset$. \end{abbreviation} -\begin{axiom}\label{addition_axiom_1} +\begin{axiom}\label{num_addition_axiom_1} For all $x \in \naturals$ $x + \zero = \zero + x = x$. \end{axiom} -\begin{axiom}\label{addition_axiom_2} +\begin{axiom}\label{num_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} +\begin{lemma}\label{num_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 index 5dd06da..d3af3f1 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -1,16 +1,10 @@ -\import{nat.tex} \import{order/order.tex} \import{relation.tex} +\import{set/suc.tex} +\import{ordinal.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 +\section{The numbers}\label{form_sec_numbers} \begin{signature} $\reals$ is a set. @@ -21,140 +15,719 @@ \end{signature} \begin{signature} - $x \times y$ is a set. + $x \rmul y$ is a set. \end{signature} + + +\subsection{Creation of natural numbers} + +\subsubsection{Defenition and axioms} + +\begin{abbreviation}\label{inductive_set} + $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$. +\end{abbreviation} + +\begin{abbreviation}\label{zero_is_emptyset} + $\zero = \emptyset$. +\end{abbreviation} + +\begin{axiom}\label{reals_axiom_zero_in_reals} + $\zero \in \reals$. +\end{axiom} + \begin{axiom}\label{one_in_reals} $1 \in \reals$. \end{axiom} -\begin{axiom}\label{reals_axiom_order} - $\lt[\reals]$ is an order on $\reals$. +\begin{axiom}\label{zero_neq_one} + $\zero \neq 1$. \end{axiom} -\begin{axiom}\label{reals_axiom_strictorder} - $\lt[\reals]$ is a strict order. +\begin{axiom}\label{one_is_suc_zero} + $\suc{\zero} = 1$. \end{axiom} -\begin{abbreviation}\label{less_on_reals} - $x < y$ iff $(x,y) \in \lt[\reals]$. -\end{abbreviation} +\begin{axiom}\label{naturals_subseteq_reals} + $\naturals \subseteq \reals$. +\end{axiom} -\begin{abbreviation}\label{greater_on_reals} - $x > y$ iff $y < x$. -\end{abbreviation} +\begin{axiom}\label{naturals_inductive_set} + $\naturals$ is an inductive set. +\end{axiom} -\begin{abbreviation}\label{lesseq_on_reals} - $x \leq y$ iff it is wrong that $x > y$. -\end{abbreviation} +\begin{axiom}\label{naturals_smallest_inductive_set} + Let $A$ be an inductive set. + Then $\naturals\subseteq A$. +\end{axiom} -\begin{abbreviation}\label{greatereq_on_reals} - $x \geq y$ iff it is wrong that $x < y$. +\begin{abbreviation}\label{is_a_natural_number} + $n$ is a natural number iff $n \in \naturals$. \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$. +\begin{axiom}\label{naturals_addition_axiom_1} + For all $n \in \naturals$ $n + \zero = \zero + n = n$. \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$. +\begin{axiom}\label{naturals_addition_axiom_2} + For all $n, m \in \naturals$ $n + \suc{m} = \suc{n} + m = \suc{n+m}$. \end{axiom} -\begin{lemma}\label{reals_one_bigger_than_zero} - $\zero < 1$. +\begin{axiom}\label{naturals_mul_axiom_1} + For all $n \in \naturals$ we have $n \rmul \zero = \zero = \zero \rmul n$. +\end{axiom} + +\begin{axiom}\label{naturals_mul_axiom_2} + For all $n,m \in \naturals$ we have $\suc{n} \rmul m = (n \rmul m) + m$. +\end{axiom} + +\begin{axiom}\label{addition_on_naturals} + If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number. +\end{axiom} + +\begin{axiom}\label{naturals_rmul_is_closed_in_n} + For all $n,m \in \naturals$ we have $(n \rmul m) \in \naturals$. +\end{axiom} + +\begin{axiom}\label{naturals_add_is_closed_in_n} + For all $n,m \in \naturals$ we have $(n + m) \in \naturals$. +\end{axiom} + +\subsubsection{Natural numbers as ordinals} + + +\begin{lemma}\label{nat_is_successor_ordinal} + Let $n\in\naturals$. + Suppose $n\neq \emptyset$. + Then $n$ is a successor ordinal. +\end{lemma} +\begin{proof} + Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$. + $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}. + Now $M\subseteq \naturals\subseteq M$ + by \cref{subseteq,naturals_smallest_inductive_set}. + Thus $M = \naturals$. + Follows by \cref{subseteq}. +\end{proof} + +\begin{lemma}\label{nat_is_transitiveset} + $\naturals$ is \in-transitive. +\end{lemma} +\begin{proof} + Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$. + $\emptyset\in M$. + For all $n\in M$ we have $\suc{n}\in M$ + by \cref{naturals_inductive_set,suc}. + Thus $M$ is an inductive set. + Now $M\subseteq \naturals\subseteq M$ + by \cref{subseteq,naturals_smallest_inductive_set}. + Hence $\naturals = M$. +\end{proof} + +\begin{lemma}\label{natural_number_is_ordinal} + Every natural number is an ordinal. \end{lemma} +\begin{proof} + Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}. +\end{proof} +\begin{lemma}\label{omega_is_an_ordinal} + $\naturals$ is an ordinal. +\end{lemma} +\begin{proof} + Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}. +\end{proof} -\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)$. +\begin{lemma}\label{omega_is_a_limit_ordinal} + $\naturals$ is a limit ordinal. +\end{lemma} +\begin{proof} + $\emptyset\precedes \naturals$. + If $n\in \naturals$, then $\suc{n}\in\naturals$. +\end{proof} + + +\subsubsection{Properties and Facts natural numbers} + +\begin{theorem}\label{induction_principle} + Let $P$ be a set. + Suppose $P \subseteq \naturals$. + Suppose $\zero \in P$. + Suppose $\forall n \in P. \suc{n} \in P$. + Then $P = \naturals$. +\end{theorem} +\begin{proof} + Trivial. +\end{proof} + +\begin{proposition}\label{existence_of_suc} + Let $n \in \naturals$. + Suppose $n \neq \zero$. + Then there exist $n' \in \naturals$ such that $\suc{n'} = n$. +\end{proposition} +\begin{proof} + Follows by \cref{transitiveset,nat_is_transitiveset,suc_intro_self,successor_ordinal,nat_is_successor_ordinal}. +\end{proof} + +\begin{proposition}\label{suc_eq_plus_one} + Let $n \in \naturals$. + Then $\suc{n} = n + 1$. +\end{proposition} +\begin{proof} + Let $P = \{ n \in \naturals \mid n + 1 = 1 + n \}$. + $\zero \in P$. + It suffices to show that if $m \in P$ then $\suc{m} \in P$. +\end{proof} + +\begin{proposition}\label{naturals_1_kommu} + Let $n \in \naturals$. + Then $1 + n = n + 1$. +\end{proposition} +\begin{proof} + Follows by \cref{suc_eq_plus_one,naturals_addition_axiom_2,naturals_addition_axiom_1,naturals_inductive_set,one_is_suc_zero}. +\end{proof} + +\begin{proposition}\label{naturals_add_kommu} + For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$. +\end{proposition} +\begin{proof} + Fix $n \in \naturals$. + Let $P = \{ m \in \naturals \mid m + n = n + m \}$. + It suffices to show that $P = \naturals$. + $P \subseteq \naturals$. + $\zero \in P$. + It suffices to show that if $m \in P$ then $\suc{m} \in P$. +\end{proof} + +\begin{proposition}\label{naturals_add_assoc} + Suppose $n,m,k \in \naturals$. + Then $n + (m + k) = (n + m) + k$. +\end{proposition} +\begin{proof} + Let $P = \{ k \in \naturals \mid \text{for all $n',m' \in \naturals$ we have $n' + (m' + k) = (n' + m') + k$}\}$. + $P \subseteq \naturals$. + $\zero \in P$. + It suffices to show that for all $k \in P$ we have $\suc{k} \in P$. + Fix $k \in P$. + It suffices to show that for all $n' \in \naturals$ we have for all $m' \in \naturals$ we have $n' + (m' + \suc{k}) = (n' + m') + \suc{k}$. + Fix $n' \in \naturals$. + Fix $m' \in \naturals$. + \begin{align*} + (n' + m') + \suc{k} \\ + &= \suc{(n' + m') + k} \\ + &= \suc{n' + (m' + k)} \\ + &= n' + \suc{(m' + k)} \\ + &= n' + (m' + \suc{k}) + \end{align*} +\end{proof} + +\begin{proposition}\label{naturals_rmul_one_left} + For all $n \in \naturals$ we have $1 \rmul n = n$. +\end{proposition} +\begin{proof} + Fix $n \in \naturals$. + \begin{align*} + 1 \rmul n \\ + &= \suc{\zero} \rmul n \\ + &= (\zero \rmul n) + n \\ + &= (\zero) + n \\ + &= n + \end{align*} +\end{proof} + +\begin{proposition}\label{naturals_add_remove_brakets} + Suppose $n,m,k \in \naturals$. + Then $(n + m) + k = n + m + k = n + (m + k)$. +\end{proposition} + +\begin{proposition}\label{naturals_add_remove_brakets2} + Suppose $n,m,k,l \in \naturals$. + Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$. +\end{proposition} + +%\begin{proposition}\label{natural_disstro_oneline} +% Suppose $n,m,k \in \naturals$. +% Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. +%\end{proposition} +%\begin{proof} +% Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. +% $\zero \in P$. +% $P \subseteq \naturals$. +% It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. +% Fix $n \in P$. +% It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +% Fix $m' \in \naturals$. +% Fix $k' \in \naturals$. +% $n \in \naturals$. +% $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + m' + k' = (((n \rmul m') + (n \rmul k')) + m') + k' = (m' + ((n \rmul m') + (n \rmul k'))) + k' = ((m' + (n \rmul m')) + (n \rmul k')) + k' = (((n \rmul m') + m') + (n \rmul k')) + k' = ((n \rmul m') + m') + ((n \rmul k') + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +%\end{proof} + +\begin{proposition}\label{natural_disstro} + Suppose $n,m,k \in \naturals$. + Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. +\end{proposition} +\begin{proof} + %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. + Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$. + + $\zero \in P$. + $P \subseteq \naturals$. + It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. + Fix $n \in P$. + + It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. + Fix $m' \in \naturals$. + Fix $k' \in \naturals$. + $n \in \naturals$. + \begin{align*} + \suc{n} \rmul (m' + k') \\ + &= (n \rmul (m' + k')) + (m' + k') \\% \explanation{by \cref{naturals_mul_axiom_2}}\\ + &= ((n \rmul m') + (n \rmul k')) + (m' + k') \\%\explanation{by assumption}\\ + &= ((n \rmul m') + (n \rmul k')) + m' + k' \\%\explanation{by \cref{naturals_add_remove_brakets,naturals_add_kommu}}\\ + &= (((n \rmul m') + (n \rmul k')) + m') + k' \\%\explanation{by \cref{naturals_add_kommu,naturals_add_remove_brakets,naturals_add_assoc}}\\ + &= (m' + ((n \rmul m') + (n \rmul k'))) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\ + &= ((m' + (n \rmul m')) + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_assoc}}\\ + &= (((n \rmul m') + m') + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\ + &= ((n \rmul m') + m') + ((n \rmul k') + k') \\%\explanation{by \cref{naturals_add_assoc}}\\ + &= (\suc{n} \rmul m') + (\suc{n} \rmul k') %\explanation{by \cref{naturals_mul_axiom_2}} + \end{align*} +\end{proof} + +\begin{proposition}\label{naturals_rmul_one_kommu} + For all $n \in \naturals$ we have $n \rmul 1 = n$. +\end{proposition} +\begin{proof} + Let $P = \{ n \in \naturals \mid n \rmul 1 = n\}$. + $1 \in P$. + It suffices to show that for all $n' \in P$ we have $\suc{n'} \in P$. + Fix $n' \in P$. + It suffices to show that $\suc{n'} \rmul 1 = \suc{n'}$. + \begin{align*} + \suc{n'} \rmul 1 \\ + &= n' \rmul 1 + 1 \\ + &= n' + 1 \\ + &= \suc{n'} + \end{align*} +\end{proof} + +\begin{proposition}\label{naturals_rmul_kommu} + Let $n, m \in \naturals$. + Then $n \rmul m = m \rmul n$. +\end{proposition} +\begin{proof} + Let $P = \{n \in \naturals \mid \forall m \in \naturals. n \rmul m = m \rmul n\}$. + $\zero \in P$. + $P \subseteq \naturals$. + It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. + Fix $n \in P$. + It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul m = m \rmul \suc{n}$. + Fix $m \in \naturals$. + $n \rmul m = m \rmul n$. + \begin{align*} + \suc{n} \rmul m \\ + &= (n \rmul m) + m \\ + &= (m \rmul n) + m \\ + &= m + (m \rmul n) \\ + &= (m \rmul 1) + (m \rmul n) \\ + &= m \rmul (1 + n) \\ + &= m \rmul \suc{n} \\ + \end{align*} +\end{proof} + +\begin{proposition}\label{naturals_rmul_assoc} + Suppose $n,m,k \in \naturals$. + Then $n \rmul (m \rmul k) = (n \rmul m) \rmul k$. +\end{proposition} +\begin{proof} + Let $P = \{ n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m \rmul k) = (n \rmul m) \rmul k$ }\}$. + $\zero \in P$. + It suffices to show that for all $n' \in P$ we have $ \suc{n'} \in P$. + Fix $n' \in P$. + It suffices to show that for all $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n'} \rmul (m' \rmul k') = (\suc{n'} \rmul m') \rmul k'$. + Fix $m' \in \naturals$. + Fix $k' \in \naturals$. + \begin{align*} + \suc{n'} \rmul (m' \rmul k') \\ + &=(n' \rmul (m' \rmul k')) + (m' \rmul k') \\ + &=((n' \rmul m') \rmul k') + (m' \rmul k') \\ + &=(k' \rmul (n' \rmul m')) + (k' \rmul m') \\ + &=k' \rmul ((n' \rmul m') + m') \\ + &=k' \rmul (\suc{n'} \rmul m') \\ + &=(\suc{n'} \rmul m') \rmul k' + \end{align*} +\end{proof} + +\begin{lemma}\label{naturals_is_equal_to_two_times_naturals} + $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$. +\end{lemma} + + +\subsection{Axioms of the reals Part One} +We seen before that we can proof the common behavior of the naturals. +Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals. +Such that we can introduce the integers and raitionals as smooth as possible. + + + +The operations Multiplication and addition is closed in the reals +\begin{axiom}\label{reals_rmul} + For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$. \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$. +\begin{axiom}\label{reals_add} + For all $n,m \in \reals$ we have $(n + m) \in \reals$. \end{axiom} -\begin{axiom}\label{reals_axiom_zero_in_reals} - $\zero \in \reals$. + + + +Commutivatiy of the standart operations +\begin{axiom}\label{reals_axiom_kommu} + For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$. \end{axiom} +\begin{axiom}\label{reals_axiom_assoc} + For all $x,y,z \in \reals$ we have $(x + y) + z = x + (y + z)$. +\end{axiom} + + +Existence of one and Zero \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$. + For all $x \in \reals$ we have $x \rmul 1 = x$. \end{axiom} + + +The Existence of Inverse of both operations \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$. + For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$. \end{axiom} + + +Disstrubitiv Laws of the reals \begin{axiom}\label{reals_axiom_disstro1} - For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$. + For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$. +\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{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} +Definition of the order symbols +\begin{abbreviation}\label{rless} + $x < y$ iff $x \rless y$. +\end{abbreviation} + +\begin{abbreviation}\label{less_on_reals} + $x \leq y$ iff $x < y \lor x = y$. +\end{abbreviation} + +\begin{abbreviation}\label{greater_on_reals} + $x > y$ iff $y < x$. +\end{abbreviation} + +\begin{abbreviation}\label{greatereq_on_reals} + $x \geq y$ iff $y \leq x$. +\end{abbreviation} + + + +Laws of the order on the reals +\begin{abbreviation}\label{is_positiv} + $x$ is positiv iff $x > \zero$. +\end{abbreviation} + +\begin{axiom}\label{reals_order} + For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$. +\end{axiom} + +\begin{axiom}\label{reals_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_is_eta_zero_set} 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_one_bigger_zero} + $\zero < 1$. +\end{axiom} + +\begin{axiom}\label{reals_order_behavior_with_addition} + 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{reals_postiv_mul_is_positiv} + For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. +\end{axiom} + +\begin{axiom}\label{reals_postiv_mul_negativ_is_negativ} + For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$. +\end{axiom} + +\begin{axiom}\label{reals_negativ_mul_is_negativ} + For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$. +\end{axiom} + + + + +\subsection{The Intergers} + + +\begin{axiom}\label{neg} + For all $n \in \reals$ we have $\neg{n} \in \reals$ and $n + \neg{n} = \zero$. +\end{axiom} + +\begin{axiom}\label{neg_of_zero} + $\neg{\zero} = \zero$. +\end{axiom} + +\begin{definition}\label{minus} + $n - m = n + \neg{m}$. +\end{definition} + +\begin{lemma}\label{minus_in_reals} + Suppose $n,m \in \reals$. + Then $n - m \in \reals$. +\end{lemma} +\begin{proof} + \begin{byCase} + \caseOf{$m = \zero$.} Trivial. + \caseOf{$m \neq \zero$.} Trivial. + \end{byCase} +\end{proof} + +\begin{proposition}\label{negation_of_negation_is_id} + For all $r \in \reals$ we have $\neg{\neg{r}} = r$. +\end{proposition} +\begin{proof} + Omitted. +% Fix $r \in \reals$. +% $r + \neg{r} = \zero$. +% $\neg{r} + \neg{\neg{r}} = \zero$. +% Follows by \cref{neg,reals_axiom_kommu}. +\end{proof} + +\begin{definition}\label{integers} + $\integers = \{ z \in \reals \mid \exists n \in \naturals. z \in \naturals \lor n + z = \zero\}$. +\end{definition} + +\begin{lemma}\label{n_subset_z} + $\naturals \subseteq \integers$. +\end{lemma} + +\begin{lemma}\label{neg_of_naturals_in_integers} + For all $n \in \naturals$ we have $\neg{n} \in \integers$. +\end{lemma} + +\begin{lemma}\label{integers_eq_naturals_and_negativ_naturals} + $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{abbreviation}\label{positiv_real_number} + $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$. +\end{abbreviation} + + + +\subsection{The Rationals} + +\begin{axiom}\label{invers_reals} + For all $q \in \reals$ we have $\inv{q} \rmul q = 1$. +\end{axiom} + +\begin{abbreviation}\label{rfrac} + $\rfrac{x}{y} = x \rmul \inv{y}$. +\end{abbreviation} + +\begin{abbreviation}\label{naturalsplus} + $\naturalsPlus = \naturals \setminus \{\zero\}$. +\end{abbreviation} + +\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 (\integers \setminus \{\zero\}). 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{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} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{fraction_kuerzung} %TODO: Englischen namen rausfinden + For all $n,m,k \in \reals$ we have $\rfrac{n \rmul k}{m \rmul k} = \rfrac{n}{m}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{fraction_swap} + For all $n,m,k,l \in \reals$ we have $\rfrac{\rfrac{n}{m}}{\rfrac{k}{l}}=\rfrac{n \rmul l}{m \rmul k}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{definition}\label{divisor} + $g$ is a integral divisor of $a$ iff $g \in \naturals$ and there exist $b \in \integers$ such that $g \rmul b = a$. +\end{definition} + + + + +%\begin{abbreviation}\label{gcd} +% $g$ is greatest common divisor of $\{a,b\}$ iff +% $g$ is a integral divisor of $a$ +% and $g$ is a integral divisor of $b$ +% and for all $g'$ such that $g'$ is a integral divisor of $a$ +% and $g'$ is a integral divisor of $b$ we have $g' \leq g$. +%\end{abbreviation} +% TODO: Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, + + +\subsection{Order on the reals} + +\begin{axiom}\label{reals_order_is_transitive} + For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. +\end{axiom} + + +\begin{lemma}\label{plus_one_order} + For all $r\in \reals$ we have $ r < r + 1$. +\end{lemma} +\begin{proof} + 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} + Let $x,y \in \reals$. + Suppose $x$ is positiv and $y$ is positiv. + Then $x + y$ is positiv. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{reals_mul_of_positiv} + Let $x,y \in \reals$. + Suppose $x$ is positiv and $y$ is positiv. + Then $x \rmul y$ is positiv. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + +\begin{lemma}\label{order_reals_lemma0} + For all $x \in \reals$ we have not $x < x$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + \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)$. + Let $x,y,z \in \reals$. + Suppose $\zero < x$. + Suppose $y < z$. + Then $(y \rmul x) < (z \rmul x)$. \end{lemma} +\begin{proof} + Omitted. + %There exist $k \in \reals$ such that $y + k = z$ and $k > \zero$ by \cref{reals_definition_order_def}. + %\begin{align*} + % (z \rmul x) \\ + % &= ((y + k) \rmul x) \\ + % &= ((y \rmul x) + (k \rmul x)) \explanation{by \cref{reals_disstro2}} + %\end{align*} + %Then $(k \rmul x) > \zero$. + %Therefore $(z \rmul x) > (y \rmul x)$. +\end{proof} \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)$. + Let $x,y,z \in \reals$. + Suppose $\zero < x$. + Suppose $y < z$. + Then $(x \rmul y) < (x \rmul z)$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \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)$. + Let $x,y,z \in \reals$. + Suppose $\zero > x$. + Suppose $y < z$. + Then $(x \rmul z) < (x \rmul y)$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} -\begin{lemma}\label{o4rder_reals_lemma} - For all $x,y \in \reals$ if $x > y$ then $x \geq y$. +\begin{lemma}\label{order_reals_lemma00} + For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{order_reals_lemma5} - For all $x,y \in \reals$ if $x < y$ then $x \leq y$. + For all $x,y \in \reals$ such that $x < y$ we have $x \leq y$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{order_reals_lemma6} - For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. + For all $x,y \in \reals$ such that $x \leq y \leq x$ we have $x=y$. \end{lemma} - -\begin{axiom}\label{reals_axiom_minus} - For all $x \in \reals$ $x - x = \zero$. -\end{axiom} +\begin{proof} + Omitted. +\end{proof} \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{proof} + Omitted. +\end{proof} \begin{definition}\label{upper_bound} $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$. @@ -168,6 +741,9 @@ %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{proof} + Omitted. +\end{proof} \begin{definition}\label{supremum_reals} $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$. @@ -185,11 +761,83 @@ \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{proof} + Omitted. +\end{proof} \begin{definition}\label{infimum_reals} $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$. \end{definition} +\begin{definition}\label{minimum} + $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$. +\end{definition} + + +\begin{definition}\label{maximum} + $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$. +\end{definition} + + +\begin{definition}\label{intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + + +\begin{definition}\label{intervalopen} + $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$. +\end{definition} + +\begin{definition}\label{intervalopen_infinite_left} + $\intervalopenInfiniteLeft{b} = \{ x \in \reals \mid x < b\}$. +\end{definition} + +\begin{definition}\label{intervalopen_infinite_right} + $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid x > a\}$. +\end{definition} + +\begin{definition}\label{intervalclosed_infinite_left} + $\intervalclosedInfiniteLeft{b} = \{ x \in \reals \mid x \leq b\}$. +\end{definition} + +\begin{definition}\label{intervalclosed_infinite_right} + $\intervalclosedInfiniteRight{a} = \{ x \in \reals \mid x \geq a\}$. +\end{definition} + + +\begin{definition}\label{m_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + +\begin{axiom}\label{abs_behavior1} + If $x \geq \zero$ then $\abs{x} = x$. +\end{axiom} + +\begin{axiom}\label{abs_behavior2} + If $x < \zero$ then $\abs{x} = \neg{x}$. +\end{axiom} + +\begin{definition}\label{realsminus} + $\realsminus = \{r \in \reals \mid r < \zero\}$. +\end{definition} + +\begin{definition}\label{realsplus} + $\realsplus = \{r \in \reals \mid r > \zero\}$. +\end{definition} + +\begin{definition}\label{epsilon_ball} + $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$. +\end{definition} + + + + + + + + +%\begin{proposition}\label{safe} +% Contradiction. +%\end{proposition} diff --git a/library/ordinal.tex b/library/ordinal.tex index 3063162..6f924c1 100644 --- a/library/ordinal.tex +++ b/library/ordinal.tex @@ -3,7 +3,7 @@ \import{set/powerset.tex} \import{set/regularity.tex} \import{set/suc.tex} -\import{nat.tex} +%\import{nat.tex} \section{Transitive sets} @@ -584,55 +584,56 @@ Then $\alpha\subseteq\beta$. Follows by \cref{subseteq_antisymmetric}. \end{proof} - -\subsection{Natural numbers as ordinals} - -\begin{lemma}\label{nat_is_successor_ordinal} - Let $n\in\naturals$. - Suppose $n\neq \emptyset$. - Then $n$ is a successor ordinal. -\end{lemma} -\begin{proof} - Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$. - $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}. - Now $M\subseteq \naturals\subseteq M$ - by \cref{subseteq,naturals_smallest_inductive_set}. - Thus $M = \naturals$. - Follows by \cref{subseteq}. -\end{proof} - -\begin{lemma}\label{nat_is_transitiveset} - $\naturals$ is \in-transitive. -\end{lemma} -\begin{proof} - Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$. - $\emptyset\in M$. - For all $n\in M$ we have $\suc{n}\in M$ - by \cref{naturals_inductive_set,suc}. - Thus $M$ is an inductive set. - Now $M\subseteq \naturals\subseteq M$ - by \cref{subseteq,naturals_smallest_inductive_set}. - Hence $\naturals = M$. -\end{proof} - -\begin{lemma}\label{natural_number_is_ordinal} - Every natural number is an ordinal. -\end{lemma} -\begin{proof} - Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}. -\end{proof} - -\begin{lemma}\label{omega_is_an_ordinal} - $\naturals$ is an ordinal. -\end{lemma} -\begin{proof} - Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}. -\end{proof} - -\begin{lemma}\label{omega_is_a_limit_ordinal} - $\naturals$ is a limit ordinal. -\end{lemma} -\begin{proof} - $\emptyset\precedes \naturals$. - If $n\in \naturals$, then $\suc{n}\in\naturals$. -\end{proof} +% +%\subsection{Natural numbers as ordinals} +% +%\begin{lemma}\label{nat_is_successor_ordinal} +% Let $n\in\naturals$. +% Suppose $n\neq \emptyset$. +% Then $n$ is a successor ordinal. +%\end{lemma} +%\begin{proof} +% Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$. +% $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}. +% Now $M\subseteq \naturals\subseteq M$ +% by \cref{subseteq,naturals_smallest_inductive_set}. +% Thus $M = \naturals$. +% Follows by \cref{subseteq}. +%\end{proof} +% +%\begin{lemma}\label{nat_is_transitiveset} +% $\naturals$ is \in-transitive. +%\end{lemma} +%\begin{proof} +% Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$. +% $\emptyset\in M$. +% For all $n\in M$ we have $\suc{n}\in M$ +% by \cref{naturals_inductive_set,suc}. +% Thus $M$ is an inductive set. +% Now $M\subseteq \naturals\subseteq M$ +% by \cref{subseteq,naturals_smallest_inductive_set}. +% Hence $\naturals = M$. +%\end{proof} +% +%\begin{lemma}\label{natural_number_is_ordinal} +% Every natural number is an ordinal. +%\end{lemma} +%\begin{proof} +% Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}. +%\end{proof} +% +%\begin{lemma}\label{omega_is_an_ordinal} +% $\naturals$ is an ordinal. +%\end{lemma} +%\begin{proof} +% Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}. +%\end{proof} +% +%\begin{lemma}\label{omega_is_a_limit_ordinal} +% $\naturals$ is a limit ordinal. +%\end{lemma} +%\begin{proof} +% $\emptyset\precedes \naturals$. +% If $n\in \naturals$, then $\suc{n}\in\naturals$. +%\end{proof} +%
\ No newline at end of file diff --git a/library/relation.tex b/library/relation.tex index b5aebcd..d63e747 100644 --- a/library/relation.tex +++ b/library/relation.tex @@ -422,6 +422,9 @@ \begin{proposition}\label{fld_cons} $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$. \end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} \begin{proposition}\label{fld_union} $\fld{(A\union B)} = \fld{A}\union\fld{B}$. @@ -630,6 +633,7 @@ This lets us use the same symbol for composition of functions. \begin{proof} %$x\in\dom{R}$ and $z\in\ran{S}$. There exists $y$ such that $x\mathrel{R} y\mathrel{S} z$ by \cref{circ,pair_eq_iff}. + Follows by assumption. \end{proof} \begin{proposition}\label{circ_iff} diff --git a/library/set.tex b/library/set.tex index 2fd18ea..69b9526 100644 --- a/library/set.tex +++ b/library/set.tex @@ -654,6 +654,9 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio Suppose $(A\inter B)\union C = A\inter (B\union C)$. Then $C\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{union_upper_right,union_upper_left,subseteq_union_iff,subseteq_antisymmetric,subseteq_inter_iff}. +\end{proof} % From Isabelle/ZF equalities theory \begin{proposition}\label{union_inter_crazy} diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex index a846b78..a922052 100644 --- a/library/set/equinumerosity.tex +++ b/library/set/equinumerosity.tex @@ -15,7 +15,7 @@ $A\approx A$. \end{proposition} \begin{proof} - $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}. + $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}. Follows by \cref{equinum}. \end{proof} diff --git a/library/topology/basis.tex b/library/topology/basis.tex index 6fa9fbd..f0f77e4 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -2,7 +2,7 @@ \import{set.tex} \import{set/powerset.tex} -\subsection{Topological basis} +\subsection{Topological basis}\label{form_sec_topobasis} \begin{abbreviation}\label{covers} $C$ covers $X$ iff @@ -56,24 +56,52 @@ $\emptyset \in \genOpens{B}{X}$. \end{lemma} -\begin{lemma}\label{all_is_in_genopens} + + +\begin{lemma}\label{union_in_genopens} Assume $B$ is a topological basis for $X$. - $X \in \genOpens{B}{X}$. + Assume $F\subseteq \genOpens{B}{X}$. + Then $\unions{F}\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}$. + We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}. + + Show for all $x\in \unions{F}$ there exists $W \in B$ + such that $x\in W$ and $W \subseteq \unions{F}$. + \begin{subproof} + Fix $x \in \unions{F}$. + There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}. + $V \in \genOpens{B}{X}$. + There exists $W \in B$ such that $x \in W \subseteq V$. + Then $W \subseteq \unions{F}$. + \end{subproof} + Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}. \end{proof} -\begin{lemma}\label{union_in_genopens} +\begin{lemma}\label{basis_is_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}$. + $B \subseteq \genOpens{B}{X}$. \end{lemma} \begin{proof} - Omitted. + We show for all $V \in B$ $V \in \genOpens{B}{X}$. + \begin{subproof} + Fix $V \in B$. + For all $x \in V$ $x \in V \subseteq V$. + $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $V \in \pow{X}$. + $V \in \genOpens{B}{X}$. + \end{subproof} \end{proof} +\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{inters_in_genopens} Assume $B$ is a topological basis for $X$. @@ -92,16 +120,13 @@ Then $x\in A,C$. There exists $V' \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}. There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}. - There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$. + There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$ by \cref{topological_basis}. 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''$. \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}$. + $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}. \end{proof} diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex new file mode 100644 index 0000000..95c4d0a --- /dev/null +++ b/library/topology/continuous.tex @@ -0,0 +1,41 @@ +\import{topology/topological-space.tex} +\import{relation.tex} +\import{function.tex} +\import{set.tex} + +\subsection{Continuous}\label{form_sec_continuous} + +\begin{definition}\label{continuous} + $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. +\end{definition} + +\begin{proposition}\label{continuous_definition_by_closeds} + Let $X$ be a topological space. + Let $Y$ be a topological space. + Let $f \in \funs{X}{Y}$. + Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. +\end{proposition} +\begin{proof} + Omitted. + %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ we have $\preimg{f}{U} \in \closeds{X}$. + %\begin{subproof} + % Suppose $f$ is continuous. + % Fix $U \in \closeds{Y}$. + % $\carrier[Y] \setminus U$ is open in $Y$. + % Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$. + % Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$. + % We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % \begin{subproof} + % It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$. + % Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + % Take $y \in \carrier[Y]$ such that $f(x)=y$. + % It suffices to show that $y \in U$. + % \end{subproof} + % $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + %\end{subproof} + %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} + diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 1c6a0ca..031aa0f 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -4,7 +4,7 @@ \import{set/powerset.tex} \import{topology/basis.tex} -\section{Metric Spaces} +\section{Metric Spaces}\label{form_sec_metric} \begin{definition}\label{metric} $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and @@ -21,44 +21,16 @@ -%\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} - @@ -93,13 +65,6 @@ \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} @@ -108,45 +73,3 @@ \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/real-topological-space.tex b/library/topology/real-topological-space.tex new file mode 100644 index 0000000..db7ee94 --- /dev/null +++ b/library/topology/real-topological-space.tex @@ -0,0 +1,786 @@ +\import{set.tex} +\import{set/cons.tex} +\import{set/powerset.tex} +\import{set/fixpoint.tex} +\import{set/product.tex} +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{topology/basis.tex} +\import{numbers.tex} +\import{function.tex} + + +\section{Topology Reals}\label{form_sec_toporeals} + +\begin{definition}\label{topological_basis_reals_eps_ball} + $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. +\end{definition} + +\begin{axiom}\label{reals_carrier_reals} + $\carrier[\reals] = \reals$. +\end{axiom} + +\begin{lemma}\label{intervals_are_connected_in_reals} + Suppose $a,b \in \reals$. + Then for all $c \in \reals$ such that $a < c < b$ we have $c \in \intervalopen{a}{b}$. +\end{lemma} + +\begin{lemma}\label{epsball_are_subset_reals_elem} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \reals$. +\end{lemma} + +\begin{lemma}\label{intervalopen_iff} + Suppose $a,b,c \in \reals$. + Suppose $a < b$. + $c \in \intervalopen{a}{b}$ iff $a < c < b$. +\end{lemma} + +\begin{lemma}\label{epsball_are_subseteq_reals_set} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then $\epsBall{x}{\epsilon} \subseteq \reals$. +\end{lemma} + +\begin{lemma}\label{epsball_are_subset_reals_set} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then $\epsBall{x}{\epsilon} \subset \reals$. +\end{lemma} + +\begin{lemma}\label{reals_order_minus_positiv} + Suppose $x,y \in \reals$. + Suppose $\zero < y$. + $x - y < x$. +\end{lemma} + +\begin{lemma}\label{realsplus_bigger_zero} + For all $x \in \realsplus$ we have $\zero < x$. +\end{lemma} + +\begin{lemma}\label{realsplus_in_reals} + For all $x \in \realsplus$ we have $x \in \reals$. +\end{lemma} + +\begin{lemma}\label{epsball_are_inhabited} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then $\epsBall{x}{\epsilon}$ is inhabited. +\end{lemma} +\begin{proof} + $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}. + $x - \epsilon < x$. + $x \in \epsBall{x}{\epsilon}$. +\end{proof} + +\begin{lemma}\label{reals_elem_inbetween} + For all $a,b \in \reals$ such that $a < b$ we have there exists $c \in \reals$ such that $a < c < b$. +\end{lemma} + +\begin{lemma}\label{epsball_equal_openinterval} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then $\epsBall{x}{\epsilon} = \intervalopen{x - \epsilon}{x + \epsilon}$. +\end{lemma} + +\begin{lemma}\label{minus_behavior1} + For all $x \in \reals$ we have $x - x = \zero$. +\end{lemma} + +\begin{lemma}\label{minus_behavior2} + For all $x \in \reals$ we have $x + \neg{x} = \zero$. +\end{lemma} + +\begin{lemma}\label{minus_behavior3} + For all $x \in \reals$ we have $\neg{x} = \zero - x$. +\end{lemma} + +\begin{lemma}\label{reals_order_is_addition_with_positiv_number} + For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + + +\begin{lemma}\label{reals_order_plus_minus} + Suppose $a,b \in \reals$. + Suppose $\zero < b$. + Then $(a-b) < (a+b)$. +\end{lemma} +\begin{proof} + We show that $a < (a+b)$. + \begin{subproof} + Trivial. + \end{subproof} + We show that $(a-b) < a$. + \begin{subproof} + Trivial. + \end{subproof} +\end{proof} + +\begin{lemma}\label{epsball_are_connected_in_reals} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then for all $c \in \reals$ such that $(x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$. +\end{lemma} +\begin{proof} + $x - \epsilon \in \reals$. + $x + \epsilon \in \reals$. + + + It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$. + Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$. + $(x - \epsilon) < c < (x + \epsilon)$. +\end{proof} + +\begin{theorem}\label{topological_basis_reals_is_prebasis} + $\topoBasisReals$ is a topological prebasis for $\reals$. +\end{theorem} +\begin{proof} + We show that $\unions{\topoBasisReals} \subseteq \reals$. + \begin{subproof} + It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$. + Fix $x \in \unions{\topoBasisReals}$. + \begin{byCase} + \caseOf{$x = \emptyset$.} + Trivial. + \caseOf{$x \neq \emptyset$.} + %There exists $U \in \topoBasisReals$ such that $x \in U$. + Take $U \in \topoBasisReals$ such that $x \in U$. + Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}. + \end{byCase} + \end{subproof} + We show that $\reals \subseteq \unions{\topoBasisReals}$. + \begin{subproof} + It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$. + Fix $x \in \reals$. + $\epsBall{x}{1} \in \topoBasisReals$. + Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}. + \end{subproof} +\end{proof} + +%\begin{lemma}\label{intervl_intersection_is_interval} +% Suppose $a,b,a',b' \in \reals$. +% Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$. +% Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$. +%\end{lemma} +% + +\begin{lemma}\label{reals_order_total} + For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. + Fix $x \in \reals$. + Fix $y \in \reals$. + Omitted. +\end{proof} + +\begin{lemma}\label{topo_basis_reals_eps_iff} + $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$. +\end{lemma} + +\begin{lemma}\label{topo_basis_reals_intro} +For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$. +\end{lemma} + +\begin{lemma}\label{realsplus_in_reals_plus} + For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$. +\end{lemma} + +\begin{lemma}\label{realspuls_in_reals_minus} + For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$. +\end{lemma} + +\begin{lemma}\label{eps_ball_implies_open_interval} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. +\end{lemma} + +\begin{lemma}\label{one_in_realsplus} + $1 \in \realsplus$. +\end{lemma} + +\begin{lemma}\label{reals_existence_addition_reverse} + For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. +\end{lemma} +\begin{proof} + Fix $\delta \in \reals$. + Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}. +\end{proof} + +\begin{lemma}\label{reals_addition_minus_behavior1} + For all $a,b,c \in \reals$ such that $a = b + c$ we have $b = a - c$. +\end{lemma} +\begin{proof} + It suffices to show that for all $a \in \reals$ for all $b \in \reals$ for all $c \in \reals$ if $a = b + c$ then $b = a - c$. + Fix $a \in \reals$. + Fix $b \in \reals$. + Fix $c \in \reals$. + Suppose $a = b + c$. + Then $a + \neg{c} = b + c + \neg{c}$. + Therefore $a - c = b + c + \neg{c}$. + $a - c = (b + c) - c$. + $(b + c) - c = (b + c) + \neg{c}$. + $(b + c) + \neg{c} = b + (c + \neg{c})$. + $b + (c + \neg{c}) = b + (\zero)$. + $a - c = b$. +\end{proof} + +\begin{lemma}\label{reals_addition_minus_behavior2} + For all $a,b,c \in \reals$ such that $a = b - c$ we have $b = c + a$. +\end{lemma} + +\begin{lemma}\label{open_interval_eq_eps_ball} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. +\end{lemma} +\begin{proof} + Let $\delta = (b-a)$. + $\delta$ is positiv by \cref{minus_in_reals,minus_behavior3,reals_axiom_zero_in_reals,reals_order_behavior_with_addition,minus_behavior1,minus}. + There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. + Let $x = a + \epsilon$. + $a + \delta = b$. + $a + \epsilon + \epsilon = b$. + $x + \epsilon = b$. + $\epsilon \in \realsplus$ by \cref{reals_order_behavior_with_addition,reals_axiom_kommu,reals_axiom_zero,reals_order_is_transitive,reals_add,minus_behavior1,minus_behavior3,minus,reals_order_total,reals_axiom_zero_in_reals,realsplus}. + $a = x - \epsilon$. + $b = x + \epsilon$. + We show that $\intervalopen{a}{b} \subseteq \epsBall{x}{\epsilon}$. + \begin{subproof} + It suffices to show that for all $y \in \intervalopen{a}{b}$ we have $y \in \epsBall{x}{\epsilon}$. + Fix $y \in \intervalopen{a}{b}$. + \end{subproof} + We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$. + \begin{subproof} + It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}. + Fix $y \in \epsBall{x}{\epsilon}$. + \end{subproof} + +\end{proof} + +\begin{lemma}\label{intersection_openinterval_inclusion_of_border} + Suppose $a,b,x,y \in \reals$. + Suppose $a < b$. + Suppose $x < y$. + Suppose $a \leq x < y \leq b$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{intersection_openinterval_lower_border_eq} + Suppose $a,b,x,y \in \reals$. + Suppose $a < b$. + Suppose $x < y$. + Suppose $a = x$ and $b \leq y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{intersection_openinterval_upper_border_eq} + Suppose $a,b,x,y \in \reals$. + Suppose $a < b$. + Suppose $x < y$. + Suppose $a \leq x$ and $b = y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{intersection_openinterval_none_border_eq} + Suppose $a,b,x,y \in \reals$. + Suppose $a < b$. + Suppose $x < y$. + If $a \leq x < b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{b}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{reals_order_total2} + For all $a,b \in \reals$ we have $a < b \lor a > b \lor a = b$. +\end{lemma} + + +\begin{theorem}\label{topological_basis_reals_is_basis} + $\topoBasisReals$ is a topological basis for $\reals$. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}. + Let $B = \topoBasisReals$. + It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$. + Fix $U \in B$. + Fix $V \in B$. + It suffices to show that for all $x \in U \inter V$ there exists $W\in B$ such that $x\in W\subseteq U, V$. + Fix $x \in U \inter V$. + \begin{byCase} + \caseOf{$U \inter V = \emptyset$.} + Trivial. + \caseOf{$U \inter V \neq \emptyset$.} + Then $U \inter V$ is inhabited. + $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}. + There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$. + There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$. + Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$. + Then $ (x_2 - \beta) < x < (x_2 + \beta)$. + Let $a = (x_1 - \alpha)$. + Let $b = (x_1 + \alpha)$. + Let $c = (x_2 - \beta)$. + Let $d = (x_2 + \beta)$. + We have $a < b$ and $a < x$ and $x < b$. + We have $c < d$ and $c < x$ and $x < d$. + We have $a \in \reals$. + We have $b \in \reals$. + We have $c \in \reals$. + We have $d \in \reals$. + We show that there exist $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$. + \begin{subproof} + \begin{byCase} + \caseOf{$a < c$.} + \begin{byCase} + \caseOf{$b < d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \caseOf{$b = d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \caseOf{$b > d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \end{byCase} + \caseOf{$a = c$.} + \begin{byCase} + \caseOf{$b < d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \caseOf{$b = d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \caseOf{$b > d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}. + \end{byCase} + \caseOf{$a > c$.} + \begin{byCase} + \caseOf{$b < d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}. + \caseOf{$b = d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}. + \caseOf{$b > d$.} + Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}. + \end{byCase} + \end{byCase} + \end{subproof} + + Take $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$. + We have $a',b' \in \reals$ by assumption. + We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}. + Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$. + Then $x \in \epsBall{x'}{\epsilon'}$ by \cref{epsilon_ball}. + + Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}. + %Then $(x_1 - \alpha) < (x_2 + \beta)$. + + %Therefore $U \inter V = \intervalopen{}{(x_2 + \beta)}$. + + %We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$. + %\begin{subproof} + % Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$. + % $x \in \epsBall{x}{\delta}$. + % $\epsBall{x}{\delta} \subseteq U$. + % $\epsBall{x}{\delta} \subseteq V$. + % $\epsBall{x}{\delta} \in B$. + %\end{subproof} + %It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$. + + + %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$. + %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$. + %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$. + %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$. + %Then $ (x_2 - \beta) < x < (x_2 + \beta)$. + %\begin{byCase} + % \caseOf{$x_1 = x_2$.} + % Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$. + % \caseOf{$x_1 < x_2$.} + % \caseOf{$x_1 > x_2$.} + %\end{byCase} + %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$. + %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$. + %Then $m < x < n$. + %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$. + %\begin{subproof} + % Suppose not. + % Then For all $y \in U \inter V$ we have $x \leq y$. + %\end{subproof} + %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$. + %\begin{subproof} + % Trivial. + %\end{subproof} + \end{byCase} +\end{proof} + +\begin{axiom}\label{topological_space_reals} + $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$. +\end{axiom} + +\begin{theorem}\label{reals_is_topological_space} + $\reals$ is a topological space. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological basis for $\reals$. + Let $B = \topoBasisReals$. + We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$. + \begin{subproof} + It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$. + Fix $A \in \opens[\reals]$. + Follows by \cref{powerset_elim,topological_space_reals,genopens}. + \end{subproof} + We show that $\reals \in\opens[\reals]$. + \begin{subproof} + $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $\unions{B} \in \genOpens{B}{\reals}$. + $\reals \subseteq \unions{B}$. + \end{subproof} + We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,inters_in_genopens}. + \end{subproof} + We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,union_in_genopens}. + \end{subproof} + $\carrier[\reals] = \reals$. + Follows by \cref{topological_space}. +\end{proof} + +\begin{proposition}\label{open_interval_is_open} + Suppose $a,b \in \reals$. + Then $\intervalopen{a}{b} \in \opens[\reals]$. +\end{proposition} +\begin{proof} + If $a > b$ then $\intervalopen{a}{b} = \emptyset$. + If $a = b$ then $\intervalopen{a}{b} = \emptyset$. + It suffices to show that if $a < b$ then $\intervalopen{a}{b} \in \opens[\reals]$. + Suppose $a \rless b$. + Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. + It suffices to show that $\epsBall{x}{\epsilon} \in \opens[\reals]$. + $\topoBasisReals$ is a topological basis for $\reals$. + $\epsBall{x}{\epsilon} \in \topoBasisReals$. + $\topoBasisReals \subseteq \opens[\reals]$ by \cref{basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis}. +\end{proof} + +\begin{lemma}\label{reals_minus_to_realsplus} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $(b - a) \in \realsplus$. +\end{lemma} + +\begin{lemma}\label{existence_of_epsilon_upper_border} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. +\end{lemma} +\begin{proof} + Let $\epsilon = b - a$. + Then $\epsilon \in \realsplus$. + It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}. + Suppose not. + Then $ b \in \epsBall{a}{\epsilon}$. + Therefore $ (a - \epsilon) < b < (a + \epsilon)$. + $b = (a + \epsilon)$. + Contradiction. +\end{proof} + +\begin{lemma}\label{existence_of_epsilon_lower_border} + Suppose $a,b \in \reals$. + Suppose $a > b$. + Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. +\end{lemma} +\begin{proof} + Let $\epsilon = a - b$. + Then $\epsilon \in \realsplus$. + It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}. + Suppose not. + Then $ b \in \epsBall{a}{\epsilon}$. + Therefore $ (a - \epsilon) < b < (a + \epsilon)$. + $b = (a - \epsilon)$. + Contradiction. +\end{proof} + +\begin{proposition}\label{openinterval_infinite_left_in_opens} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteLeft{a} \in \opens[\reals]$. +\end{proposition} +\begin{proof} + Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteLeft{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta} \}$. + We show that for all $x \in \intervalopenInfiniteLeft{a}$ we have there exists $e \in E$ such that $x \in e$. + \begin{subproof} + Fix $x \in \intervalopenInfiniteLeft{a}$. + Then $x < a$. + Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$. + $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_left}. + $a \notin \epsBall{x}{\delta'}$. + $\epsBall{x}{\delta'} \in E$. + \end{subproof} + $E \subseteq \topoBasisReals$. + We show that $\unions{E} = \intervalopenInfiniteLeft{a}$. + \begin{subproof} + We show that $\unions{E} \subseteq \intervalopenInfiniteLeft{a}$. + \begin{subproof} + It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteLeft{a}$. + Fix $x \in \unions{E}$. + Take $e \in E$ such that $x \in e$ by \cref{unions_iff}. + $x \in \reals$. + Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}. + $\epsBall{x'}{\delta'} \in E$. + We show that for all $y \in e$ we have $y < a$. + \begin{subproof} + Fix $y \in e$. + Then $y \in \epsBall{x'}{\delta'}$. + $e = \epsBall{x'}{\delta'}$. + There exists $x'' \in \intervalopenInfiniteLeft{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteLeft{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Suppose not. + Take $y' \in e$ such that $y' > a$. + $x'' < a$. + $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}. + $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}. + Then $x'' < a < y'$. + Therefore $(x'' - \delta'') < a < (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_left,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq}. + Then $a \in e$ by \cref{epsball_are_connected_in_reals,intervalopen_infinite_left,neq_witness}. + Contradiction. + \end{subproof} + $x < a$. + Then $x \in \intervalopenInfiniteLeft{a}$. + \end{subproof} + We show that $\intervalopenInfiniteLeft{a} \subseteq \unions{E}$. + \begin{subproof} + Trivial. + \end{subproof} + \end{subproof} + $\unions{E} \in \opens[\reals]$ by \cref{opens_unions,reals_is_topological_space,basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis,subset_transitive}. +\end{proof} + +\begin{lemma}\label{continuous_on_basis_implies_continuous_endo} + Suppose $X$ is a topological space. + Suppose $B$ is a topological basis for $X$. + Suppose $f$ is a function from $X$ to $X$. + $f$ is continuous iff for all $b \in B$ we have $\preimg{f}{b} \in \opens[X]$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{openinterval_infinite_right_in_opens} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$. +\end{proposition} +\begin{proof} + Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteRight{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta} \}$. + We show that for all $x \in \intervalopenInfiniteRight{a}$ we have there exists $e \in E$ such that $x \in e$. + \begin{subproof} + Fix $x \in \intervalopenInfiniteRight{a}$. + Then $a < x$. + Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$. + $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_right}. + $a \notin \epsBall{x}{\delta'}$. + $\epsBall{x}{\delta'} \in E$. + \end{subproof} + $E \subseteq \topoBasisReals$. + We show that $\unions{E} = \intervalopenInfiniteRight{a}$. + \begin{subproof} + We show that $\unions{E} \subseteq \intervalopenInfiniteRight{a}$. + \begin{subproof} + It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$. + Fix $x \in \unions{E}$. + Take $e \in E$ such that $x \in e$ by \cref{unions_iff}. + $x \in \reals$. + Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}. + $\epsBall{x'}{\delta'} \in E$. + We show that for all $y \in e$ we have $y > a$. + \begin{subproof} + Fix $y \in e$. + Then $y \in \epsBall{x'}{\delta'}$. + $e = \epsBall{x'}{\delta'}$. + There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Suppose not. + Take $y' \in e$ such that $y' < a$ by \cref{reals_order_total,intervalopen,eps_ball_implies_open_interval}. + $x'' > a$. + $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}. + $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}. + Then $x'' > a > y'$. + Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}. + Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}. + Contradiction. + \end{subproof} + $x > a$. + Then $x \in \intervalopenInfiniteRight{a}$. + \end{subproof} + We show that $\intervalopenInfiniteRight{a} \subseteq \unions{E}$. + \begin{subproof} + Trivial. + \end{subproof} + \end{subproof} + $\unions{E} \in \opens[\reals]$. + + %Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$. + %Let $f(x) = \neg{x}$ for $x \in \reals$. + %$f$ is a function from $\reals$ to $\reals$. + %We show that $f$ is continuous. + %\begin{subproof} + % It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$. + % Fix $b \in \topoBasisReals$. + % Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$. + % Let $y = \neg{x}$. + % It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}. + % It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$. + % $\preimg{f}{\epsBall{x}{\epsilon}} \subseteq \reals$. + % $\epsBall{y}{\epsilon} \subseteq \reals$ by \cref{intervalopen,subseteq,minus,epsilon_ball}. + % %It suffices to show that for all $x \in \reals$ we have $x \in \epsBall{y}{\epsilon}$ iff $x \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % %Fix $x \in \reals$. + % Let $u = (y - \epsilon)$. + % Let $v = (y + \epsilon)$. + % $u = \neg{(x - \epsilon)}$. + % $v = \neg{(x + \epsilon)}$. + % %$v - u = \epsilon + \epsilon$. + % We show that for all $z \in \epsBall{y}{\epsilon}$ we have $z \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % \begin{subproof} + % Fix $z \in \epsBall{y}{\epsilon}$. + % Then $u < z < v$. + % Let $z' = z - u$. + % Then $z = u + z'$. + % Suppose not. + % Let $h = \neg{z}$. + % $\neg{h} = \neg{\neg{z}}$. + % $\neg{h} = z$. + % Then $f(h) = \neg{h}$. + % $f(h) = z$. + % Then $z \in \preimg{f}{\{h\}}$. +% + % \end{subproof} + % We show that for all $z \in \preimg{f}{\epsBall{x}{\epsilon}}$ we have $z \in \epsBall{y}{\epsilon}$. + % \begin{subproof} + % Fix $z \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % Take $h \in \epsBall{x}{\epsilon}$ such that $f(h) = z$. + % \end{subproof} + % Follows by set extensionality. + %\end{subproof} + %$\intervalopenInfiniteLeft{a} \in \opens[\reals]$. + %We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$. + %\begin{subproof} + % Omitted. + %\end{subproof} + %Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}. +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals1} + Suppose $a,b \in \reals$. + Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$. +\end{lemma} +\begin{proof} + We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$. + \begin{subproof} + Fix $x \in \reals$. + Follows by \cref{union_intro_left,intervalopen_infinite_left,reals_order_total,reals_order_total2,union_iff,intervalopen_infinite_right,union_assoc,union_intro_right,intervalclosed}. + \end{subproof} +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals2} + Suppose $a \in \reals$. + Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$ by \cref{intervalopen_infinite_left,union_intro_left,neq_witness,intervalclosed_infinite_right,union_intro_right,union_iff}. + Trivial. +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals3} + Suppose $a \in \reals$. + Then $\reals = \intervalopenInfiniteRight{a} \union \intervalclosedInfiniteLeft{a}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have either $x \in \intervalclosedInfiniteLeft{a}$ or $x \in \intervalopenInfiniteRight{a}$. + Trivial. +\end{proof} + +\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_right} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$. +\end{lemma} +\begin{proof} + Follows by \cref{reals_order_total,inter_lower_left,intervalopen_infinite_right,order_reals_lemma6,inter_lower_right,foundation,subseteq,intervalclosed_infinite_left}. +\end{proof} + +\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteLeft{a} \inter \intervalclosedInfiniteRight{a} = \emptyset$. +\end{lemma} + +\begin{proposition}\label{closedinterval_infinite_right_in_closeds} + Suppose $a \in \reals$. + Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$. +\end{proposition} +\begin{proof} + $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{intersection_of_open_closed__infinite_intervals_open_left,reals_as_union_of_open_closed_intervals2,setminus_inter,double_relative_complement,subseteq_union_setminus,subseteq_setminus,setminus_union,setminus_disjoint,setminus_partition,setminus_subseteq,setminus_emptyset,setminus_self,setminus_setminus,double_complement_union}. +\end{proof} + +\begin{proposition}\label{closedinterval_infinite_left_in_closeds} + Suppose $a \in \reals$. + Then $\intervalclosedInfiniteLeft{a} \in \closeds{\reals}$. +\end{proposition} +\begin{proof} + $\intervalclosedInfiniteLeft{a} = \reals \setminus \intervalopenInfiniteRight{a}$. +\end{proof} + +\begin{proposition}\label{closedinterval_eq_openintervals_setminus_reals} + Suppose $a,b \in \reals$. + Then $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$. +\end{proposition} +\begin{proof} + We have $\intervalclosed{a}{b} \subseteq \reals$. + We show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + \begin{subproof} + We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + \begin{subproof} + Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$. + Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{setminus,double_complement_union}. + Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$ by \cref{union_upper_left,subseteq,union_comm,subseteq_implies_setminus_supseteq}. + Follows by \cref{inter_intro}. + \end{subproof} + We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$. + \begin{subproof} + Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ by \cref{setminus_setminus,setminus}. + Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$ by \cref{inter_lower_right,elem_subseteq,setminus_setminus}. + \end{subproof} + Follows by \cref{setminus_union}. + \end{subproof} + We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$. + \begin{subproof} + For all $x \in \intervalclosedInfiniteRight{a}$ we have $x \geq a$. + For all $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ we have $x \geq a$. + Follows by set extensionality. + \end{subproof} + $\reals \setminus \intervalopenInfiniteRight{b} = \intervalclosedInfiniteLeft{b}$. + It suffices to show that $\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a} = \intervalclosed{a}{b}$. + For all $x \in \intervalclosed{a}{b}$ we have $a \leq x \leq b$. + For all $x \in (\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a})$ we have $a \leq x \leq b$. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{closedinterval_is_closed} + Suppose $a,b \in \reals$. + Then $\intervalclosed{a}{b} \in \closeds{\reals}$. +\end{proposition} +\begin{proof} + We have $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$. + It suffices to show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$ by \cref{closeds,setminus_subseteq,powerset_intro,closed_minus_open_is_closed,opens_type,subseteq_refl,union_open,is_closed_in,reals_carrier_reals,setminus_self,emptyset_open,reals_is_topological_space,openinterval_infinite_left_in_opens,openinterval_infinite_right_in_opens}. +\end{proof} diff --git a/library/topology/separation.tex b/library/topology/separation.tex index f70cb50..aaa3907 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -1,5 +1,7 @@ \import{topology/topological-space.tex} +\import{set.tex} +\subsection{Separation}\label{form_sec_separation} % T0 separation \begin{definition}\label{is_kolmogorov} @@ -73,14 +75,30 @@ \begin{proposition}\label{teeone_implies_singletons_closed} Let $X$ be a \teeone-space. - Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. + Assume $x \in \carrier[X]$. + Then $\{x\}$ is closed in $X$. \end{proposition} \begin{proof} Omitted. - % TODO - % Choose for every y distinct from x and open subset U_y containing y but not x. - % The union U of all the U_y is open. - % {x} is the complement of U in \carrier[X]. + %Let $V = \{ U \in \opens[X] \mid x \notin U\}$. + %For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$ by \cref{carrier_open,teeone}. + %For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. + % + %$\unions{V} \in \opens[X]$. + %For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$. + %We show that $\carrier[X] \setminus \{x\} = \unions{V}$. + %\begin{subproof} + % We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$. + % \begin{subproof} + % Fix $y \in \carrier[X] \setminus \{x\}$. + % $y \neq x$. + % $y \in \carrier[X]$. + % $y \in \unions{V}$. + % \end{subproof} + % For all $y \in \unions{V}$ we have $y \notin \{x\}$. + % For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. + % Follows by set extensionality. + %\end{subproof} \end{proof} % % Conversely, if \{x\} is open, then for any y distinct from x we can use @@ -120,5 +138,146 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - Omitted. % TODO + We show that for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $U\ni x\notin V$ and $V\ni y\notin U$. + \begin{subproof} + $X$ is hausdorff. + For all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. + \end{subproof} +\end{proof} + +\begin{definition}\label{is_regular} + $X$ is regular iff for all $C,p$ such that $p \in \carrier[X]$ and $p \notin C \in \closeds{X}$ we have there exists $U,C \in \opens[X]$ such that $p \in U$ and $C \subseteq V$ and $U \inter V = \emptyset$. +\end{definition} + +\begin{abbreviation}\label{regular_space} + $X$ is a regular space iff $X$ is a topological space and $X$ is regular. +\end{abbreviation} + + +\begin{abbreviation}\label{teethree} + $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ . +\end{abbreviation} + +\begin{abbreviation}\label{teethree_space} + $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . +\end{abbreviation} + +\begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + Suppose $X$ is \teethree\ . + For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. +\end{proposition} +\begin{proof} + Omitted. + %%Suppose $X$ is regular and kolmogorov. + %Fix $U \in \opens[X]$. + %Fix $x \in U$. + %Let $C = \carrier[X] \setminus U$. + %Then $C \in \closeds{X}$. + %$x \notin C$. + %$x \in \carrier[X]$. + %We show that there exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$. + %We show that $B \subseteq (\carrier[X] \setminus A)$. + %$(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$. + %$(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$. + %$x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$. + %Let $N = (\carrier[X] \setminus A)$. + %Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$. + %$N \in \neighbourhoods{x}{X}$. +\end{proof} + +\begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. +\end{proposition} +\begin{proof} + We show that if $X$ is \teethree\ then for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. + \begin{subproof} + %For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. + Omitted. + \end{subproof} + + We show that if for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$ then $X$ is \teethree\ . + \begin{subproof} + Omitted. + \end{subproof} \end{proof} + + +\begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. +\end{proposition} +\begin{proof} + Omitted. + %Follows by \cref{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods,teethree_implies_closed_neighbourhood_in_open}. +\end{proof} + + +\begin{proposition}\label{teethree_space_is_teetwo_space} + Let $X$ be a \teethree-space. + Suppose $X$ is inhabited. + Then $X$ is a \teetwo-space. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + For all $x,y \in \carrier[X]$ such that $x \neq y$ we have $x \notin \{y\}$. + It suffices to show that $X$ is hausdorff. + It suffices to show that for all $x \in \carrier[X]$ we have for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$. + Fix $x \in \carrier[X]$. + It suffices to show that for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$. + Fix $y \in \carrier[X]$. + + + We show that there exist $U,V,C$ such that $U,V \in \opens[X]$ and $C\in \closeds{X}$ and $x \in U$ and $y \in C \subseteq V$ and $U$ is disjoint from $V$. + \begin{subproof} + There exist $C' \in \closeds{X}$ such that $x \in \carrier[X]$ and $x \notin C' \in \closeds{X}$ and there exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$. + There exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$. + $U'$ is disjoint from $V'$. + $x \in U'$. + $x \notin C' \subseteq V'$. + $U',V' \in \opens[X]$. + $C' \in \closeds{X}$. + We show that there exist $K \in \closeds{X}$ such that $x \notin K \ni y$. + \begin{subproof} + $X$ is Kolmogorov. + For all $x',y'\in\carrier[X]$ such that $x'\neq y'$ there exist $H\in\opens[X]$ such that $x'\in H\not\ni y'$ or $x'\notin H\ni y'$. + we show that there exist $H \in \opens[X]$ such that $x \notin H \ni y$ or $y \notin H \ni x$. + \begin{subproof} + Omitted. + \end{subproof} + $H \subseteq \carrier[X]$ by \cref{opens_type,subseteq}. + Since $\carrier[X] \ni x \notin H$ or $\carrier[X] \ni y \notin H$, we have there exist $c \in H$. + Then $H \neq \carrier[X]$. + Since $y \in H$ or $x \in H$, we have $H \neq \emptyset$. + Let $K = \carrier[X] \setminus H$. + $K$ is inhabited. + $K \in \closeds{X}$ by \cref{complement_of_open_is_closed}. + $x \notin K \ni y$ or $y \notin K \ni x$. + \begin{byCase} + \caseOf{$y \in K$.} Trivial. + \caseOf{$y \notin K$.} + Then there exist $U'',V'' \in \opens[X]$ such that $x \in U''$ and $K \subseteq V''$ and $U'' \inter V'' = \emptyset$ by \cref{is_regular}. + Let $K' = \carrier[X] \setminus U''$. + $x \in K'$. + $K' \in \closeds{X}$. + \end{byCase} + + + \end{subproof} + + Follows by assumption. + \end{subproof} + $y \in V$ by assumption. + Follows by assumption. + + +%\end{proof} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 55bc253..409e107 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -1,7 +1,8 @@ \import{set.tex} \import{set/powerset.tex} +\import{set/cons.tex} -\section{Topological spaces} +\section{Topological spaces}\label{form_sec_topospaces} \begin{struct}\label{topological_space} A topological space $X$ is a onesorted structure equipped with @@ -67,7 +68,8 @@ such that $a\in U\subseteq A$. \end{proposition} \begin{proof} - Take $U\in\interiors{A}{X}$ such that $a\in U$. + Omitted. + %Take $U\in\interiors{A}{X}$ such that $a\in U$. \end{proof} \begin{proposition}[Interior]\label{interior_elem_iff} @@ -161,10 +163,22 @@ \begin{proposition}\label{carrier_is_closed} Let $X$ be a topological space. - Then $\emptyset$ is closed in $X$. + Then $\carrier[X]$ is closed in $X$. \end{proposition} \begin{proof} $\carrier[X]\setminus \carrier[X] = \emptyset$. + Follows by \cref{emptyset_open,is_closed_in}. +\end{proof} + +\begin{proposition}\label{opens_minus_closed_is_open} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Suppose $B$ is closed in $X$. + Then $A \setminus B$ is open in $X$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_eq_emptyset_iff_subseteq,is_closed_in,opens_inter,inter_comm_left,setminus_union,inter_assoc,inter_setminus,inter_lower_left,inter_lower_right,setminus_subseteq,double_complement,setminus_setminus,setminus_eq_inter_complement,setminus_self,setminus_inter,union_comm,emptyset_subseteq,setminus_partition}. \end{proof} \begin{definition}[Closed sets]\label{closeds} @@ -216,31 +230,282 @@ Follows by \cref{inters_singleton,closure}. \end{proof} +\begin{proposition}\label{subseteq_inters_iff_to_right} + Let $A,F$ be sets. + Suppose $A \subseteq \inters{F}$. + Then for all $X \in F$ we have $A \subseteq X$. +\end{proposition} + -\begin{proposition}%[Complement of interior equals closure of complement] -\label{complement_interior_eq_closure_complement} +\begin{proposition}\label{subseteq_of_all_then_subset_of_union} + Let $A,F$ be sets. + Suppose $F$ is inhabited. %TODO: Remove!! + Suppose for all $X \in F$ we have $A \subseteq X$. + Then $A \subseteq \unions{F}$. +\end{proposition} +\begin{proof} + There exist $X \in F$ such that $X \subseteq \unions{F}$. + $A \subseteq X \subseteq \unions{F}$. +\end{proof} + + + +\begin{proposition}\label{subseteq_inters_iff_to_left} + Let $A,F$ be sets. + Suppose $F$ is inhabited. % TODO:Remove!! + Suppose for all $X \in F$ we have $A \subseteq X$. + Then $A \subseteq \inters{F}$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.}Trivial. + \caseOf{$A \neq \emptyset$.} + $F$ is inhabited. + It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. + Fix $a \in A$. + For all $X \in F$ we have $a \in X$. + $A \subseteq \unions{F}$. + $a \in \unions{F}$. + \end{byCase} +\end{proof} + +\begin{proposition}\label{subseteq_inters_iff_new} + Suppose $F$ is inhabited. + $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$. +\end{proposition} + +\begin{proposition}\label{set_is_subseteq_to_closure_of_the_set} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + $A \subseteq \closure{A}{X}$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.} + Trivial. + \caseOf{$A \neq \emptyset$.} + We show that $\carrier[X] \in \closures{A}{X}$. + \begin{subproof} + $\carrier[X]$ is closed in $X$. + $\carrier[X] \in \pow{\carrier[X]}$. + \end{subproof} + $\closures{A}{X}$ is inhabited. + For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$. + Therefore $A \subseteq \inters{\closures{A}{X}}$. + \end{byCase} +\end{proof} + +\begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. +\end{proposition} +\begin{proof} + It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$. + If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$ by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,elem_subseteq,setminus}. + Follows by \cref{subseteq_setminus_cons_elim,cons_absorb,double_complement_union,union_as_unions,set_is_subseteq_to_closure_of_the_set,setminus_subseteq,setminus_intro,closure,setminus_elim_left}. +\end{proof} + +\begin{proposition}\label{complement_of_closed_is_open} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Suppose $A$ is closed in $X$. + Then $\carrier[X] \setminus A$ is open in $X$. +\end{proposition} + +\begin{proposition}\label{complement_of_open_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Then $\carrier[X] \setminus A$ is closed in $X$. +\end{proposition} + +\begin{proposition}\label{intersection_of_closed_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ are closed in $X$. + Suppose $B$ are closed in $X$. + Then $A \inter B$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. + $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) \in \opens[X]$. + $A \inter B = \carrier[X] \setminus ((\carrier[X] \setminus A) \union (\carrier[X] \setminus B))$. +\end{proof} + +\begin{proposition}\label{union_of_closed_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ are closed in $X$. + Suppose $B$ are closed in $X$. + Then $A \union B$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. + $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) \in \opens[X]$. + $A \union B = \carrier[X] \setminus ((\carrier[X] \setminus A) \inter (\carrier[X] \setminus B))$. +\end{proof} + +\begin{proposition}\label{closed_minus_open_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Suppose $B$ is closed in $X$. + Then $B \setminus A$ is closed in $X$. +\end{proposition} + + + +\begin{proposition}\label{intersection_of_closed_is_closed_infinite} + Let $X$ be a topological space. + Suppose $F \subseteq \pow{\carrier[X]}$. + Suppose for all $A \in F$ we have $A$ is closed in $X$. + Suppose $F$ is inhabited. + Then $\inters{F}$ is closed in $X$. +\end{proposition} +\begin{proof} + Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $. + For all $Y \in F'$ we have $Y$ is open in $X$. + $\unions{F'}$ is open in $X$. + $\unions{F'}, \inters{F} \subseteq \carrier[X]$. + We show that $\inters{F} = \carrier[X] \setminus (\unions{F'})$. + \begin{subproof} + We show that for all $a \in \inters{F}$ we have $a \in \carrier[X] \setminus (\unions{F'})$. + \begin{subproof} + Fix $a \in \inters{F}$. + $a \in \carrier[X]$. + For all $A \in F$ we have $a \in A$. + For all $A \in F$ we have $a \notin (\carrier[X] \setminus A)$. + Then $a \notin \unions{F'}$. + Therefore $a \in \carrier[X] \setminus (\unions{F'})$. + \end{subproof} + We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$. + \begin{subproof} + \begin{byCase} + \caseOf{$\inters{F} = \emptyset$.} + $F$ is inhabited. + Take $U$ such that $U \in F$. + Let $F'' = F \setminus \{U\}$. + There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$. + Omitted. + \caseOf{$\inters{F} \neq \emptyset$.} + + Fix $a \in \carrier[X] \setminus (\unions{F'})$. + $\inters{F}$ is inhabited. + $a \in \carrier[X]$. + $a \notin \unions{F'}$. + For all $A \in F'$ we have $a \notin A$. + For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$. + For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$ by \cref{setminus_setminus,inter_absorb_supseteq_left,pow_iff,subseteq}. + For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$. + For all $Y \in F$ we have $a \in Y$. + Therefore $a \in \inters{F}$. + \end{byCase} + \end{subproof} + Follows by set extensionality. + \end{subproof} + Follows by \cref{complement_of_open_is_closed}. +\end{proof} + +\begin{proposition}\label{closure_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\closure{A}{X}$ is closed in $X$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$\closure{A}{X} = \emptyset$.} + Trivial. + \caseOf{$\closure{A}{X} \neq \emptyset$.} + $\closures{A}{X}$ is inhabited. + $\closures{A}{X} \subseteq \pow{\carrier[X]}$. + For all $B \in \closures{A}{X}$ we have $B$ is closed in $X$. + $\inters{\closures{A}{X}}$ is closed in $X$. + \end{byCase} +\end{proof} + + + +\begin{proposition}\label{closure_is_minimal_closed_set} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + For all $Y \in \closeds{X}$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$. +\end{proposition} +\begin{proof} + Follows by \cref{closure,closeds,inters_subseteq_elem,closures}. +\end{proof} + +\begin{proposition}\label{interior_is_maximal} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$. +\end{proposition} + +\begin{proposition}\label{complement_interior_eq_closure_complement} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - Omitted. % Use general De Morgan's Law in Pow|X| + We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$. + \begin{subproof} + + Fix $x \in \carrier[X]\setminus\interior{A}{X}$. + Suppose not. + $x \notin \closure{(\carrier[X]\setminus A)}{X}$. + $x \in \carrier[X]$. + $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$. + $x \in A$. + $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$. + $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. + There exist $U \in \opens[X]$ such that $x \in U$ and $U\subseteq A$. + $U \subseteq \interior{A}{X}$. + Contradiction. + \end{subproof} + $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$. + $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. \end{proof} + + \begin{definition}[Frontier]\label{frontier} $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. \end{definition} +\begin{proposition}\label{closure_interior_frontier_is_in_carrier} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$. +\end{proposition} + +\begin{proposition}\label{frontier_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\frontier{A}{X}$ is closed in $X$. +\end{proposition} +\begin{proof} + $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ by \cref{closure_interior_frontier_is_in_carrier,closure_is_closed,interior_is_open,closed_minus_open_is_closed}. +\end{proof} + +\begin{proposition}\label{setdifference_eq_intersection_with_complement} + Suppose $A,B \subseteq C$. + Then $A \setminus B = A \inter (C \setminus B)$. +\end{proposition} -\begin{proposition}%[Frontier as intersection of closures] -\label{frontier_as_inter} + +\begin{proposition}\label{frontier_as_inter} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - % TODO - Omitted. - %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition) - %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement - %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement + \begin{align*} + \frontier{A}{X} \\ + &= \closure{A}{X}\setminus\interior{A}{X} \\ + &= \closure{A}{X} \inter (\carrier[X] \setminus \interior{A}{X}) \explanation{by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}}\\ + &= \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X} \explanation{by \cref{complement_interior_eq_closure_complement}} + \end{align*} \end{proof} \begin{proposition}\label{frontier_of_emptyset} @@ -264,3 +529,7 @@ \begin{definition}\label{neighbourhoods} $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$. \end{definition} + +\begin{definition}\label{neighbourhoods_set} + $\neighbourhoodsSet{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\subseteq U\subseteq N\}$. +\end{definition} diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex new file mode 100644 index 0000000..cd85fbc --- /dev/null +++ b/library/topology/urysohn.tex @@ -0,0 +1,924 @@ +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{topology/basis.tex} +\import{numbers.tex} +\import{function.tex} +\import{set.tex} +\import{cardinal.tex} +\import{relation.tex} +\import{relation/uniqueness.tex} +\import{set/cons.tex} +\import{set/powerset.tex} +\import{set/fixpoint.tex} +\import{set/product.tex} + +\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1} +% In this section we want to proof Urysohns lemma. +% We try to follow the proof of Klaus Jänich in his book. TODO: Book reference +% The Idea is to construct staircase functions as a chain. +% The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$. +% With the property that \[f\mid_{A}=1 \land f\mid_{B}=0\] for \[A,B\] closed sets. + +%Chains of sets. + +This is the first attempt to prove Urysohns Lemma with the usage of struct. + +\subsection{Chains of sets} +% Assume $A,B$ are subsets of a topological space $X$. + +% As Jänich propose we want a special property on chains of subsets. +% We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. +% \begin{align} +% A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B +% \end{align} +% such that for all elements in this chain following holds, +% $\overline{A_{i-1}} \subset \interior{A_{i}}$. +% In this case we call the chain legal. + +\begin{definition}\label{urysohnone_one_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + + + +%%----------------------- +% Idea: +% A sequence could be define as a family of sets, +% together with the existence of an indexing function. +% +%%----------------------- +\begin{struct}\label{urysohnone_sequence} + A sequence $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\indexx$ + \item $\indexxset$ + + \end{enumerate} + such that + \begin{enumerate} + \item\label{urysohnone_indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$. + \item\label{urysohnone_index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$. + \end{enumerate} +\end{struct} + +% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen + + + + +\begin{definition}\label{urysohnone_cahin_of_subsets} + $C$ is a chain of subsets iff + $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$. +\end{definition} + +\begin{definition}\label{urysohnone_chain_of_n_subsets} + $C$ is a chain of $n$ subsets iff + $C$ is a chain of subsets and $n \in \indexxset[C]$ + and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$. +\end{definition} + + + +% TODO: The Notion above should be generalised to sequences since we need them as well for our limit +% and also for the subproof of continuity of the limit. + + +% \begin{definition}\label{urysohnone_legal_chain} +% $C$ is a legal chain of subsets of $X$ iff +% $C \subseteq \pow{X}$. %and +% %there exist $f \in \funs{C}{\naturals}$ such that +% %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$. +% \end{definition} + +% TODO: We need a notion for declarinf new properties to existing thing. +% +% The following gives a example and a wish want would be nice to have: +% "A (structure) is called (adjectiv of property), if" +% +% This should then be use als follows: +% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). +% Which should be translated to fol like this: +% ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X) +% --------------------------------------------------------------- + + + +\subsection{staircase function} + +\begin{definition}\label{urysohnone_minimum} + $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$. +\end{definition} + +\begin{definition}\label{urysohnone_maximum} + $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$. +\end{definition} + +\begin{definition}\label{urysohnone_intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + +\begin{definition}\label{urysohnone_intervalopen} + $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$. +\end{definition} + + +\begin{struct}\label{urysohnone_staircase_function} + A staircase function $f$ is a onesorted structure equipped with + \begin{enumerate} + \item $\chain$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{urysohnone_staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$. + \item \label{urysohnone_staircase_domain} $\dom{f}$ is a topological space. + \item \label{urysohnone_staricase_def_chain} $C$ is a chain of subsets. + \item \label{urysohnone_staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. + \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. + \item \label{urysohnone_staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. + \item \label{urysohnone_staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$. + \item \label{urysohnone_staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ + such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{urysohnone_legal_staircase} + $f$ is a legal staircase function iff + $f$ is a staircase function and + for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$. +\end{definition} + +\begin{abbreviation}\label{urysohnone_urysohnspace} + $X$ is a urysohn space iff + $X$ is a topological space and + for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$ + we have there exist $A',B' \in \opens[X]$ + such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. +\end{abbreviation} + +\begin{definition}\label{urysohnone_urysohnchain} + $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused! + $C$ is a chain of subsets and + for all $A \in C$ we have $A \subseteq X$ and + for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$. +\end{definition} + +\begin{definition}\label{urysohnone_urysohnchain_without_cardinality} + $C$ is a urysohnchain in $X$ iff + $C$ is a chain of subsets and + for all $A \in C$ we have $A \subseteq X$ and + for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$. +\end{definition} + +\begin{abbreviation}\label{urysohnone_infinte_sequence} + $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite. +\end{abbreviation} + +\begin{definition}\label{urysohnone_infinite_product} + $X$ is the infinite product of $Y$ iff + $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$. +\end{definition} + +\begin{definition}\label{urysohnone_refinmant} + $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$ + and for all $x \in C$ we have $x \in C'$ + and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$ + and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$. +\end{definition} + +\begin{abbreviation}\label{urysohnone_two} + $\two = \suc{1}$. +\end{abbreviation} + +\begin{lemma}\label{urysohnone_two_in_reals} + $\two \in \reals$. +\end{lemma} + +\begin{lemma}\label{urysohnone_two_in_naturals} + $\two \in \naturals$. +\end{lemma} + +\begin{inductive}\label{urysohnone_power_of_two} + Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$. + \begin{enumerate} + \item $(\zero, 1) \in \powerOfTwoSet$. + \item If $(m,k) \in \powerOfTwoSet$, then $(m+1, k \rmul \two) \in \powerOfTwoSet$. + \end{enumerate} +\end{inductive} + +\begin{abbreviation}\label{urysohnone_pot} + $\pot = \powerOfTwoSet$. +\end{abbreviation} + +\begin{lemma}\label{urysohnone_dom_pot} + $\dom{\pot} = \naturals$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{urysohnone_ran_pot} + $\ran{\pot} \subseteq \naturals$. +\end{lemma} + + +\begin{axiom}\label{urysohnone_pot1} + $\pot \in \funs{\naturals}{\naturals}$. +\end{axiom} + +\begin{axiom}\label{urysohnone_pot2} + For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$. + %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$. +\end{axiom} + + +%Without this abbreviation \pot cant be sed as a function in the standard sense +\begin{abbreviation}\label{urysohnone_pot_as_function} + $\pot(n) = \apply{\pot}{n}$. +\end{abbreviation} + +%Take all points, besids one but then take all open sets not containing x but all other, so \{x\} has to be closed +\begin{axiom}\label{urysohnone_hausdorff_implies_singltons_closed} + For all $X$ such that $X$ is Hausdorff we have + for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$. +\end{axiom} + + +\begin{lemma}\label{urysohnone_urysohn_set_in_between} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \subset B$. + %Suppose $B \union A \neq \carrier[X]$. + There exist $C \in \closeds{X}$ + such that $A \subset C \subset B$ or $A, B \in \opens[X]$. +\end{lemma} +\begin{proof} + We have $B \setminus A$ is inhabited. + Take $x$ such that $x \in (B \setminus A)$. + Then $A \subset (A \union \{x\})$. + Let $C = \closure{A \union \{x\}}{X}$. + We have $(A \union \{x\}) \subseteq \closure{A \union \{x\}}{X}$. + Therefore $A \subset C$. + $A \subseteq B \subseteq \carrier[X]$. + $x \in B$. + Therefore $x \in \carrier[X]$. + $(A \union \{x\}) \subseteq \carrier[X]$. + We have $\closure{A \union \{x\}}{X}$ is closed in $X$ by \cref{closure_is_closed}. + Therefore $C$ is closed in $X$ by \cref{closure_is_closed}. + \begin{byCase} + \caseOf{$C = B$.} + %We have $\carrier[X] \setminus A$ is open in $X$. + %We have $\carrier[X] \setminus B$ is open in $X$. + %$\{x\}$ is closed in $X$.% by \cref{hausdorff_implies_singltons_closed}. + %$A \union \{x\} = C$. + %$\carrier[X] \setminus (A \union \{x\}) = (\carrier[X] \setminus C)$. + %$\carrier[X] \setminus (A) = \{x\} \union (\carrier[X] \setminus C)$. + + + %Therefore $\{x\}$ is open in $X$. + Omitted. + \caseOf{$C \neq B$.} + Omitted. + \end{byCase} + +\end{proof} + + +\begin{proposition}\label{urysohnone_urysohnchain_induction_begin} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \inter B$ is empty. + Then there exist $U$ + such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ + and $\indexxset[U]= \{\zero, 1\}$ + and $\indexx[U](\zero) = A$ + and $\indexx[U](1) = (\carrier[X] \setminus B)$. + %$U$ is a urysohnchain in $X$. +\end{proposition} +\begin{proof} + + Omitted. + + % We show that $U$ is a sequence. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $A \subseteq (\carrier[X] \setminus B)$. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $U$ is a chain of subsets. + % \begin{subproof} + % For all $n \in \indexxset[U]$ we have $n = \zero \lor n = 1$. + % It suffices to show that for all $n \in \indexxset[U]$ we have + % for all $m \in \indexxset[U]$ such that + % $n < m$ we have $\indexx[U](n) \subseteq \indexx[U](m)$. + % Fix $n \in \indexxset[U]$. + % Fix $m \in \indexxset[U]$. + % \begin{byCase} + % \caseOf{$n = 1$.} Trivial. + % \caseOf{$n = \zero$.} + % \begin{byCase} + % \caseOf{$m = \zero$.} Trivial. + % \caseOf{$m = 1$.} Omitted. + % \end{byCase} + % \end{byCase} + % \end{subproof} +% + % $A \subseteq X$. + % $(X \setminus B) \subseteq X$. + % We show that for all $x \in U$ we have $x \subseteq X$. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % We show that for all $n,m \in \indexxset[U]$ such that $n < m$ we have + % $\closure{\indexx[U](n)}{X} \subseteq \interior{\indexx[U](m)}{X}$. + % \begin{subproof} + % Omitted. + % \end{subproof} + + +\end{proof} + +\begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \inter B$ is empty. + Suppose there exist $U$ + such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ + and $\indexxset[U]= \{\zero, 1\}$ + and $\indexx[U](\zero) = A$ + and $\indexx[U](1) = (\carrier[X] \setminus B)$. + Then $U$ is a urysohnchain in $X$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + + + +\begin{proposition}\label{urysohnone_t_four_propositon} + Let $X$ be a urysohn space. + Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$ + we have there exists $C \subseteq X$ such that + $\closure{A}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{B}{X}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + + + +\begin{proposition}\label{urysohnone_urysohnchain_induction_step_existence} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain in $X$. + Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$. +\end{proposition} +\begin{proof} + % U = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n}) + % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ... A_{n-1}, A'_{n}, A_{n}) + + % Let $m = \max{\indexxset[U]}$. + % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$. + + + %\begin{definition}\label{urysohnone_refinmant} + % $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and + % for all $y \in C$ such that $y \subset x$ + % we have there exist $c \in C'$ such that $y \subset c \subset x$ + % and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$. + %\end{definition} + Omitted. + +\end{proof} + + + + + +\begin{proposition}\label{urysohnone_existence_of_staircase_function} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$. + Suppose $k \neq \zero$. + Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ + we have $f(x) = \rfrac{n}{k}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{abbreviation}\label{urysohnone_refinment_abbreviation} + $x \refine y$ iff $x$ is a refinmant of $y$. +\end{abbreviation} + + + + + +\begin{abbreviation}\label{urysohnone_sequence_of_functions} + $f$ is a sequence of functions iff $f$ is a sequence + and for all $g \in \carrier[f]$ we have $g$ is a function. +\end{abbreviation} + +\begin{abbreviation}\label{urysohnone_sequence_in_reals} + $s$ is a sequence of real numbers iff $s$ is a sequence + and for all $r \in \carrier[s]$ we have $r \in \reals$. +\end{abbreviation} + + + +\begin{axiom}\label{urysohnone_abs_behavior1} + If $x \geq \zero$ then $\abs{x} = x$. +\end{axiom} + +\begin{axiom}\label{urysohnone_abs_behavior2} + If $x < \zero$ then $\abs{x} = \neg{x}$. +\end{axiom} + +\begin{abbreviation}\label{urysohnone_converge} + $s$ converges iff $s$ is a sequence of real numbers + and $\indexxset[s]$ is infinite + and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have + there exist $N \in \indexxset[s]$ such that + for all $m \in \indexxset[s]$ such that $m > N$ + we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$. +\end{abbreviation} + + +\begin{definition}\label{urysohnone_limit_of_sequence} + $x$ is the limit of $s$ iff $s$ is a sequence of real numbers + and $x \in \reals$ and + for all $\epsilon \in \reals$ such that $\epsilon > \zero$ + we have there exist $n \in \indexxset[s]$ such that + for all $m \in \indexxset[s]$ such that $m > n$ + we have $\abs{x - \indexx[s](n)} < \epsilon$. +\end{definition} + +\begin{proposition}\label{urysohnone_existence_of_limit} + Let $s$ be a sequence of real numbers. + Then $s$ converges iff there exist $x \in \reals$ + such that $x$ is the limit of $s$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{definition}\label{urysohnone_limit_sequence} + $x$ is the limit sequence of $f$ iff + $x$ is a sequence and $\indexxset[x] = \dom{f}$ and + for all $n \in \indexxset[x]$ we have + $\indexx[x](n) = f(n)$. +\end{definition} + +\begin{definition}\label{urysohnone_realsminus} + $\realsminus = \{r \in \reals \mid r < \zero\}$. +\end{definition} + +\begin{abbreviation}\label{urysohnone_realsplus} + $\realsplus = \reals \setminus \realsminus$. +\end{abbreviation} + +\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $\intervalclosed{a}{b} \subseteq \reals$. +\end{proposition} + + + +\begin{lemma}\label{urysohnone_fraction1} + Let $x \in \reals$. + Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{urysohnone_frection2} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $\intervalopen{a}{b}$ is infinite. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{urysohnone_frection3} + Suppose $a \in \reals$. + Suppose $a < \zero$. + Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{urysohnone_fraction4} + Suppose $a,b,\epsilon \in \reals$. + Suppose $\epsilon > \zero$. + $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{urysohnone_fraction5} + Suppose $a,b,\epsilon \in \reals$. + Suppose $\epsilon > \zero$. + $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{urysohnone_fraction6} + Suppose $a,\epsilon \in \reals$. + Suppose $\epsilon > \zero$. + $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $. +\end{proposition} + +\begin{abbreviation}\label{urysohnone_epsilonball} + $\epsBall{a}{\epsilon} = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$. +\end{abbreviation} + +\begin{proposition}\label{urysohnone_fraction7} + Suppose $a,\epsilon \in \reals$. + Suppose $\epsilon > \zero$. + Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + + + + +%\begin{definition}\label{urysohnone_sequencetwo} +% $Z$ is a sequencetwo iff $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$. +%\end{definition} +% +%\begin{proposition}\label{urysohnone_sequence_existence} +% Suppose $N \subseteq \naturals$. +% Suppose $M \subseteq \naturals$. +% Suppose $N = M$. +% Then there exist $Z,f$ such that $f$ is a bijection from $N$ to $M$ and $Z=(N,f,M)$ and $Z$ is a sequencetwo. +%\end{proposition} +%\begin{proof} +% Let $f(x) = x$ for $x \in N$. +% Let $Z=(N,f,M)$. +%\end{proof} +%The proposition above and the definition prove false together with +% ordinal_subseteq_unions, omega_is_an_ordinal, powerset_intro, in_irrefl + + + + + + + + + +\begin{theorem}\label{urysohnone_urysohn1} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \inter B$ is empty. + Suppose $\carrier[X]$ is inhabited. + There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous. +\end{theorem} +\begin{proof} + + There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ + and $\indexxset[\eta] = \{\zero, 1\}$ + and $\indexx[\eta](\zero) = A$ + and $\indexx[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnone_urysohnchain_induction_begin}. + + We show that there exist $\zeta$ such that $\zeta$ is a sequence + and $\indexxset[\zeta] = \naturals$ + and $\eta \in \carrier[\zeta]$ and $\indexx[\zeta](\eta) = \zero$ + and for all $n \in \indexxset[\zeta]$ we have $n+1 \in \indexxset[\zeta]$ + and $\indexx[\zeta](n+1)$ is a refinmant of $\indexx[\zeta](n)$. + \begin{subproof} + %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$. + %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$. + % + % % TODO: Proof that \beta is a function which would be used for the indexing. + %For all $n \in \naturals$ we have there exist $x \in \alpha$ such that $(n,x) \in \beta$. + %$\dom{\beta} = \naturals$. + %$\ran{\beta} = \alpha$. + %$\beta \in \funs{\naturals}{\alpha}$. + %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$. + Omitted. + \end{subproof} + + Let $\alpha = \carrier[X]$. + %Define $f : \alpha \to \naturals$ such that $f(x) =$ + %\begin{cases} + % & 1 & \text{if} x \in A \lor x \in B + % & k & \text{if} \exists k \in \naturals + %\end{cases} +% + %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that + %$k(x)$ + + %For all $n \in \naturals$ we have $\indexx[\zeta](n)$ is a urysohnchain in $X$. + + We show that for all $n \in \indexxset[\zeta]$ we have $\indexx[\zeta](n)$ has cardinality $\pot(n)$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that for all $m \in \naturals$ we have $\pot(m) \in \naturals$. + \begin{subproof} + Omitted. + \end{subproof} + + +% We show that for all $m \in \indexxset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ +% and for all $n \in \indexxset[\indexx[\zeta](m)]$ we have for all $x \in \indexx[\indexx[\zeta](m)](n)$ such that $x \notin \indexx[\indexx[\zeta](m)](n-1)$ +% we have $f(x) = \rfrac{n}{\pot(m)}$. +% \begin{subproof} +% Fix $m \in \indexxset[\zeta]$. +% %$\indexx[\zeta](m)$ is a urysohnchain in $X$. +% +% %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$ +% %\begin{cases} +% % & 0 & \text{if} x \in A +% % & 1 & \text{if} x \in B +% % & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \indexx[\indexx[\zeta](m)](n) \land x \notin \indexx[\indexx[\zeta](m)](n-1) +% %\end{cases} +%% +% Omitted. +% \end{subproof} +% +% +% +% %The sequenc of the functions +% Let $\gamma = \{ +% (n,f) \mid +% n \in \naturals \mid +% +% \forall n' \in \indexxset[\indexx[\zeta](n)]. +% \forall x \in \carrier[X]. +% +% +% f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land +% +% +% % (n,f) \in \gamma <=> \phi(n,f) +% % with \phi (n,f) := +% % (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n ) +% % \/ (x \notin A_k for all k \in {1,..,n} ==> f(x) = 1 +% +% ( (n' = \zero) +% \land (x \in \indexx[\indexx[\zeta](n)](n')) +% \land (f(x)= \zero) ) +% +% \lor +% +% ( (n' > \zero) +% \land (x \in \indexx[\indexx[\zeta](n)](n')) +% \land (x \notin \indexx[\indexx[\zeta](n)](n'-1)) +% \land (f(x) = \rfrac{n'}{\pot(n)}) ) +% +% \lor +% +% ( (x \notin \indexx[\indexx[\zeta](n)](n')) +% \land (f(x) = 1) ) +% +% \}$. +% +% Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. +% +% We show that for all $n \in \naturals$ we have $\gamma(n)$ +% is a function from $\carrier[X]$ to $\reals$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% +% We show that for all $n \in \naturals$ we have $\gamma(n)$ +% is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $\gamma$ is a function from $\naturals$ to $\reals$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \indexx[\indexx[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} = \rfrac{k}{\pot(n)}$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. +% \begin{subproof} +% Fix $n \in \naturals$. +% Fix $x \in \carrier[X]$. +% Omitted. +% \end{subproof} +% +% +% +% We show that +% if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ +% then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% +% +% We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +% \begin{subproof} +% We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +% \begin{subproof} +% Fix $x \in \carrier[X]$. +% +% Omitted. +% +% % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. +% %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. +% \end{subproof} +% Omitted. +% \end{subproof} +% +% +% Let $G(x) = g(x)$ for $x \in \carrier[X]$. +% We have $\dom{G} = \carrier[X]$. +% +% We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$. +% \begin{subproof} +% %Fix $x \in \dom{G}$. +% %It suffices to show that $g(x) \in \reals$. +%% +% %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +%% +% %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$. +% %\begin{subproof} +% % Fix $\epsilon \in \reals$. +% % +%% +% %\end{subproof} +% %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}. +% Omitted. +% \end{subproof} +% +% We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. +% \begin{subproof} +% %Fix $x \in \dom{G}$. +% %Then $x \in \carrier[X]$. +% %\begin{byCase} +% % \caseOf{$x \in A$.} +% % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$. +%% +%% +% % \caseOf{$x \notin A$.} +% % \begin{byCase} +% % \caseOf{$x \in B$.} +% % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. +%% +% % \caseOf{$x \notin B$.} +% % Omitted. +% % \end{byCase} +% %\end{byCase} +% Omitted. +% \end{subproof} +% +% +% We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. +% \begin{subproof} +% %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}. +% %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$. +% %Fix $x \in \dom{G}$. +% %Then $x \in \carrier[X]$. +% %$g(x) = G(x)$. +% %We have $G(x) \in \reals$. +% %$\zero \leq G(x) \leq 1$. +% %We have $G(x) \in \intervalclosed{\zero}{1}$ . +% Omitted. +% \end{subproof} +% +% We show that $G(A) = \zero$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $G(B) = 1$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $G$ is continuous. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% %Suppose $\eta$ is a urysohnchain in $X$. +% %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ +% %and $\indexxset[\eta] = \{\zero, 1\}$ +% %and $\indexx[\eta](\zero) = A$ +% %and $\indexx[\eta](1) = (X \setminus B)$. +% +% +% %Then $\eta$ is a urysohnchain in $X$. +% +% % Take $P$ such that $P$ is a infinite sequence and $\indexxset[P] = \naturals$ and for all $i \in \indexxset[P]$ we have $\indexx[P](i) = \pow{X}$. +% % +% % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence +% % and for all $i \in \indexxset[\zeta]$ we have +% % $\indexx[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ +% % and $A \subseteq \indexx[\zeta](i)$ +% % and $\indexx[\zeta](i) \subseteq (X \setminus B)$ +% % and for all $j \in \indexxset[\zeta]$ such that +% % $j < i$ we have for all $x \in \indexx[\zeta](j)$ we have $x \in \indexx[\zeta](i)$. +% % \begin{subproof} +% % Omitted. +% % \end{subproof} +% % +% % +% % + % + % + % + % + % + % We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % $g$ is a staircase function and $\chain[g] = C$. + % $g$ is a legal staircase function. + % + % + % We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + % and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + % \begin{subproof} + % Omitted. + % \end{subproof} + + + % We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. + % \begin{subproof} + % Omitted. + % \end{subproof} + + % Proof Sheme Idea: + % -We proof for n=1 that C_{n} is a chain and legal + % -Then by induction with P(n+1) is refinmant of P(n) + % -Therefore we have a increing refinmant of these Chains such that our limit could even apply + % --------------------------------------------------------- + + % We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function + % \begin{subproof} + % Omitted. + % \end{subproof} + + + % Formalization idea of enumarted sequences: + % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} + % - This should give all finite and infinte enumarable sequences + % - Introduce a notion for the indexing of these enumarable sequences. + % - Then we can define the limit of a enumarted sequence of functions. + % --------------------------------------------------------- + % + % Here we need a limit definition for sequences of functions + % We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F(A) = 1$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F(B) = 0$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F$ is continuous. + % \begin{subproof} + % Omitted. + % \end{subproof} +\end{proof} +% +%\begin{theorem}\label{urysohnone_safe} +% Contradiction. +%\end{theorem} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex new file mode 100644 index 0000000..a1a3ba0 --- /dev/null +++ b/library/topology/urysohn2.tex @@ -0,0 +1,989 @@ +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{topology/basis.tex} +\import{numbers.tex} +\import{function.tex} +\import{set.tex} +\import{cardinal.tex} +\import{relation.tex} +\import{relation/uniqueness.tex} +\import{set/cons.tex} +\import{set/powerset.tex} +\import{set/fixpoint.tex} +\import{set/product.tex} +\import{topology/real-topological-space.tex} +\import{set/equinumerosity.tex} + +\section{Urysohns Lemma}\label{form_sec_urysohn} + + + + +\begin{definition}\label{sequence} + $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$. +\end{definition} + + +\begin{abbreviation}\label{urysohnspace} + $X$ is a urysohn space iff + $X$ is a topological space and + for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$ + we have there exist $A',B' \in \opens[X]$ + such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. +\end{abbreviation} + + +\begin{abbreviation}\label{at} + $\at{f}{n} = f(n)$. +\end{abbreviation} + + +\begin{definition}\label{chain_of_subsets} + $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $n < m$ we have $\at{X}{n} \subseteq \at{X}{m}$. +\end{definition} + + +\begin{definition}\label{urysohnchain}%<-- zulässig + $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$. +\end{definition} + +\begin{definition}\label{urysohn_finer_set} + $A$ is finer between $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$. +\end{definition} + +\begin{definition}\label{finer} %<-- verfeinerung + $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$. +\end{definition} + +\begin{definition}\label{follower_index} + $y$ follows $x$ in $I$ iff $x < y$ and $x,y \in I$ and for all $i \in I$ such that $x < i$ we have $y \leq i$. +\end{definition} + +\begin{definition}\label{finer_smallest_step} + $Y$ is a minimal finer extention of $X$ in $U$ iff $Y$ is finer then $X$ in $U$ and for all $x_1,x_2 \in \dom{X}$ such that $x_1$ follows $x_2$ in $\dom{X}$ we have there exist $y \in \dom{Y}$ such that $y$ follows $x_1$ in $\dom{X}$ and $x_2$ follows $y$ in $\dom{X}$. +\end{definition} + +\begin{definition}\label{sequence_of_reals} + $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$. +\end{definition} + + +\begin{definition}\label{pointwise_convergence} + $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$. +\end{definition} + + +\begin{proposition}\label{iff_sequence} + Suppose $X$ is a function. + Suppose $\dom{X} \subseteq \naturals$. + Then $X$ is a sequence. +\end{proposition} + +\begin{definition}\label{lifted_urysohn_chain} + $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$. +\end{definition} + +\begin{definition}\label{normal_ordered_urysohnchain} + $U$ is normal ordered iff there exist $n \in \naturals$ such that $\dom{U} = \seq{\zero}{n}$. +\end{definition} + +\begin{definition}\label{bijection_of_urysohnchains} + $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$. +\end{definition} + + +%\begin{definition}\label{staircase} +% $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$. +%\end{definition} + + +\begin{definition}\label{staircase_step_value1} + $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$. +\end{definition} + +\begin{definition}\label{staircase_step_value2} + $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_step_value3} + $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$. +\end{definition} + + +\begin{definition}\label{staircase2} + $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_sequence} + $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_limit_point} + $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$. +\end{definition} + +%\begin{definition}\label{staircase_limit_function} +% $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. +%\end{definition} +% +\begin{definition}\label{staircase_limit_function} + $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. +\end{definition} + + +\begin{proposition}\label{naturals_in_transitive} + $\naturals$ is a \in-transitive set. +\end{proposition} +\begin{proof} + Follows by \cref{nat_is_transitiveset}. +\end{proof} + +\begin{proposition}\label{naturals_elem_in_transitive} + If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. + %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{natural_number_is_ordinal_for_all} + For all $n \in \naturals$ we have $n$ is a ordinal. +\end{proposition} + +\begin{proposition}\label{zero_is_in_minimal} + $\zero$ is an \in-minimal element of $\naturals$. +\end{proposition} + +\begin{proposition}\label{natural_rless_eq_precedes} + For all $n,m \in \naturals$ we have $n \precedes m$ iff $n \in m$. +\end{proposition} + +\begin{proposition}\label{naturals_precedes_suc} + For all $n \in \naturals$ we have $n \precedes \suc{n}$. +\end{proposition} + +\begin{proposition}\label{zero_is_empty} + There exists no $x$ such that $x \in \zero$. +\end{proposition} +\begin{proof} + Follows by \cref{notin_emptyset}. +\end{proof} + +\begin{proposition}\label{one_is_positiv} + $1$ is positiv. +\end{proposition} + +\begin{proposition}\label{suc_of_positive_is_positive} + For all $n \in \naturals$ such that $n$ is positiv we have $\suc{n}$ is positiv. +\end{proposition} + +\begin{proposition}\label{naturals_are_positiv_besides_zero} + For all $n \in \naturals$ such that $n \neq \zero$ we have $n$ is positiv. +\end{proposition} +\begin{proof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + \begin{byCase} + \caseOf{$n = \zero$.} Trivial. + \caseOf{$n \neq \zero$.} + Take $k \in \naturals$ such that $\suc{k} = n$. + \end{byCase} +\end{proof} + + + +\begin{proposition}\label{naturals_sum_eq_zero} + For all $n,m \in \naturals$ we have if $n+m = \zero$ then $n = m = \zero$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{no_natural_between_n_and_suc_n} + For all $n,m \in \naturals$ we have not $n < m < \suc{n}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_is_zero_one_or_greater} + $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_one_zero_or_greater} + For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$. +\end{proposition} +\begin{proof} + Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}. +\end{proof} + +\begin{proposition}\label{naturals_rless_existence_of_lesser_natural} + For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + + \begin{byCase} + \caseOf{$n = \zero$.} + + We show that for all $m \in \naturals$ such that $m < n$ we have there exist $k \in \naturals$ such that $m + k = n$. + \begin{subproof}[Proof by \in-induction on $m$] + Assume $m \in \naturals$. + \begin{byCase} + \caseOf{$m = \zero$.} + Trivial. + \caseOf{$m \neq \zero$.} + Trivial. + \end{byCase} + \end{subproof} + \caseOf{$n = 1$.} + Fix $m$. + For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$. + Then $\zero + 1 = 1$. + \caseOf{$n > 1$.} + Take $l \in \naturals$ such that $\suc{l} = n$. + Omitted. + \end{byCase} +\end{proof} + + +\begin{proposition}\label{rless_eq_in_for_naturals} + For all $n,m \in \naturals$ such that $n < m$ we have $n \in m$. +\end{proposition} +\begin{proof} + We show that for all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ we have $m \in n$. + \begin{subproof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$. + \begin{subproof}[Proof by \in-induction on $m$] + Assume $m \in \naturals$. + \begin{byCase} + \caseOf{$\suc{m}=n$.} + \caseOf{$\suc{m}\neq n$.} + \begin{byCase} + \caseOf{$n = \zero$.} + \caseOf{$n \neq \zero$.} + Take $l \in \naturals$ such that $\suc{l} = n$. + Omitted. + + \end{byCase} + \end{byCase} + \end{subproof} + \end{subproof} + + %Fix $n \in \naturals$. + + %\begin{byCase} + % \caseOf{$n = \zero$.} + % For all $k \in \naturals$ we have $k = \zero$ or $\zero < k$. + % + % \caseOf{$n \neq \zero$.} + % Fix $m \in \naturals$. + % It suffices to show that $m \in n$. + %\end{byCase} + +\end{proof} + + + +\begin{proposition}\label{naturals_leq} + For all $n \in \naturals$ we have $\zero \leq n$. +\end{proposition} + + + + +\begin{proposition}\label{naturals_leq_on_suc} + For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{x_in_seq_iff} + Suppose $n,m,x \in \naturals$. + $x \in \seq{n}{m}$ iff $n \leq x \leq m$. +\end{proposition} + +\begin{proposition}\label{seq_zero_to_n_eq_to_suc_n} + For all $n \in \naturals$ we have $\seq{\zero}{n} = \suc{n}$. +\end{proposition} +\begin{proof} [Proof by \in-induction on $n$] + Assume $n \in \naturals$. + $n \in \naturals$. + For all $m \in n$ we have $m \in \naturals$. + \begin{byCase} + \caseOf{$n = \zero$.} + It suffices to show that $1 = \seq{\zero}{\zero}$. + Follows by set extensionality. + \caseOf{$n \neq \zero$.} + Take $k$ such that $k \in \naturals$ and $\suc{k} = n$. + Then $k \in n$. + Therefore $\seq{\zero}{k} = \suc{k}$. + We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{n\}$. + \begin{subproof} + We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{n\}$. + \begin{subproof} + It suffices to show that for all $x \in \seq{\zero}{n}$ we have $x \in \seq{\zero}{k} \union \{n\}$. + $n \in \naturals$. + $\zero \leq n$. + $n \leq n$. + We have $n \in \seq{\zero}{n}$. + Therefore $\seq{\zero}{n}$ is inhabited. + Take $x$ such that $x \in \seq{\zero}{n}$. + Therefore $\zero \leq x \leq n$. + $x = n$ or $x < n$. + Then either $x = n$ or $x \leq k$. + Therefore $x \in \seq{\zero}{k}$ or $x = n$. + Follows by \cref{reals_order,natural_number_is_ordinal,ordinal_empty_or_emptyset_elem,naturals_leq_on_suc,reals_axiom_zero_in_reals,naturals_subseteq_reals,subseteq,union_intro_left,naturals_inductive_set,m_to_n_set,x_in_seq_iff,union_intro_right,singleton_intro}. + \end{subproof} + We show that $\seq{\zero}{k} \union \{n\} \subseteq \seq{\zero}{n}$. + \begin{subproof} + It suffices to show that for all $x \in \seq{\zero}{k} \union \{n\}$ we have $x \in \seq{\zero}{n}$. + $k \leq n$ by \cref{naturals_subseteq_reals,suc_eq_plus_one,plus_one_order,subseteq}. + $k \in n$. + $\seq{\zero}{k} = \suc{k}$ by assumption. + $n \in \naturals$. + $\zero \leq n$. + $n \leq n$. + We have $n \in \seq{\zero}{n}$. + Therefore $\seq{\zero}{n}$ is inhabited. + Take $x$ such that $x \in \seq{\zero}{n}$. + Therefore $\zero \leq x \leq n$. + $x = n$ or $x < n$. + Then either $x = n$ or $x \leq k$. + Therefore $x \in \seq{\zero}{k}$ or $x = n$. + Fix $x$. + \begin{byCase} + \caseOf{$x \in \seq{\zero}{k}$.} + Trivial. + \caseOf{$x = n$.} + It suffices to show that $n \in \seq{\zero}{n}$. + \end{byCase} + \end{subproof} + Trivial. + \end{subproof} + We have $\suc{n} = n \union \{n\}$. + \end{byCase} + + %Assume $n$ is a natural number. + %We show that $\seq{\zero}{\zero}$ has cardinality $1$. + %\begin{subproof} + % It suffices to show that $1 = \seq{\zero}{\zero}$. + % Follows by set extensionality. + %\end{subproof} + %It suffices to show that if $n \neq \zero$ then $\seq{\zero}{n}$ has cardinality $\suc{n}$. + %We show that for all $m \in \naturals$ such that $m \neq \zero$ we have $\seq{\zero}{m}$ has cardinality $\suc{m}$. + %\begin{subproof} + % Fix $m \in \naturals$. + % Take $k$ such that $k \in \naturals$ and $\suc{k} = m$. + % Then $k \in m$. + %\end{subproof} + + + %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$. + %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$. + %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} + +\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n} + For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$. +\end{proposition} + +\begin{proposition}\label{bijection_naturals_order} + For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{naturals_suc_injective} + Suppose $n,m \in \naturals$. + $n = m$ iff $\suc{n} = \suc{m}$. +\end{lemma} + +\begin{lemma}\label{naturals_rless_implies_not_eq} + Suppose $n,m \in \naturals$. + Suppose $n < m$. + Then $n \neq m$. +\end{lemma} + +\begin{lemma}\label{cardinality_of_singleton} + For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$. +\end{lemma} +\begin{proof} + Omitted. + %Fix $x$. + %Suppose $x \neq \emptyset$. + %Let $X = \{x\}$. + %$\seq{\zero}{\zero}=1$. + %$\seq{\zero}{\zero}$ has cardinality $1$. + %$X \setminus \{x\} = \emptyset$. + %$1 = \{\emptyset\}$. + %Let $F = \{(x,\emptyset)\}$. + %$F$ is a relation. + %$\dom{F} = X$. + %$\emptyset \in \ran{F}$. + %for all $x \in 1$ we have $x = \emptyset$. + %$\ran{F} = 1$. + %$F$ is injective. + %$F \in \surj{X}{1}$. + %$F$ is a bijection from $X$ to $1$. +\end{proof} + +\begin{lemma}\label{cardinality_n_plus_1} + For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_n_m_plus} + For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_plus_disjoint} + Suppose $X \inter Y = \emptyset$. + Suppose $X$ is finite. + Suppose $Y$ is finite. + Suppose $X$ has cardinality $n$. + Suppose $Y$ has cardinality $m$. + Then $X \union Y$ has cardinality $m+n$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $X$ is finite and $Y$ is finite. + For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + Suppose $Y$ has cardinality $n$. + $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}. + \begin{byCase} + \caseOf{$n = \zero$.} + Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}. + \caseOf{$n \neq \zero$.} + %Take $n' \in n$ such that $n = \suc{n'}$. + %$n' \in \naturals$. + %$n' + 1 = n$. + %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. + %Let $Y' = Y \setminus \{y\}$. + %$Y' \subseteq Y$. + %$Y'$ is finite. + %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Take $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Then $Y'$ has cardinality $n'$. + %Let $x' = \apply{\converse{f}}{y'}$. + %$x' \in X$. + %Let $X' = X \setminus \{x'\}$. + %$X' \subseteq X$. + %$X'$ is finite. + %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$. + %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$. + %Then $X'$ has cardinality $n'$. + %Let $f'(z)=f(z)$ for $z \in X'$. + %$\dom{f'} = X'$. + %$\ran{f'} = Y'$. + %$f'$ is a bijection from $X'$ to $Y'$. + %Let $g'(z) = g(z)$ for $z \in X'$. + %Then $g'$ is injective. + %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}. + %Define $G : X \to Y$ such that $G(z)= + %\begin{cases} + % g'(z) & \text{if} z \in X' \\ + % y' & \text{if} z = x' + %\end{cases}$ + %$G = g$. + %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}. + Omitted. + \end{byCase} + %$\converse{f}$ is a bijection from $Y$ to $X$. + %Let $h = g \circ \converse{f}$. + %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}. + %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}. +% + %Fix $y \in Y$. + %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$. + +\end{proof} + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $Y$ is finite. + Then $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof} + There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}. + Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}. +\end{proof} + + + +\begin{lemma}\label{naturals_bijection_implies_eq} + Suppose $n,m \in \naturals$. + Suppose $f$ is a bijection from $n$ to $m$. + Then $n = m$. +\end{lemma} +\begin{proof} + $n$ is finite. + $m$ is finite. + Suppose not. + Then $n < m$ or $m < n$. + \begin{byCase} + \caseOf{$n < m$.} + Then $n \in m$. + There exist $x \in m$ such that $x \notin n$. + $\identity{n}$ is a function from $n$ to $m$. + $\identity{n}$ is injective. + $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \caseOf{$m < n$.} + Then $m \in n$. + There exist $x \in n$ such that $x \notin m$. + $\converse{f}$ is a bijection from $m$ to $n$. + $\identity{m}$ is a function from $m$ to $n$. + $\identity{m}$ is injective. + $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \end{byCase} +\end{proof} + +\begin{lemma}\label{naturals_eq_iff_bijection} + Suppose $n,m \in \naturals$. + $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$. +\end{lemma} +\begin{proof} + We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$. + \begin{subproof} + Trivial. + \end{subproof} + We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$. + \begin{subproof}%[Proof by \in-induction on $k$] + %Assume $k \in \naturals$. + %\begin{byCase} + % \caseOf{$k = \zero$.} + % Trivial. + % \caseOf{$k \neq \zero$.} + % \begin{byCase} + % \caseOf{$m = \zero$.} + % Trivial. + % \caseOf{$m \neq \zero$.} + % Take $k' \in \naturals$ such that $\suc{k'} = k$. + % Then $k' \in k$. + % Take $m' \in \naturals$ such that $m = \suc{m'}$. + % Then $m' \in m$. + % + % \end{byCase} + %\end{byCase} + \end{subproof} +\end{proof} + +\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $n = m$. +\end{lemma} +\begin{proof} + We have $\seq{\zero}{n} = \suc{n}$. + Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$. + Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}. +\end{proof} + +\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $\seq{\zero}{n} = \seq{\zero}{m}$. +\end{lemma} + +\begin{proposition}\label{existence_normal_ordered_urysohn} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain of $X$. + Suppose $\dom{U}$ is finite. + Suppose $U$ is inhabited. + Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered. +\end{proposition} +\begin{proof} + Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}. + \begin{byCase} + \caseOf{$n = \zero$.} + Omitted. + \caseOf{$n \neq \zero$.} + Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. + We have $\dom{U} \subseteq \naturals$. + $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}. + $\dom{U}$ has cardinality $\suc{k}$. + We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. + \begin{subproof} + For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. + We have $\dom{U} \subseteq \naturals$. + $\dom{U}$ is inhabited. + Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}. + $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}. + %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$. + %\begin{subproof} + % We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$. + % \begin{subproof} + % It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$. + % Fix $y \in \seq{\emptyset}{k'}$. + % Then $y \leq k'$. + % Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}. + % + % Therefore $y \in \suc{k}$. + % Therefore $y \in \seq{\emptyset}{k}$. + % \end{subproof} + % We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$. + % \begin{subproof} + % Fix $y \in \seq{\emptyset}{k}$. + % \end{subproof} + %\end{subproof} + \end{subproof} + Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. + Let $N = \seq{\zero}{k}$. + Let $M = \pow{X}$. + Define $V : N \to M$ such that $V(n)= + \begin{cases} + \at{U}{F(n)} & \text{if} n \in N + \end{cases}$ + $\dom{V} = \seq{\zero}{k}$. + We show that $V$ is a urysohnchain of $X$. + \begin{subproof} + It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. + We show that $V$ is a chain of subsets in $X$. + \begin{subproof} + It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. + $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}. + It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. + Fix $n \in \dom{V}$. + Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$. + Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. + Fix $n \in \dom{V}$. + Fix $m$ such that $m \in \dom{V} \land n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + We show that $F$ is consistent on $V$ to $U$. + \begin{subproof} + It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}. + $F$ is a bijection from $\dom{V}$ to $\dom{U}$. + It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$. + Fix $n \in \dom{V}$. + Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + $V$ is normal ordered. + \end{byCase} + +\end{proof} + + +\begin{proposition}\label{staircase_ran_in_zero_to_one} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain of $X$. + Suppose $f$ is a staircase function adapted to $U$ in $X$. + Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{staircase_limit_is_continuous} + Let $X$ be a urysohn space. + Suppose $U$ is a lifted urysohnchain of $X$. + Suppose $S$ is staircase sequence of $U$ in $X$. + Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$. + Then $f$ is continuous. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{theorem}\label{urysohnsetinbeetween} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $\closure{A}{X} \subseteq \interior{B}{X}$. + Suppose $\carrier[X]$ is inhabited. + There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$. +\end{theorem} +\begin{proof} + Omitted. +\end{proof} + + +\begin{theorem}\label{induction_on_urysohnchains} + Let $X$ be a urysohn space. + Suppose $U_0$ is a sequence. + Suppose $U_0$ is a chain of subsets in $X$. + Suppose $U_0$ is a urysohnchain of $X$. + There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$. +\end{theorem} +\begin{proof} + %$U_0$ is a urysohnchain of $X$. + %It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$. + Omitted. +\end{proof} + +\begin{lemma}\label{fractions_between_zero_one} + Suppose $n,m \in \naturals$. + Suppose $m > n$. + Then $\zero \leq \rfrac{n}{m} \leq 1$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{intervalclosed_border_is_elem} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $a,b \in \intervalclosed{a}{b}$. +\end{lemma} + +\begin{lemma}\label{urysohnchain_subseteqrel} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain of $X$. + Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$. +\end{lemma} + + +\begin{theorem}\label{urysohn} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \inter B$ is empty. + Suppose $\carrier[X]$ is inhabited. + There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f$ is continuous + and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$. +\end{theorem} +\begin{proof} + Let $X' = \carrier[X]$. + Let $N = \{\zero, 1\}$. + $1 = \suc{\zero}$. + $1 \in \naturals$ and $\zero \in \naturals$. + $N \subseteq \naturals$. + Let $A' = (X' \setminus B)$. + $B \subseteq X'$ by \cref{powerset_elim,closeds}. + $A \subseteq X'$. + Therefore $A \subseteq A'$. + Define $U_0: N \to \{A, A'\}$ such that $U_0(n) = + \begin{cases} + A &\text{if} n = \zero \\ + A' &\text{if} n = 1 + \end{cases}$ + $U_0$ is a function. + $\dom{U_0} = N$. + $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. + $U_0$ is a sequence. + We have $1, \zero \in N$. + We show that $U_0$ is a chain of subsets in $X$. + \begin{subproof} + We have $\dom{U_0} \subseteq \naturals$. + We have for all $n \in \dom{U_0}$ we have $\at{U_0}{n} \subseteq \carrier[X]$ by \cref{topological_prebasis_iff_covering_family,union_as_unions,union_absorb_subseteq_left,subset_transitive,setminus_subseteq}. + We have $\dom{U_0} = \{\zero, 1\}$. + + It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$. + + Fix $n \in \dom{U_0}$. + Fix $m \in \dom{U_0}$. + + \begin{byCase} + \caseOf{$n \neq \zero$.} + Trivial. + \caseOf{$n = \zero$.} + \begin{byCase} + \caseOf{$m = \zero$.} + Trivial. + \caseOf{$m \neq \zero$.} + We have $A \subseteq A'$. + We have $\at{U_0}{\zero} = A$ by assumption. + We have $\at{U_0}{1}= A'$ by assumption. + Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,notin_emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}. + \end{byCase} + \end{byCase} + \end{subproof} + + We show that $U_0$ is a urysohnchain of $X$. + \begin{subproof} + It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $n < m$ we have $\closure{\at{U_0}{n}}{X} \subseteq \interior{\at{U_0}{m}}{X}$. + Fix $n \in \dom{U_0}$. + Fix $m \in \dom{U_0}$. + \begin{byCase} + \caseOf{$n \neq \zero$.} + Follows by \cref{ran_converse,upair_iff,one_in_reals,order_reals_lemma0,reals_axiom_zero_in_reals,reals_one_bigger_zero,reals_order}. + \caseOf{$n = \zero$.} + \begin{byCase} + \caseOf{$m = \zero$.} + Trivial. + \caseOf{$m \neq \zero$.} + Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,inhabited,notin_emptyset,subseteq,union_as_unions,natural_number_is_ordinal}. + \end{byCase} + \end{byCase} + \end{subproof} + %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain. + + We show that there exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$. + \begin{subproof} + Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}. + \end{subproof} + Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$. + + We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$. + \begin{subproof} + Omitted. + \end{subproof} + Take $S$ such that $S$ is staircase sequence of $U$ in $X$. + + %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$. +% + %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for . + We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. + \begin{subproof} + Omitted. + \end{subproof} + Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. + Then $f$ is continuous. + We show that $\dom{f} = \carrier[X]$. + \begin{subproof} + Trivial. + \end{subproof} + $f$ is a function. + We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$. + \begin{subproof} + It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$. + It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$. + Fix $x \in \dom{f}$. + $f(x)$ is the staircase limit of $S$ with $x$. + Therefore $f(x) \in \reals$. + + We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + \begin{subproof} + Fix $n \in \naturals$. + Let $g = \at{S}{n}$. + Let $U' = \at{U}{n}$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + $g$ is a staircase function adapted to $U'$ in $X$. + $U'$ is a urysohnchain of $X$. + $g$ is a function from $\carrier[X]$ to $\reals$. + It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}. + It suffices to show that for all $x \in \dom{g}$ we have $g(x) \in \intervalclosed{\zero}{1}$. + Fix $x\in \dom{g}$. + Then $x \in \carrier[X]$. + \begin{byCase} + \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.} + Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$. + We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. + \begin{subproof} + Omitted. + \end{subproof} + Therefore $x \notin (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$. + We show that $g(x) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.} + \begin{byCase} + \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.} + We show that $g(x) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + \caseOf{$x \in (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.} + Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$. + Omitted. + \end{byCase} + \end{byCase} + + + + %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + %$\at{U}{n}$ is a urysohnchain of $X$. + %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$. + %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. + %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. + %\begin{byCase} + % \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.} + % $1 \in \intervalclosed{\zero}{1}$. + % We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % Then $\apply{\at{S}{n}}{x} = 1$. + % \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.} + % %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. + % Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. + % Then $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$. + % It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$. + % $\zero \leq m' \leq k$. + %\end{byCase} + %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$. + %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$. + \end{subproof} + + Suppose not. + Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}. + For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}. + \begin{byCase} + \caseOf{$f(x) < \zero$.} + Let $\delta = \zero - f(x)$. + $\delta \in \realsplus$. + It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. + Fix $n \in \naturals$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}. + It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + Trivial. + \caseOf{$f(x) > 1$.} + Let $\delta = f(x) - 1$. + $\delta \in \realsplus$. + It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. + Fix $n \in \naturals$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}. + It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + Trivial. + \end{byCase} + + \end{subproof} + Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}. + + We show that for all $a \in A$ we have $f(a) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + We show that for all $b \in B$ we have $f(b) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + + +\end{proof} + +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} + + + + + + diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex new file mode 100644 index 0000000..74ea899 --- /dev/null +++ b/library/wunschzettel.tex @@ -0,0 +1,108 @@ +%This is just a .tex file with a wishlist of functionalitys + + +Tupel struct + +\newtheorem{struct2}[theoremcount]{Struct2} + +\begin{theorem} + %Some Theorem. +\end{theorem} +\begin{proof} + %Wish for nice Function definition. --------------------- + + %Some Proof where we need a Function. + %Privisuly defined. + $n \in \naturals$. + There is a Set $A = \{A_{0}, ..., A_{n}\}$. + For all $i$ we have $A_{i} \subseteq X$. + + Define function $f: X \to Y$, + \begin{align} + &x \mapsto \rfrac{y}{n} &; if \exists k \in \{1, ... n\}. x \in A_{k} \\ + &x \mapsto 0 &; if x \phi(x) \\ + %phi is some fol formula + + &x \mapsto \eta &; for \phi(x) and \psi(\eta) + + &x \mapsto \some_term(x)(u)(v)(w) &; \exist.u,v,w \psi(x)(u)(v)(w) \\ + % here i see the real need of varibles that can be useds in the define term + + &x \mapsto \some_else_term(x) &; else + % the else term would be great + + % the following axioms should be automaticly added. + % \dom{f} = X + % \ran{f} \subseteq Y + % f is function + + % therefor we should add the prompt for a proof that f is well defined + \end{align} + \begin{proof_well_defined} + % we need to proof that f allways maps X to Y + \end{proof_well_defined} + + % more proof but now i can use the function f + + % -------------------------------------------------------- + \begin{equation} + X= + \begin{cases} + 0, & \text{if}\ a=1 \\ + 1, & \text{otherwise} + \end{cases} + \end{equation} + + + + +\end{proof} + + +%------------------------------------------ +% My wish for a new struct +% I think this could be just get implemented along with the old struct + + +% If take we only take tupels, +% then just a list of defining fol formulas should be enougth. +\begin{struct2} + We say $(X,O)$ is a topological space if + \begin{enumerate} + \item $X$ is a set. % or X = \{...\mid .. \} or X = \naturals ... or ... + \item $O \subseteq \pow X$. + \item $\forall x,y \in O. x \union y \in O$ + \item %another formula + \item %.... + \end{enumerate} +\end{struct2} + + +% Then the proof of some thing is a structure is more easy. +% Since if we have just a tupel and some formulas which has to be fufilled, +% then we can make a proof as follows. + +\begin{struct2} + We say $(A,i,N)$ is a indexed set if + \begin{enumerate} + \item $f$ is a bijection from $N$ to $A$ + \item $N \subseteq \naturals$ + \end{enumerate} +\end{struct2} + + +\begin{theorem} + Let $A = \{ \{n\} \mid n \in \naturals \}$. + Let function $f: \naturals \to \pow{\naturals}$ such that, + \begin{algin} + \item x \mapsto \{x\} ; x \in \naturals + \end{algin} + Then $(A, f, \naturals)$ is a indexed set. +\end{theorem} +\begin{proof} + % Then we only need to proof that: + % \ran{f} = A + % \dom{f} = \naturals + % f is a bijection between $\naturals$ to $A$. +\end{proof} + diff --git a/source/Api.hs b/source/Api.hs index 95d5c8c..1bdf615 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -17,6 +17,7 @@ module Api , dumpTask , verify, ProverAnswer(..), VerificationResult(..) , exportMegalodon + , showFailedTask , WithCache(..) , WithFilter(..) , WithOmissions(..) @@ -29,6 +30,7 @@ module Api , WithParseOnly(..) , Options(..) , WithDumpPremselTraining(..) + , WithFailList(..) ) where @@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token) import UnliftIO import UnliftIO.Directory import UnliftIO.Environment +import Syntax.Abstract (Formula) -- | Follow all @\\import@ statements recursively and build a theory graph from them. -- The @\\import@ statements should be on their own separate line and precede all @@ -200,7 +203,9 @@ describeToken = \case EndEnv _ -> "end of environment" _ -> "delimiter" - +-- | gloss generates internal represantation of the LaTeX files. +-- First the file will be parsed and therefore checkt for grammer. +-- 'meaning' then transfer the raw parsed grammer to the internal semantics. gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon) gloss file = do (blocks, lexicon) <- parse file @@ -285,6 +290,17 @@ exportMegalodon file = do pure (Megalodon.encodeBlocks lexicon blocks) + +-- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use +showFailedTask :: (a, ProverAnswer) -> IO() +showFailedTask (_, Yes ) = Text.putStrLn "" +showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +--showFailedTask (_, _) = Text.putStrLn "Error!" + + -- | Should we use caching? data WithCache = WithoutCache | WithCache deriving (Show, Eq) @@ -312,6 +328,8 @@ pattern WithoutDump = WithDump "" data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq) +data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq) + data Options = Options { inputPath :: FilePath @@ -327,4 +345,5 @@ data Options = Options , withVersion :: WithVersion , withMegalodon :: WithMegalodon , withDumpPremselTraining :: WithDumpPremselTraining + , withFailList :: WithFailList } diff --git a/source/Checking.hs b/source/Checking.hs index dc90264..8bc38a4 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -28,6 +28,7 @@ import Data.HashSet qualified as HS import Data.InsOrdMap (InsOrdMap) import Data.InsOrdMap qualified as InsOrdMap import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.IO qualified as Text @@ -149,7 +150,7 @@ assume asms = traverse_ go asms go :: Asm -> Checking go = \case Asm phi -> do - phi' <- (canonicalize phi) + phi' <- canonicalize phi modify \st -> st{ checkingAssumptions = phi' : checkingAssumptions st , fixedVars = freeVars phi' <> fixedVars st @@ -542,6 +543,56 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue + DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do + -- We have f: X \to Y and x \mapsto ... + -- definition is a nonempty list of (expresssion e, formula phi) + -- such that f(x) = e if phi(x) + -- since we do a case deduction in the definition there has to be a check that, + -- our domains in the case are a disjunct union of dom(f) + assume + [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar) + ,Asm (rightUniqueAdj (TermVar funVar)) + ,Asm (relationNoun (TermVar funVar))] + + goals <- gets checkingGoals + setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)] + tellTasks + + fixed <- gets fixedVars + assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f) + assume (functionSubdomianExpression funVar argVar domVar fixed (NonEmpty.toList definitions)) --behavior on the subdomians + setGoals goals + checkProof continue + +-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..))) +-- where the phi_{i} are the subdomain statments +localFunctionGoal :: NonEmpty (Term,Formula) -> Formula +localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs + + +-- We have our list of expr and forumlas, in this case normaly someone would write +-- f(x) = ....cases +-- & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\) +-- +-- since we have to bind all globaly free Varibels we generate following asumptions. +-- +-- For x \mapsto expr(x,ys,cs) , if formula(x,ys) ; here cs are just global constants +-- -> \forall x,ys: ( formula(x,ys) => expr(x,ys,cs)) + + +functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm] +functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs +functionSubdomianExpression _ _ _ _ [] = [] + +singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> (Term, Formula) -> Asm +singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let + -- boundVar = Set.toList (freeVars expr) in + -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) + boundVar = fixedV in + let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)) + in Asm def + + checkCalc :: Calc -> Checking checkCalc calc = locally do diff --git a/source/CommandLine.hs b/source/CommandLine.hs index a9fb00d..b8c170e 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,7 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix - +import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -43,10 +43,12 @@ run = do case withDump opts of WithoutDump -> skip WithDump dir -> do + liftIO (Text.putStrLn "\ESC[1;36mCreating Dumpfiles.\ESC[0m") let serials = [dir </> show n <.> "p" | n :: Int <- [1..]] tasks <- zip serials <$> encodeTasks (inputPath opts) createDirectoryIfMissing True dir forM_ tasks (uncurry dumpTask) + liftIO (Text.putStrLn "\ESC[35mDump ready.\ESC[0m") case (withParseOnly opts, withMegalodon opts) of (WithParseOnly, _) -> do ast <- parse (inputPath opts) @@ -60,6 +62,7 @@ run = do -- A custom E executable can be configured using environment variables. -- If the environment variable is undefined we fall back to the -- a globally installed E executable. + liftIO (Text.putStrLn "\ESC[1;96mStart of verification.\ESC[0m") vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE" eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER" let prover = case withProver opts of @@ -69,23 +72,43 @@ run = do WithDefaultProver -> Provers.vampire vampirePathPath let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts) result <- verify proverInstance (inputPath opts) - liftIO case result of - VerificationSuccess -> (Text.putStrLn "Verification successful.") - VerificationFailure [] -> error "Empty verification fail" - VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of - Yes -> - skip - No tptp -> do - putStrLn "Verification failed: prover found countermodel" - Text.hPutStrLn stderr tptp - ContradictoryAxioms tptp -> do - putStrLn "Verification failed: contradictory axioms" - Text.hPutStrLn stderr tptp - Uncertain tptp -> do - putStrLn "Verification failed: out of resources" - Text.hPutStrLn stderr tptp - Error err -> - Text.hPutStrLn stderr err + case withFailList opts of + WithoutFailList -> liftIO case result of + VerificationSuccess -> putStrLn "Verification successful." + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of + Yes -> + skip + No tptp -> do + putStrLn "Verification failed: prover found countermodel" + Text.hPutStrLn stderr tptp + ContradictoryAxioms tptp -> do + putStrLn "Verification failed: contradictory axioms" + Text.hPutStrLn stderr tptp + Uncertain tptp -> do + putStrLn "Verification failed: out of resources" + Text.hPutStrLn stderr tptp + Error err tptp task -> do + putStr "Error at:" + + Text.putStrLn task + Text.putStrLn err + Text.putStrLn tptp + + WithFailList -> liftIO case result of + VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure fails -> do + putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m" + traverse_ showFailedTask fails + Text.hPutStrLn stderr "Don't give up!" + + + + + + + @@ -104,6 +127,7 @@ parseOptions = do withVersion <- withVersionParser withMegalodon <- withMegalodonParser withDumpPremselTraining <- withDumpPremselTrainingParser + withFailList <- withFailListParser pure Options{..} withTimeLimitParser :: Parser Provers.TimeLimit @@ -160,3 +184,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump withMegalodonParser :: Parser WithMegalodon withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.") <|> pure WithoutMegalodon -- Default to using the cache. + +withFailListParser :: Parser WithFailList +withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") + <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file diff --git a/source/Meaning.hs b/source/Meaning.hs index 3017c1f..9b4bc45 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -605,9 +605,22 @@ glossProof = \case if domVar == argVar then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." + + Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do + if funVar == funVar2 + then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + else error "missmatched function names" Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof + +glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) +glossLocalFunctionExprDef (definingExpression, localDomain) = do + e <- glossExpr definingExpression + d <- glossFormula localDomain + pure (e,d) + + glossCase :: Raw.Case -> Gloss Sem.Case glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof diff --git a/source/Provers.hs b/source/Provers.hs index a33f9d2..273751c 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -110,7 +110,7 @@ data ProverAnswer | No Text | ContradictoryAxioms Text | Uncertain Text - | Error Text + | Error Text Text Text deriving (Show, Eq) nominalDiffTimeToText :: NominalDiffTime -> Text @@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr = | saidNo -> No tptp | doesNotKnow -> Uncertain tptp | warned -> ContradictoryAxioms tptp - | otherwise -> Error (answer <> answerErr) + | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task))) diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 4aa8623..c8022c7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -369,6 +369,13 @@ data Proof -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/. -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument. -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function). + + + + + | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. + -- deriving (Show, Eq, Ord) -- | An inline justification. diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 3a8b3d6..4b43bc6 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -27,13 +27,15 @@ scanChunk ltoks = matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos) in case ltoks of Located{startPos = pos, unLocated = BeginEnv "definition"} : _ -> - matchOrErr definition "definition" (pos) + matchOrErr definition "definition" pos Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ -> matchOrErr abbreviation "abbreviation" pos Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ -> matchOrErr struct "struct definition" pos Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos + --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> + -- matchOrErr signatureIntro "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon @@ -85,6 +87,18 @@ abbreviation = do skipUntilNextLexicalEnv pure [lexicalItem m] +signatureIntro :: RE Token [ScannedLexicalItem] --since signiture is a used word of haskell we have to name it diffrentliy +signatureIntro = do + sym (BeginEnv "signature") + few notEndOfLexicalEnvToken + m <- label + few anySym + lexicalItem <- head + few anySym + sym (EndEnv "signature") + skipUntilNextLexicalEnv + pure [lexicalItem m] + label :: RE Token Marker label = msym \case Label m -> Just (Marker m) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index b51b738..9b947b0 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -351,8 +351,42 @@ grammar lexicon@Lexicon{..} = mdo define <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof defineFunction <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*> expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof + - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed] + + + + + -- Define $f $\fromTo{X}{Y} such that, + -- Define function $f: X \to Y$, + -- \begin{align} + -- &x \mapsto 3*x &, + -- &x \mapsto 4*k &, \forall k \in \N. x \in \Set{k} + -- \end{align} + -- + + -- Follwing is the definition right now. + -- Define function $f: X \to Y$ such that, + -- \begin{cases} + -- 1 & \text{if } x \in \mathbb{Q}\\ + -- 0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q} + -- 3 & \text{else} + -- \end{cases} + + functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) + defineFunctionLocal <- rule $ DefineFunctionLocal + <$> (_define *> beginMath *> varSymbol) -- Define $ f + <*> (_colon *> varSymbol) -- : 'var' \to 'var' + <*> (_to *> expr <* endMath <* _suchThat) + -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) + -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) + <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq ) + <*> cases (many1 functionDefineCase) <* endMath <* optional _dot + <*> proof + + + + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed] blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom @@ -436,7 +470,6 @@ enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> lab - -- This function could be rewritten, so that it can be used directly in the grammar, -- instead of with specialized variants. -- @@ -611,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...} align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a align body = begin "align*" *> body <* end "align*" +cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a +cases body = begin "cases" *> body <* end "cases" + maybeVarToken :: Located Token -> Maybe VarSymbol maybeVarToken ltok = case unLocated ltok of diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs index 135cdac..b507e7e 100644 --- a/source/Syntax/Concrete/Keywords.hs +++ b/source/Syntax/Concrete/Keywords.hs @@ -108,7 +108,7 @@ _either = word "either" ? "either" _equipped :: Prod r Text (Located Token) SourcePos _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with" _every :: Prod r Text (Located Token) SourcePos -_every = (word "every") ? "every" +_every = word "every" ? "every" _exist :: Prod r Text (Located Token) SourcePos _exist = word "there" <* word "exist" ? "there exist" _exists :: Prod r Text (Located Token) SourcePos @@ -124,7 +124,7 @@ _for = word "for" ? "for" _forAll :: Prod r Text (Located Token) SourcePos _forAll = (word "for" <* word "all") <|> word "all" ? "all" _forEvery :: Prod r Text (Located Token) SourcePos -_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every" +_forEvery = (word "for" <* word "every") <|> word "every" ? "for every" _have :: Prod r Text (Located Token) SourcePos _have = word "we" <* word "have" <* optional (word "that") ? "we have" _if :: Prod r Text (Located Token) SourcePos @@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos _in = symbol "∈" <|> command "in" ? "\\in" _subseteq :: Prod r Text (Located Token) SourcePos _subseteq = command "subseteq" ? "\\subseteq" +_to :: Prod r Text (Located Token) SourcePos +_to = command "to" ? "\\to" +_mapsto :: Prod r Text (Located Token) SourcePos +_mapsto = command "mapsto" ? "\\mapsto" +_ampersand :: Prod r Text (Located Token) SourcePos +_ampersand = symbol "&" ? "&"
\ No newline at end of file diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 44603ad..c098380 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -324,6 +324,16 @@ makeDisjunction = \case [] -> Bottom es -> List.foldl1' Or es +makeIff :: [ExprOf a] -> ExprOf a +makeIff = \case + [] -> Bottom + es -> List.foldl1' Iff es + +makeXor :: [ExprOf a] -> ExprOf a +makeXor = \case + [] -> Bottom + es -> List.foldl1' Xor es + finiteSet :: NonEmpty (ExprOf a) -> ExprOf a finiteSet = foldr cons EmptySet where @@ -436,6 +446,8 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof + | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof + deriving instance Show Proof deriving instance Eq Proof deriving instance Ord Proof diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 463dd18..4fe8730 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>) builtinIdentifiers = identifier <$> [ "emptyset" , "naturals" + , "integers" , "rationals" , "reals" , "unit" @@ -110,6 +111,8 @@ prefixOps = , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd")) , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) + , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv")) + , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index cb3f4cb..53e1e6a 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:)) Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:)) + --Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken @@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:)) Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:)) + --Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:)) Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:)) Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:)) Just t -> goMath (f . (t:)) @@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof -- | Parses a single normal mode token. tok :: Lexer (Located Token) tok = - word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command + word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command -- | Parses a single math mode token. mathToken :: Lexer (Located Token) mathToken = - var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command + var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command beginText :: Lexer (Located Token) beginText = lexeme do @@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do setMathMode pure (BeginEnv "align*") +casesBegin :: Lexer (Located Token) +casesBegin = guardM isTextMode *> lexeme do + Char.string "\\begin{cases}" + --setMathMode + pure (BeginEnv "cases") -- | Parses a single end math token. mathEnd :: Lexer (Located Token) @@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do setTextMode pure (EndEnv "align*") +casesEnd :: Lexer (Located Token) +casesEnd = guardM isMathMode *> lexeme do + Char.string "\\end{cases}" + --setTextMode + pure (EndEnv "cases") + -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on. word :: Lexer (Located Token) diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs index 705aaa5..c01c249 100644 --- a/source/Test/Golden.hs +++ b/source/Test/Golden.hs @@ -39,6 +39,7 @@ testOptions = Api.Options , withTimeLimit = Provers.defaultTimeLimit , withVersion = Api.WithoutVersion , withMegalodon = Api.WithoutMegalodon + , withFailList = Api.WithoutFailList } goldenTests :: IO TestTree diff --git a/source/TheoryGraph.hs b/source/TheoryGraph.hs index c4887ea..e49bc1f 100644 --- a/source/TheoryGraph.hs +++ b/source/TheoryGraph.hs @@ -67,12 +67,12 @@ member :: FilePath -> TheoryGraph -> Bool member n (TheoryGraph g) = Map.member n g --- | Add a node to the TheoryGraph. This is a noop if the node is already present in the graph. +-- | Add a node to the TheoryGraph. addNode :: FilePath -> TheoryGraph -> TheoryGraph addNode a (TheoryGraph g) = TheoryGraph (Map.insertWith Set.union a Set.empty g) --- | Add an edge to the TheoryGraph. This is a noop if the edge is already present in the graph. +-- | Add an edge to the TheoryGraph. This is a loop if the edge is already present in the graph. addPrecedes :: Precedes FilePath -> TheoryGraph -> TheoryGraph addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertTail e g)) where @@ -85,7 +85,9 @@ addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertT singleton :: FilePath -> TheoryGraph singleton a = TheoryGraph (Map.singleton a Set.empty) - +-- | Construct a graph, from a list of nodes and edges. +-- It takes all nodes a and add the pair (a, emptyset) to the Theorygraph, +-- afterwards it add all edges between the nodes. makeTheoryGraph :: [Precedes FilePath] -> [FilePath] -> TheoryGraph makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es where @@ -94,6 +96,8 @@ makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es {-# INLINE makeTheoryGraph #-} +-- | Construct a graph, from a list @x:xs@, +-- where @x@ is a pair of theorys @(a,b)@ with @a@ gets imported in @b@. fromList :: [Precedes FilePath] -> TheoryGraph fromList es = TheoryGraph (Map.fromListWith Set.union es') where |