From 6129ebdf0d8549f3e4d23aa771f2c06020182b7e Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Wed, 7 Aug 2024 15:28:45 +0200 Subject: Created first urysohn formalization --- library/topology/urysohn.tex | 274 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 274 insertions(+) create mode 100644 library/topology/urysohn.tex (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex new file mode 100644 index 0000000..65457ea --- /dev/null +++ b/library/topology/urysohn.tex @@ -0,0 +1,274 @@ +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{numbers.tex} +\import{function.tex} +\import{set.tex} +\import{cardinal.tex} + +\section{Urysohns Lemma} +% 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. + +The first tept will be a formalisation of chain constructions. + +\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{one_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + +\begin{definition}\label{cardinality} + $X$ has cardinality of $n$ iff + $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$. +\end{definition} + + + +\begin{struct}\label{sequence} + A sequence $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\index$ + \item $\indexset$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{cahin_of_subsets} + $C$ is a chain of subsets iff + $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. +\end{definition} + +\begin{definition}\label{chain_of_n_subsets} + $C$ is a chain of $n$ subsets iff + $C$ is a chain of subsets and $n \in \indexset[C]$ + and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[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{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{intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + + +\begin{struct}\label{staircase_function} + A staircase function $f$ is a onesorted structure equipped with + \begin{enumerate} + \item $\chain$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$. + \item \label{staircase_domain} $\dom{f}$ is a topological space. + \item \label{staricase_def_chain} $C$ is a chain of subsets. + \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. + \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. + \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{legal_staircase} + $f$ is a legal staircase function iff + $f$ is a staircase function and + for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$. +\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{definition}\label{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 \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. +\end{definition} + +\begin{abbreviation}\label{infinte_sequence} + $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. +\end{abbreviation} + +\begin{definition}\label{infinite_product} + $X$ is the infinite product of $Y$ iff + $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$. +\end{definition} + +\begin{definition}\label{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} + + +% The next thing we need to define is the uniform staircase function. +% This function has it's domain in $X$ and maps to the closed interval $[0,1]$. +% These functions should behave als follows, +% \begin{align} +% &f(A_{0}) = 1 &\text{consant} \\ +% &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.} +% \end{align} + +% We then prove that for any given $r$ we find a repolished chain, +% which contains the $A_{i}$ and this replished chain is also legal. +% +% The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ +% be a staircase function with $n$ many refinemants. +% This limit will be continuous and we would be done. + + +% TODO: Since we want to prove that $f$ is continus, we have to formalize that +% \reals with the usual topology is a topological space. +% ------------------------------------------------------------- + +\begin{theorem}\label{urysohn} + Let $X$ be a urysohn space. + Suppose $A,B \subseteq \closeds{X}$. + Suppose $A \inter B$ is empty. + There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. +\end{theorem} +\begin{proof} + We show that for all $n \in \naturals$ we have + if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ + then there exist $C'$ such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ + and $C'$ is a refinmant of $C$. + \begin{subproof} + Omitted. + \end{subproof} + + + + Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + + We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence + and for all $i \in \indexset[\zeta]$ we have + $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ + and $A \subseteq \index[\zeta](i)$ + and $\index[\zeta](i) \subseteq (X \setminus B)$ + and for all $j \in \indexset[\zeta]$ such that + $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\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{safe} +% Contradiction. +%\end{theorem} -- cgit v1.2.3 From 65e5a741655d8339ad5763e365ea2addd2e96e51 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Fri, 9 Aug 2024 15:15:49 +0200 Subject: put cardinalit to the right place --- library/cardinal.tex | 6 ++++++ library/topology/urysohn.tex | 39 ++++++++++++++++++++++++++++++++------- 2 files changed, 38 insertions(+), 7 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/cardinal.tex b/library/cardinal.tex index d0dec59..8691b30 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -3,6 +3,7 @@ \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,8 @@ \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/topology/urysohn.tex b/library/topology/urysohn.tex index 65457ea..c795db8 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -33,10 +33,6 @@ The first tept will be a formalisation of chain constructions. $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. \end{definition} -\begin{definition}\label{cardinality} - $X$ has cardinality of $n$ iff - $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$. -\end{definition} @@ -134,6 +130,13 @@ The first tept will be a formalisation of chain constructions. for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. \end{definition} +\begin{definition}\label{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 \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. +\end{definition} + \begin{abbreviation}\label{infinte_sequence} $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. \end{abbreviation} @@ -149,6 +152,26 @@ The first tept will be a formalisation of chain constructions. and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$. \end{definition} +\begin{abbreviation}\label{two} + $\two = \suc{1}$. +\end{abbreviation} + +\begin{lemma}\label{two_in_reals} + $\two \in \reals$. +\end{lemma} + +\begin{lemma}\label{two_in_naturals} + $\two \in \naturals$. +\end{lemma} + +\begin{inductive}\label{power_of_two} + Define $\powerOfTwoSet \subseteq \naturals$. + \begin{enumerate} + \item $\two \in \powerOfTwoSet$. + \item If $n \in \powerOfTwoSet$, then $n \rmul \two \in \powerOfTwoSet$. + \end{enumerate} + +\end{inductive} % The next thing we need to define is the uniform staircase function. % This function has it's domain in $X$ and maps to the closed interval $[0,1]$. @@ -186,6 +209,8 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} + There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$. + Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. @@ -269,6 +294,6 @@ The first tept will be a formalisation of chain constructions. %\end{subproof} \end{proof} -%\begin{theorem}\label{safe} -% Contradiction. -%\end{theorem} +\begin{theorem}\label{safe} + Contradiction. +\end{theorem} -- cgit v1.2.3 From d49a4f85a928c4e93c6cbb2ebada5875e12c4b4f Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 10 Aug 2024 01:25:48 +0200 Subject: more ur Date: Sat, 10 Aug 2024 16:02:43 +0200 Subject: more urysohn --- library/topology/urysohn.tex | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index bb28116..3152de7 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -262,12 +262,26 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} +\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{proposition}\label{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{\indexset[U]}$. + For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. %\begin{definition}\label{refinmant} @@ -276,9 +290,7 @@ The first tept will be a formalisation of chain constructions. % 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} -- cgit v1.2.3 From 34aad4be8fb8433f0205517732da0d449d077572 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 10 Aug 2024 19:18:39 +0200 Subject: more more urysohn --- library/cardinal.tex | 2 + library/topology/urysohn.tex | 341 ++++++++++++++++++++++++------------------- 2 files changed, 190 insertions(+), 153 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/cardinal.tex b/library/cardinal.tex index 8691b30..044e5d1 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -18,3 +18,5 @@ $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/topology/urysohn.tex b/library/topology/urysohn.tex index 3152de7..028e10f 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -198,60 +198,82 @@ The first tept will be a formalisation of chain constructions. Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. - Suppose $U = \{A,(X \setminus B)\}$. - Suppose $\indexset[U]= \{\zero, 1\}$. - Suppose $\index[U](\zero) = A$. - Suppose $\index[U](1) = (X \setminus B)$. - Then $U$ is a urysohnchain in $X$. + Then there exist $U$ + such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ + and $\indexset[U]= \{\zero, 1\}$ + and $\index[U](\zero) = A$ + and $\index[U](1) = (\carrier[X] \setminus B)$. + %$U$ is a urysohnchain in $X$. \end{proposition} \begin{proof} - We show that $U$ is a sequence. - \begin{subproof} - Omitted. - \end{subproof} - We show that $A \subseteq (X \setminus B)$. - \begin{subproof} - Omitted. - \end{subproof} + Omitted. - We show that $U$ is a chain of subsets. - \begin{subproof} - For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$. - It suffices to show that for all $n \in \indexset[U]$ we have - for all $m \in \indexset[U]$ such that - $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. - Fix $n \in \indexset[U]$. - Fix $m \in \indexset[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} + % 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 \indexset[U]$ we have $n = \zero \lor n = 1$. + % It suffices to show that for all $n \in \indexset[U]$ we have + % for all $m \in \indexset[U]$ such that + % $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. + % Fix $n \in \indexset[U]$. + % Fix $m \in \indexset[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 \indexset[U]$ such that $n < m$ we have + % $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. + % \begin{subproof} + % Omitted. + % \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} + +\end{proof} - 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 \indexset[U]$ such that $n < m$ we have - $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. - \begin{subproof} - Omitted. - \end{subproof} +\begin{proposition}\label{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 $\indexset[U]= \{\zero, 1\}$ + and $\index[U](\zero) = A$ + and $\index[U](1) = (\carrier[X] \setminus B)$. + Then $U$ is a urysohnchain in $X$. +\end{proposition} +\begin{proof} + Omitted. \end{proof} + \begin{proposition}\label{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}$ @@ -295,134 +317,147 @@ The first tept will be a formalisation of chain constructions. \end{proof} +\begin{proposition}\label{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 \indexset[U]$ we have for all $x \in \index[U](n)$ + we have $f(x) = \rfrac{n}{k}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} +\begin{abbreviation}\label{refinment_abbreviation} + $x \refine y$ iff $x$ is a refinmant of $y$. +\end{abbreviation} - - -% The next thing we need to define is the uniform staircase function. -% This function has it's domain in $X$ and maps to the closed interval $[0,1]$. -% These functions should behave als follows, -% \begin{align} -% &f(A_{0}) = 1 &\text{consant} \\ -% &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.} -% \end{align} - -% We then prove that for any given $r$ we find a repolished chain, -% which contains the $A_{i}$ and this replished chain is also legal. -% -% The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ -% be a staircase function with $n$ many refinemants. -% This limit will be continuous and we would be done. - - -% TODO: Since we want to prove that $f$ is continus, we have to formalize that -% \reals with the usual topology is a topological space. -% ------------------------------------------------------------- - \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. - There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. \end{theorem} \begin{proof} - We show that for all $n \in \naturals$ we have - if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ - then there exist $C'$ such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ - and $C'$ is a refinmant of $C$. - \begin{subproof} - Omitted. - \end{subproof} - - There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$. - - - Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ + and $\indexset[\eta] = \{\zero, 1\}$ + and $\index[\eta](\zero) = A$ + and $\index[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. - We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence - and for all $i \in \indexset[\zeta]$ we have - $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ - and $A \subseteq \index[\zeta](i)$ - and $\index[\zeta](i) \subseteq (X \setminus B)$ - and for all $j \in \indexset[\zeta]$ such that - $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. + We show that there exist $\zeta$ such that $\zeta$ is a sequence + and $\indexset[\zeta] = \naturals$ + and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$ + and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ + and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$. \begin{subproof} - Omitted. - \end{subproof} - - - - - - + %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$. + %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$. + 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)))\}$. - - 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. + % TODO: Proof that \beta is a function which would be used for the indexing. + \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} + %Suppose $\eta$ is a urysohnchain in $X$. + %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ + %and $\indexset[\eta] = \{\zero, 1\}$ + %and $\index[\eta](\zero) = A$ + %and $\index[\eta](1) = (X \setminus B)$. + + + %Then $\eta$ is a urysohnchain in $X$. + + % Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + % + % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence + % and for all $i \in \indexset[\zeta]$ we have + % $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ + % and $A \subseteq \index[\zeta](i)$ + % and $\index[\zeta](i) \subseteq (X \setminus B)$ + % and for all $j \in \indexset[\zeta]$ such that + % $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\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{safe} - Contradiction. -\end{theorem} +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} -- cgit v1.2.3 From e9fa2c5d9539067d9ecce52bbbccacdfd020c563 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sun, 11 Aug 2024 17:10:57 +0200 Subject: more more more urysohn --- library/topology/urysohn.tex | 34 +++++++++++++++++++++++++++------- 1 file changed, 27 insertions(+), 7 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 028e10f..f34f12f 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -5,6 +5,7 @@ \import{function.tex} \import{set.tex} \import{cardinal.tex} +\import{relation.tex} \section{Urysohns Lemma} % In this section we want to proof Urysohns lemma. @@ -188,10 +189,20 @@ The first tept will be a formalisation of chain constructions. \end{lemma} +\begin{axiom}\label{pot1} + $\pot \in \funs{\naturals}{\naturals}$. +\end{axiom} +\begin{axiom}\label{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{pot_as_function} + $\pot(n) = \apply{\pot}{n}$. +\end{abbreviation} \begin{proposition}\label{urysohnchain_induction_begin} @@ -356,15 +367,24 @@ The first tept will be a formalisation of chain constructions. and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$. \begin{subproof} - %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$. - %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$. - 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)))\}$. + %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 $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$. + Omitted. + \end{subproof} - % TODO: Proof that \beta is a function which would be used for the indexing. - + We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. + \begin{subproof} + Trivial. \end{subproof} + -- cgit v1.2.3 From c4894bc4e788fae079b76b824a8d86c167098cc8 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 00:12:07 +0200 Subject: more more way more urysohn --- library/topology/urysohn.tex | 127 ++++++++++++++++++++++++++++++++++++++++--- source/Api.hs | 8 +-- source/CommandLine.hs | 5 +- source/Syntax/Lexicon.hs | 1 + 4 files changed, 127 insertions(+), 14 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index f34f12f..6662706 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -36,7 +36,12 @@ The first tept will be a formalisation of chain constructions. - +%%----------------------- +% Idea: +% A sequence could be define as a family of sets, +% together with the existence of an indexing function. +% +%%----------------------- \begin{struct}\label{sequence} A sequence $X$ is a onesorted structure equipped with \begin{enumerate} @@ -148,8 +153,9 @@ The first tept will be a formalisation of chain constructions. \end{definition} \begin{definition}\label{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$ + $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} @@ -312,9 +318,9 @@ The first tept will be a formalisation of chain constructions. % 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{\indexset[U]}$. - For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ - such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. + % Let $m = \max{\indexset[U]}$. + % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. %\begin{definition}\label{refinmant} @@ -347,6 +353,58 @@ The first tept will be a formalisation of chain constructions. + +\begin{abbreviation}\label{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{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{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{abbreviation}\label{converge} + $s$ converges iff $s$ is a sequence of real numbers + and $\indexset[s]$ is infinite + and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have + there exist $N \in \indexset[s]$ such that + for all $m \in \indexset[s]$ such that $m > N$ + we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$. +\end{abbreviation} + + +\begin{definition}\label{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 \indexset[s]$ such that + for all $m \in \indexset[s]$ such that $m > n$ + we have $\abs{x - \index[s](n)} < \epsilon$. +\end{definition} + +\begin{proposition}\label{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{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -381,12 +439,65 @@ The first tept will be a formalisation of chain constructions. We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. \begin{subproof} - Trivial. + Omitted. \end{subproof} - + For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + %%------------- Maybe use Abstrect.hs line 368 "Local Function". + + We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ + we have $f(x) = \rfrac{n}{\pot(m)}$. + \begin{subproof} + % Fix $m \in \indexset[\zeta]$. + % $\index[\zeta](m)$ is a urysohnchain in $X$. + % + % Follows by \cref{existence_of_staircase_function}. + + Omitted. + \end{subproof} + + + + %The sequenc of the functions + Let $\gamma = \{ + (n,f) \mid + n \in \naturals \mid + + \forall n' \in \indexset[\index[\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 \index[\index[\zeta](n)](n')) + \land (f(x)= \zero) ) + + \lor + + ( (n' > \zero) + \land (x \in \index[\index[\zeta](n)](n')) + \land (x \notin \index[\index[\zeta](n)](n'-1)) + \land (f(x) = \rfrac{n'}{\pot(n)}) ) + + \lor + + ( (x \notin \index[\index[\zeta](n)](n')) + \land (f(x) = 1) ) + + \}$. + + + + %Suppose $\eta$ is a urysohnchain in $X$. %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ diff --git a/source/Api.hs b/source/Api.hs index f597153..3fb0ca2 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -292,10 +292,10 @@ exportMegalodon file = do -- | 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 ("Prover found countermodel: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("Contradictory axioms: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("Out of resources: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("Error at: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +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!" diff --git a/source/CommandLine.hs b/source/CommandLine.hs index 47efe22..711f7f0 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -87,15 +87,16 @@ run = do 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 "Verification successful." + VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" VerificationFailure [] -> error "Empty verification fail" VerificationFailure fails -> do - putStrLn "Following task couldn't be solved by the ATP: " + putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m" traverse_ showFailedTask fails Text.hPutStrLn stderr "Don't give up!" diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index de6d966..4fe8730 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -112,6 +112,7 @@ prefixOps = , ([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")) -- cgit v1.2.3 From a79924e85260c911045f43bac3f051a8be6e5334 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 00:52:54 +0200 Subject: Completed the structure of the proof of Urysohn. Now every single step has to be proven. --- library/topology/urysohn.tex | 44 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 40 insertions(+), 4 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 6662706..0c4052d 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -410,7 +410,7 @@ The first tept will be a formalisation of chain constructions. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + and $f(A) = 0$ and $f(B)= 1$ and $f$ is continuous. \end{theorem} \begin{proof} @@ -442,8 +442,10 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} - For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. - + We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + \begin{subproof} + Omitted. + \end{subproof} %%------------- Maybe use Abstrect.hs line 368 "Local Function". @@ -495,9 +497,43 @@ The first tept will be a formalisation of chain constructions. \}$. + Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. + + + We show that there exist $F$ such that + $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and + for all $x \in \carrier[X]$ we have + there exist $k \in \intervalclosed{\zero}{1}$ + such that $F(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{(k - \apply{\gamma(N')}{x})} \leq \epsilon$. + \begin{subproof} + Omitted. + \end{subproof} + - + We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F(A) = 0$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F(B) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F$ is continuous. + \begin{subproof} + Omitted. + \end{subproof} %Suppose $\eta$ is a urysohnchain in $X$. %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ -- cgit v1.2.3 From 85920f166c95904550134a1d4e84d5430c05d009 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 11:43:26 +0200 Subject: way more urysohn --- library/topology/urysohn.tex | 116 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 102 insertions(+), 14 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 0c4052d..d8b1e14 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -402,18 +402,32 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} +\begin{definition}\label{limit_sequence} + $x$ is the limit sequence of $f$ iff + $x$ is a sequence and $\indexset[x] = \dom{f}$ and + for all $n \in \indexset[x]$ we have + $\index[x](n) = f(n)$. +\end{definition} +\begin{definition}\label{realsminus} + $\realsminus = \{r \in \reals \mid r < \zero\}$. +\end{definition} + +\begin{abbreviation}\label{realsplus} + $\realsplus = \reals \setminus \realsminus$. +\end{abbreviation} \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(A) = 0$ and $f(B)= 1$ and $f$ is continuous. + 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 $\indexset[\eta] = \{\zero, 1\}$ and $\index[\eta](\zero) = A$ @@ -498,29 +512,103 @@ The first tept will be a formalisation of chain constructions. \}$. Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. - + %We show that there exist $\kappa$ such that $\kappa$ is the limit sequence of $\gamma$. + %\begin{subproof} + % Omitted. + %\end{subproof} - We show that there exist $F$ such that - $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and - for all $x \in \carrier[X]$ we have - there exist $k \in \intervalclosed{\zero}{1}$ - such that $F(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{(k - \apply{\gamma(N')}{x})} \leq \epsilon$. + %Let $\gamma(n)(x) = \apply{\gamma(n)}{x}$ for $x\in \carrier[X]$ + + 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 there exist $g$ such 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$ and $g(x)= k$. + \begin{subproof} + + %Let $G(x) = \{k \in \carrier[X] \mid \forall \epsilon \in \realsplus. \exists N \in \naturals. \forall N' \in \naturals. (N' > N) \land (\abs{\apply{\gamma(n)}{x} - k} < \epsilon)\}$ for $x \in \carrier[X]$. +% + %We show that for all $x \in \carrier[X]$ we have $G(x)$ has cardinality $1$. + %\begin{subproof} + % Omitted. + %\end{subproof} +% + %Let $H(x) = \unions{G(x)}$ for $x \in \carrier[X]$. + %For all $x \in \carrier[X]$ we have $\{H(x)\} = G(x)$. + + 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} + Omitted. + \end{subproof} + + + \end{subproof} + + + %Let $S(x) = \{(n,x) \mid n \in naturals \mid x = (\gamma(n))(x)\}$. + + %Let $S(x) + + %We show that there exist $F$ such that + %for all $x \in \carrier[X]$ we have $F(x)$ is + + + %We show that there exist $F$ such that + %$F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and + %for all $x \in \carrier[X]$ we have + %there exist $k \in \intervalclosed{\zero}{1}$ + %such that $F(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{(k - \apply{\gamma(N')}{x})} \leq \epsilon$. + %\begin{subproof} + % Omitted. + %\end{subproof} + + We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. - \begin{subproof} + \begin{subproof} Omitted. + + %It suffices to show that $\dom{F} = \carrier[X]$ and + %$F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $F$ is right-unique. + % + %We show that $F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$. + %\begin{subproof} + % It suffices to show that $F \in \pow{\carrier[X] \times \intervalclosed{\zero}{1}}$. + % It suffices to show that for all $w \in F$ we have $w \in (\carrier[X] \times \intervalclosed{\zero}{1})$. +% + % Fix $w \in F$. +% + % %Take $x$ such that there exist $k \in \intervalclosed{\zero}{1}$ such that $w = (x,k)$. +% +% + %\end{subproof} + % +% +% + %Trivial. \end{subproof} - We show that $F(A) = 0$. + We show that $F(A) = \zero$. \begin{subproof} Omitted. \end{subproof} -- cgit v1.2.3 From b51f61e6be5be4729e61ede79fb0bd3cb26f57a6 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 14:41:32 +0200 Subject: way way more urysohn --- library/topology/urysohn.tex | 82 +++++++++++++++++++++++--------------------- source/CommandLine.hs | 3 ++ 2 files changed, 45 insertions(+), 40 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index d8b1e14..414043f 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -526,6 +526,11 @@ The first tept will be a formalisation of chain constructions. 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} + Omitted. + \end{subproof} + We show that there exist $g$ such that @@ -535,18 +540,7 @@ The first tept will be a formalisation of chain constructions. 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$ and $g(x)= k$. - \begin{subproof} - - %Let $G(x) = \{k \in \carrier[X] \mid \forall \epsilon \in \realsplus. \exists N \in \naturals. \forall N' \in \naturals. (N' > N) \land (\abs{\apply{\gamma(n)}{x} - k} < \epsilon)\}$ for $x \in \carrier[X]$. -% - %We show that for all $x \in \carrier[X]$ we have $G(x)$ has cardinality $1$. - %\begin{subproof} - % Omitted. - %\end{subproof} -% - %Let $H(x) = \unions{G(x)}$ for $x \in \carrier[X]$. - %For all $x \in \carrier[X]$ we have $\{H(x)\} = G(x)$. - + \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 @@ -554,10 +548,9 @@ The first tept will be a formalisation of chain constructions. for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$. \begin{subproof} - Omitted. + Fix $x \in \carrier[X]$. + 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} - - \end{subproof} @@ -581,44 +574,53 @@ The first tept will be a formalisation of chain constructions. %\begin{subproof} % Omitted. %\end{subproof} + + Let $G(x) = g(x)$ for $x \in \carrier[X]$. + We have $\dom{G} = \carrier[X]$. - - We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. - \begin{subproof} + %For all $x \in \carrier[X]$ for all $n \in \naturals$ we have $g(x) \leq \apply{\gamma(n)}{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$ and $g(x)= k$. + + + + \end{subproof} + + We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. + \begin{subproof} Omitted. - - %It suffices to show that $\dom{F} = \carrier[X]$ and - %$F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $F$ is right-unique. - % - %We show that $F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$. - %\begin{subproof} - % It suffices to show that $F \in \pow{\carrier[X] \times \intervalclosed{\zero}{1}}$. - % It suffices to show that for all $w \in F$ we have $w \in (\carrier[X] \times \intervalclosed{\zero}{1})$. -% - % Fix $w \in F$. -% - % %Take $x$ such that there exist $k \in \intervalclosed{\zero}{1}$ such that $w = (x,k)$. -% -% - %\end{subproof} - % -% -% - %Trivial. \end{subproof} - We show that $F(A) = \zero$. + + 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}$ . + \end{subproof} + + We show that $G(A) = \zero$. \begin{subproof} Omitted. \end{subproof} - We show that $F(B) = 1$. + We show that $G(B) = 1$. \begin{subproof} Omitted. \end{subproof} - We show that $F$ is continuous. + We show that $G$ is continuous. \begin{subproof} Omitted. \end{subproof} diff --git a/source/CommandLine.hs b/source/CommandLine.hs index 711f7f0..b8c170e 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -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 -- cgit v1.2.3 From 8a19eec1e581efa473af0173ba79b553e4191ffa Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 15:55:17 +0200 Subject: way way way more urysohn --- library/topology/urysohn.tex | 58 +++++++++++++++++--------------------------- 1 file changed, 22 insertions(+), 36 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 414043f..3be3c30 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -461,8 +461,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} - %%------------- Maybe use Abstrect.hs line 368 "Local Function". - + We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ we have $f(x) = \rfrac{n}{\pot(m)}$. @@ -513,13 +512,7 @@ The first tept will be a formalisation of chain constructions. Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. - %We show that there exist $\kappa$ such that $\kappa$ is the limit sequence of $\gamma$. - %\begin{subproof} - % Omitted. - %\end{subproof} - - %Let $\gamma(n)(x) = \apply{\gamma(n)}{x}$ for $x\in \carrier[X]$ - + We show that for all $n \in \naturals$ we have $\gamma(n)$ is a function from $\carrier[X]$ to $\reals$. \begin{subproof} @@ -552,49 +545,42 @@ The first tept will be a formalisation of chain constructions. 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} \end{subproof} - - - %Let $S(x) = \{(n,x) \mid n \in naturals \mid x = (\gamma(n))(x)\}$. - - %Let $S(x) - - %We show that there exist $F$ such that - %for all $x \in \carrier[X]$ we have $F(x)$ is - - - %We show that there exist $F$ such that - %$F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and - %for all $x \in \carrier[X]$ we have - %there exist $k \in \intervalclosed{\zero}{1}$ - %such that $F(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{(k - \apply{\gamma(N')}{x})} \leq \epsilon$. - %\begin{subproof} - % Omitted. - %\end{subproof} Let $G(x) = g(x)$ for $x \in \carrier[X]$. We have $\dom{G} = \carrier[X]$. - %For all $x \in \carrier[X]$ for all $n \in \naturals$ we have $g(x) \leq \apply{\gamma(n)}{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$ and $g(x)= k$. - + 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$. + $g(x)= k$. + + 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}. \end{subproof} We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. \begin{subproof} - Omitted. + 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} = 0$. + + + \caseOf{$x \notin A$.} + \begin{byCase} + \caseOf{$x \in B$.} + OFor all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. + + \caseOf{$x \notin B$.} + Omitted. + \end{byCase} + \end{byCase} \end{subproof} -- cgit v1.2.3 From 41357a4c0ad22b1ea0094ea52c832d117ec3fec4 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:30:47 +0200 Subject: way way way way more urysohn --- library/topology/urysohn.tex | 51 +++++++++++++++++++++++++++++++++++++++----- 1 file changed, 46 insertions(+), 5 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 3be3c30..c94dbd4 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -98,6 +98,10 @@ The first tept will be a formalisation of chain constructions. $\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{struct}\label{staircase_function} A staircase function $f$ is a onesorted structure equipped with @@ -333,6 +337,34 @@ The first tept will be a formalisation of chain constructions. \end{proof} +\begin{lemma}\label{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{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{frection3} + Suppose $a,b \in \reals$. + Suppose $\zero < a < 1$. + Suppose $\zero < b < 1$. + % Here take exist n such that n/2^n is between a and b + T +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + \begin{proposition}\label{existence_of_staircase_function} Let $X$ be a urysohn space. @@ -489,8 +521,9 @@ The first tept will be a formalisation of chain constructions. % (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 + % 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 \index[\index[\zeta](n)](n')) @@ -556,7 +589,15 @@ The first tept will be a formalisation of chain constructions. 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$. - $g(x)= k$. + + 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$. + %Assume $\epsilon > \zero$. + %Take $N' \in \naturals$ such that $\epsilon > \rfrac{1}{\pot(N')}$. + \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}. @@ -569,13 +610,13 @@ The first tept will be a formalisation of chain constructions. Then $x \in \carrier[X]$. \begin{byCase} \caseOf{$x \in A$.} - For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 0$. + For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$. \caseOf{$x \notin A$.} \begin{byCase} \caseOf{$x \in B$.} - OFor all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. + For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. \caseOf{$x \notin B$.} Omitted. -- cgit v1.2.3 From ee24a73a01608125e6648f7b66d9c679e955009d Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 13 Aug 2024 23:51:57 +0200 Subject: less urysohn --- library/relation.tex | 1 + library/topology/urysohn.tex | 182 +++++++++++++++++++++++++++++++------------ 2 files changed, 133 insertions(+), 50 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/relation.tex b/library/relation.tex index 4c4065f..d63e747 100644 --- a/library/relation.tex +++ b/library/relation.tex @@ -633,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/topology/urysohn.tex b/library/topology/urysohn.tex index c94dbd4..ba9780a 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -1,11 +1,17 @@ \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} % In this section we want to proof Urysohns lemma. @@ -337,33 +343,8 @@ The first tept will be a formalisation of chain constructions. \end{proof} -\begin{lemma}\label{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{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{frection3} - Suppose $a,b \in \reals$. - Suppose $\zero < a < 1$. - Suppose $\zero < b < 1$. - % Here take exist n such that n/2^n is between a and b - T -\end{lemma} -\begin{proof} - Omitted. -\end{proof} \begin{proposition}\label{existence_of_staircase_function} @@ -449,6 +430,86 @@ The first tept will be a formalisation of chain constructions. $\realsplus = \reals \setminus \realsminus$. \end{abbreviation} +\begin{proposition}\label{intervalclosed_subseteq_reals} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $\intervalclosed{a}{b} \subseteq \reals$. +\end{proposition} + + + +\begin{lemma}\label{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{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{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{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{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{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{epsilonball} + $\epsBall{a}{\epsilon} = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$. +\end{abbreviation} + +\begin{proposition}\label{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} + + + +% Note this could maybe reslove some issues!!!! +\begin{definition}\label{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{theorem}\label{urysohn} Let $X$ be a urysohn space. @@ -483,6 +544,8 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} + For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$. + We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. \begin{subproof} Omitted. @@ -493,6 +556,11 @@ The first tept will be a formalisation of chain constructions. 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 \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ @@ -545,37 +613,56 @@ The first tept will be a formalisation of chain constructions. 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$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. + + 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 \index[\index[\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]$. + \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 - 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$ and $g(x)= k$. + + 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$. + 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]$. - 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}. + + + + % 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} \end{subproof} @@ -588,20 +675,15 @@ The first tept will be a formalisation of chain constructions. 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$. + 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$. + 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$. - %Assume $\epsilon > \zero$. - %Take $N' \in \naturals$ such that $\epsilon > \rfrac{1}{\pot(N')}$. - \end{subproof} - - - + + \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}. - \end{subproof} We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. -- cgit v1.2.3 From 5a7450eedc020867ee52ae9f1ecb6def7aa998bb Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Wed, 14 Aug 2024 10:50:26 +0200 Subject: The added proposition and definition should have resloved some proofing complications, but they can prove flase together with lemmas about ordinal, the exat lemma are in urysohn.tex at line 522. --- library/topology/urysohn.tex | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index ba9780a..c3c72f0 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -503,11 +503,24 @@ The first tept will be a formalisation of chain constructions. -% Note this could maybe reslove some issues!!!! + \begin{definition}\label{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{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 + @@ -544,7 +557,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} - For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$. + %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$. We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. \begin{subproof} @@ -824,6 +837,6 @@ The first tept will be a formalisation of chain constructions. % \end{subproof} \end{proof} -%\begin{theorem}\label{safe} -% Contradiction. -%\end{theorem} +\begin{theorem}\label{safe} + Contradiction. +\end{theorem} -- cgit v1.2.3 From 29027c9d2cdbdfe59e48b5aa28eb2d32d1a4c1f7 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 24 Aug 2024 11:43:29 +0200 Subject: naproch sty extension --- latex/naproche.sty | 10 ++++++++ latex/stdlib.tex | 2 ++ library/topology/urysohn.tex | 33 ++++++++++++++----------- library/topology/urysohn2.tex | 56 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 87 insertions(+), 14 deletions(-) create mode 100644 library/topology/urysohn2.tex (limited to 'library/topology/urysohn.tex') diff --git a/latex/naproche.sty b/latex/naproche.sty index 7ef2359..5ca673d 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -100,6 +100,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}{<} @@ -133,6 +134,14 @@ \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{\indexset}[2]{#1} + \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol @@ -166,6 +175,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..2faa267 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -46,4 +46,6 @@ \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} \input{../library/numbers.tex} + \input{../library/topology/urysohn.tex} + \input{../library/wunschzettel.tex} \end{document} diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index c3c72f0..b8a5fa5 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -504,26 +504,31 @@ The first tept will be a formalisation of chain constructions. -\begin{definition}\label{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{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} +%\begin{definition}\label{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{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{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex new file mode 100644 index 0000000..8e5261e --- /dev/null +++ b/library/topology/urysohn2.tex @@ -0,0 +1,56 @@ +\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} + + + +\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{definition}\label{intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + + + + +\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(A) = \zero$ and $f(B)= 1$ and $f$ is continuous. +\end{theorem} +\begin{proof} + + + + + + Contradiction. + +\end{proof} + +\begin{theorem}\label{safe} + Contradiction. +\end{theorem} -- cgit v1.2.3 From 565db8eb643673f15c44bd8a8ac30debc9b388fd Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Thu, 29 Aug 2024 15:22:11 +0200 Subject: working commit --- library/topology/urysohn.tex | 43 +++++++++++++++++++++++++++++++------------ library/topology/urysohn2.tex | 30 ++++++++++++++++++++++-------- 2 files changed, 53 insertions(+), 20 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index b8a5fa5..79d65dc 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -100,6 +100,14 @@ The first tept will be a formalisation of chain constructions. \subsection{staircase function} +\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} @@ -122,6 +130,9 @@ The first tept will be a formalisation of chain constructions. \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. + \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$. + \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ + such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. \end{enumerate} \end{struct} @@ -311,13 +322,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\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{proposition}\label{urysohnchain_induction_step_existence} Let $X$ be a urysohn space. @@ -562,6 +567,16 @@ The first tept will be a formalisation of chain constructions. 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 $\index[\zeta](n)$ is a urysohnchain in $X$. We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. @@ -581,15 +596,19 @@ The first tept will be a formalisation of chain constructions. We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ + and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ we have $f(x) = \rfrac{n}{\pot(m)}$. \begin{subproof} - % Fix $m \in \indexset[\zeta]$. - % $\index[\zeta](m)$ is a urysohnchain in $X$. - % - % Follows by \cref{existence_of_staircase_function}. + Fix $m \in \indexset[\zeta]$. + $\index[\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 \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1) + \end{cases} - Omitted. + \end{subproof} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 40a3615..71de210 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -68,18 +68,32 @@ Let $H = \carrier[X] \setminus B$. Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$. + Let $\eta = \carrier[X]$. - - - Define $f : X \to \reals$ such that $f(x) = $ + + % Provable + % vvv + Define $F : \eta \to \reals$ such that $F(x) =$ \begin{cases} - &(x + k) &\text{if} x \in X \land k \in \naturals - & x &\text{if} x \neq \zero - & \zero & \text{if} x = \zero - % & x ,x \in X <- will result in technicly ambigus parse + & \zero &\text{if} x \in A\\ + & \rfrac{1}{1+1} &\text{if} x \in (\carrier[X] \setminus (A \union B))\\ + & 1 &\text{if} x \in B \end{cases} - + %Define $f : \naturals \to \pow{P}$ such that $f(x)=$ + %\begin{cases} + % & \emptyset & \text{if} x = \zero \\ + % & \{A, H\} & \text{if} x = 1 \\ + % & G & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \} + %\end{cases} + + Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$. + Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff + $q = \zero \land S = A$ or $q = 1 \land S = H$ or + for all $q_1, q_2, S_1, S_2$ + such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ + we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ + and $q \mathrel{R} S$. Trivial. -- cgit v1.2.3 From 8155ba18260743b1e45507e6fb8d4f80c22c425e Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Fri, 30 Aug 2024 19:25:00 +0200 Subject: working commit --- library/topology/urysohn.tex | 151 +++++++++++++++++++++++++++++-------------- 1 file changed, 101 insertions(+), 50 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 79d65dc..e1fa924 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -231,6 +231,51 @@ The first tept will be a formalisation of chain constructions. $\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{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{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{urysohnchain_induction_begin} Let $X$ be a urysohn space. @@ -600,15 +645,16 @@ The first tept will be a formalisation of chain constructions. we have $f(x) = \rfrac{n}{\pot(m)}$. \begin{subproof} Fix $m \in \indexset[\zeta]$. - $\index[\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 \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1) - \end{cases} - - + %$\index[\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 \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1) + %\end{cases} +% + Omitted. \end{subproof} @@ -677,6 +723,7 @@ The first tept will be a formalisation of chain constructions. \begin{subproof} Fix $n \in \naturals$. Fix $x \in \carrier[X]$. + Omitted. \end{subproof} @@ -696,11 +743,12 @@ The first tept will be a formalisation of chain constructions. \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} @@ -709,51 +757,54 @@ The first tept will be a formalisation of chain constructions. 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}. + %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} + %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}$ . + %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$. @@ -860,7 +911,7 @@ The first tept will be a formalisation of chain constructions. % Omitted. % \end{subproof} \end{proof} - -\begin{theorem}\label{safe} - Contradiction. -\end{theorem} +% +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} -- cgit v1.2.3 From 26cf156763f71aaa9f638408ba4bffb85b886ab0 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 31 Aug 2024 18:02:42 +0200 Subject: working commit --- library/algebra/group.tex | 10 +++ library/topology/urysohn.tex | 6 ++ library/topology/urysohn2.tex | 157 +++++++++++++++++++++++++++++++++++------- 3 files changed, 148 insertions(+), 25 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/algebra/group.tex b/library/algebra/group.tex index a79bd2f..7de1051 100644 --- a/library/algebra/group.tex +++ b/library/algebra/group.tex @@ -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/topology/urysohn.tex b/library/topology/urysohn.tex index e1fa924..17e2911 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -61,6 +61,11 @@ The first tept will be a formalisation of chain constructions. \end{enumerate} \end{struct} +% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen + + + + \begin{definition}\label{cahin_of_subsets} $C$ is a chain of subsets iff $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. @@ -237,6 +242,7 @@ The first tept will be a formalisation of chain constructions. for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$. \end{axiom} + \begin{lemma}\label{urysohn_set_in_between} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 71de210..e963951 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -15,23 +15,35 @@ \section{Urysohns Lemma} +\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{one_to_n_set} $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. \end{definition} -\begin{struct}\label{sequence} - A sequence $X$ is a onesorted structure equipped with - \begin{enumerate} - \item $\index$ - \item $\indexset$ - \end{enumerate} - such that - \begin{enumerate} - \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. - \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. - \end{enumerate} -\end{struct} + +\begin{definition}\label{sequence} + $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$. +\end{definition} + \begin{abbreviation}\label{urysohnspace} $X$ is a urysohn space iff @@ -42,10 +54,66 @@ \end{abbreviation} -\begin{definition}\label{intervalclosed} - $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\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]$. +\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{finer} %<-- verfeinerung + $X$ is finer then $Y$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $ \closure{\at{X}{n}}{U} \subseteq \interior{\at{Y}{k}}{U} \subseteq \closure{\at{Y}{k}}{U} \subseteq \interior{\at{X}{m}}{U}$. +\end{definition} + + +\begin{definition}\label{sequence_of_reals} + $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$. +\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 = \reals \setminus \realsminus$. +\end{definition} + +\begin{definition}\label{epsilon_ball} + $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$. +\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{theorem}\label{urysohnsetinbeetween} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -55,7 +123,6 @@ \end{theorem} - \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -76,8 +143,8 @@ Define $F : \eta \to \reals$ such that $F(x) =$ \begin{cases} & \zero &\text{if} x \in A\\ - & \rfrac{1}{1+1} &\text{if} x \in (\carrier[X] \setminus (A \union B))\\ - & 1 &\text{if} x \in B + & \rfrac{1}{1+1} &\text{if} x \in (\carrier[X] \setminus (A \union B))\\ + & 1 &\text{if} x \in B \end{cases} %Define $f : \naturals \to \pow{P}$ such that $f(x)=$ @@ -87,19 +154,59 @@ % & G & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \} %\end{cases} - Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$. - Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff - $q = \zero \land S = A$ or $q = 1 \land S = H$ or - for all $q_1, q_2, S_1, S_2$ - such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ - we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ - and $q \mathrel{R} S$. + %Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$. + %Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff + % $q = \zero \land S = A$ or $q = 1 \land S = H$ or + % for all $q_1, q_2, S_1, S_2$ + % such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ + % we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ + % and $q \mathrel{R} S$. - Trivial. + %Let $J = \{(n,f) \mid n denots the cardinality of a urysohn chain on which f is a staircase function\}$. +% + %Let $N = \naturals$. + %Define $j : N \to \funs{\carrier[X]}{\eals}$ such that $j(n) =$ + %\begin{cases} + % & f &\text{if} n \in N \land \exist w \in J. J=(n,f) + %\end{cases} + + + + + + + + + \end{proof} \begin{theorem}\label{safe} Contradiction. \end{theorem} + + + + +% +%Ideen: +%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat +% +%zulässig und verfeinerung von ketten als predicat definieren. +% +%limits und punkt konvergenz als prädikat. +% +% +%Vor dem Beweis vor dem eigentlichen Beweis. +%die abgeleiteten Funktionen +% +%\derivedstiarcasefunction on A +% +%abbreviation: \at{f}{n} = f_{n} +% +% +%TODO: +%Reals ist ein topologischer Raum +% + -- cgit v1.2.3 From 588c6ab14184cab4bb7df89def641acaafe3b7eb Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 16 Sep 2024 11:34:01 +0200 Subject: working commit --- latex/naproche.sty | 20 +- latex/stdlib.tex | 4 +- library/topology/real-topological-space.tex | 121 ++++++- library/topology/urysohn.tex | 515 ++++++++++++++-------------- library/topology/urysohn2.tex | 14 +- 5 files changed, 387 insertions(+), 287 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/latex/naproche.sty b/latex/naproche.sty index 5ca673d..1a8afb6 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} @@ -139,9 +140,22 @@ \newcommand{\rationals}{\mathcal{Q}} \newcommand{\rminus}{-_{\mathcal{R}}} \newcommand{\seq}[2]{\{#1, ... ,#2\}} -\newcommand{\indexx}[2]{index_{#1}(#2)} -\newcommand{\indexset}[2]{#1} - +\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\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/latex/stdlib.tex b/latex/stdlib.tex index 2faa267..9879708 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -47,5 +47,7 @@ \input{../library/topology/disconnection.tex} \input{../library/numbers.tex} \input{../library/topology/urysohn.tex} - \input{../library/wunschzettel.tex} + \input{../library/topology/urysohn2.tex} + \input{../library/topology/real-topological-space.tex} + %\input{../library/wunschzettel.tex} \end{document} diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index 1c5e4cb..ffdf46e 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -11,7 +11,7 @@ \import{function.tex} -\section{The canonical topology on $\mathbbR$} +\section{The canonical topology on $\mathbb{R}$} \begin{definition}\label{topological_basis_reals_eps_ball} $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. @@ -101,12 +101,15 @@ 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} - %Fix $x,y \in \reals$. + Omitted. \end{proof} \begin{lemma}\label{reals_order_is_transitive} For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{reals_order_plus_minus} Suppose $a,b \in \reals$. @@ -134,16 +137,9 @@ $x + \epsilon \in \reals$. - %It suffices to show that for all $c$ such that $c \rless x$ we have $c \in \epsBall{x}{\epsilon}$. - %Fix $c$ such that $c \rless x$. -% - %It suffices to show that for all $c$ such that $c < x$ we have $c \in \epsBall{x}{\epsilon}$. - %Fix $c$ such that $c < x$. - - 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)$. - %Suppose $(x - \epsilon) < c < (x + \epsilon)$. + $(x - \epsilon) < c < (x + \epsilon)$. \end{proof} \begin{theorem}\label{topological_basis_reals_is_prebasis} @@ -158,9 +154,9 @@ \caseOf{$x = \emptyset$.} Trivial. \caseOf{$x \neq \emptyset$.} - There exists $U \in \topoBasisReals$ such that $x \in \topoBasisReals$. - Take $U \in \topoBasisReals$ such that $x \in \topoBasisReals$. - + %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}$. @@ -168,10 +164,63 @@ 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}$. + 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{realspuls_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{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_}. + There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. + +\end{proof} + + + \begin{theorem}\label{topological_basis_reals_is_basis} $\topoBasisReals$ is a topological basis for $\reals$. \end{theorem} @@ -188,7 +237,45 @@ Trivial. \caseOf{$U \inter V \neq \emptyset$.} Then $U \inter V$ is inhabited. - %It suffices to show that + $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)$. + 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} @@ -230,7 +317,3 @@ Suppose $a,b \in \reals$. Then $\intervalopen{a}{b} \in \opens[\reals]$. \end{proposition} - -\begin{lemma}\label{safetwo} - Contradiction. -\end{lemma} \ No newline at end of file diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 17e2911..ff6a231 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -51,13 +51,14 @@ The first tept will be a formalisation of chain constructions. \begin{struct}\label{sequence} A sequence $X$ is a onesorted structure equipped with \begin{enumerate} - \item $\index$ - \item $\indexset$ + \item $\indexx$ + \item $\indexxset$ + \end{enumerate} such that \begin{enumerate} - \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. - \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$. \end{enumerate} \end{struct} @@ -68,13 +69,13 @@ The first tept will be a formalisation of chain constructions. \begin{definition}\label{cahin_of_subsets} $C$ is a chain of subsets iff - $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. + $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{chain_of_n_subsets} $C$ is a chain of $n$ subsets iff - $C$ is a chain of subsets and $n \in \indexset[C]$ - and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$. + $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} @@ -133,18 +134,18 @@ The first tept will be a formalisation of chain constructions. \item \label{staircase_domain} $\dom{f}$ is a topological space. \item \label{staricase_def_chain} $C$ is a chain of subsets. \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. - \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. + \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. - \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$. - \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ - such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. + \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$. + \item \label{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{legal_staircase} $f$ is a legal staircase function iff $f$ is a staircase function and - for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$. + 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{urysohnspace} @@ -159,23 +160,23 @@ The first tept will be a formalisation of chain constructions. $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 \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. + 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{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 \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. + 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{infinte_sequence} - $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. + $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite. \end{abbreviation} \begin{definition}\label{infinite_product} $X$ is the infinite product of $Y$ iff - $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$. + $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$. \end{definition} \begin{definition}\label{refinmant} @@ -289,9 +290,9 @@ The first tept will be a formalisation of chain constructions. Suppose $A \inter B$ is empty. Then there exist $U$ such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ - and $\indexset[U]= \{\zero, 1\}$ - and $\index[U](\zero) = A$ - and $\index[U](1) = (\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} @@ -310,12 +311,12 @@ The first tept will be a formalisation of chain constructions. % % We show that $U$ is a chain of subsets. % \begin{subproof} - % For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$. - % It suffices to show that for all $n \in \indexset[U]$ we have - % for all $m \in \indexset[U]$ such that - % $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. - % Fix $n \in \indexset[U]$. - % Fix $m \in \indexset[U]$. + % 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$.} @@ -337,8 +338,8 @@ The first tept will be a formalisation of chain constructions. % \begin{subproof} % Omitted. % \end{subproof} - % We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have - % $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. + % 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} @@ -352,9 +353,9 @@ The first tept will be a formalisation of chain constructions. Suppose $A \inter B$ is empty. Suppose there exist $U$ such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ - and $\indexset[U]= \{\zero, 1\}$ - and $\index[U](\zero) = A$ - and $\index[U](1) = (\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} @@ -384,9 +385,9 @@ The first tept will be a formalisation of chain constructions. % 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{\indexset[U]}$. - % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ - % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. + % 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{refinmant} @@ -408,7 +409,7 @@ The first tept will be a formalisation of chain constructions. 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 \indexset[U]$ we have for all $x \in \index[U](n)$ + 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} @@ -445,11 +446,11 @@ The first tept will be a formalisation of chain constructions. \begin{abbreviation}\label{converge} $s$ converges iff $s$ is a sequence of real numbers - and $\indexset[s]$ is infinite + and $\indexxset[s]$ is infinite and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have - there exist $N \in \indexset[s]$ such that - for all $m \in \indexset[s]$ such that $m > N$ - we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$. + 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} @@ -457,9 +458,9 @@ The first tept will be a formalisation of chain constructions. $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 \indexset[s]$ such that - for all $m \in \indexset[s]$ such that $m > n$ - we have $\abs{x - \index[s](n)} < \epsilon$. + 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{existence_of_limit} @@ -473,9 +474,9 @@ The first tept will be a formalisation of chain constructions. \begin{definition}\label{limit_sequence} $x$ is the limit sequence of $f$ iff - $x$ is a sequence and $\indexset[x] = \dom{f}$ and - for all $n \in \indexset[x]$ we have - $\index[x](n) = f(n)$. + $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{realsminus} @@ -596,15 +597,15 @@ The first tept will be a formalisation of chain constructions. \begin{proof} There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ - and $\indexset[\eta] = \{\zero, 1\}$ - and $\index[\eta](\zero) = A$ - and $\index[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. + and $\indexxset[\eta] = \{\zero, 1\}$ + and $\indexx[\eta](\zero) = A$ + and $\indexx[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. We show that there exist $\zeta$ such that $\zeta$ is a sequence - and $\indexset[\zeta] = \naturals$ - and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$ - and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ - and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$. + 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)))\}$. @@ -614,7 +615,7 @@ The first tept will be a formalisation of chain constructions. %$\dom{\beta} = \naturals$. %$\ran{\beta} = \alpha$. %$\beta \in \funs{\naturals}{\alpha}$. - %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$. + %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$. Omitted. \end{subproof} @@ -628,14 +629,14 @@ The first tept will be a formalisation of chain constructions. %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that %$k(x)$ - %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$. + %For all $n \in \naturals$ we have $\indexx[\zeta](n)$ is a urysohnchain in $X$. - We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. + 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 \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$. \begin{subproof} Omitted. \end{subproof} @@ -646,212 +647,212 @@ The first tept will be a formalisation of chain constructions. \end{subproof} - We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ - we have $f(x) = \rfrac{n}{\pot(m)}$. - \begin{subproof} - Fix $m \in \indexset[\zeta]$. - %$\index[\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 \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1) - %\end{cases} +% 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$. % - Omitted. - \end{subproof} - - - - %The sequenc of the functions - Let $\gamma = \{ - (n,f) \mid - n \in \naturals \mid - - \forall n' \in \indexset[\index[\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 \index[\index[\zeta](n)](n')) - \land (f(x)= \zero) ) - - \lor - - ( (n' > \zero) - \land (x \in \index[\index[\zeta](n)](n')) - \land (x \notin \index[\index[\zeta](n)](n'-1)) - \land (f(x) = \rfrac{n'}{\pot(n)}) ) - - \lor - - ( (x \notin \index[\index[\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 \index[\index[\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$. +% %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} % - %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$. - % +% %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]. +% % - %\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 $\indexset[\eta] = \{\zero, 1\}$ - %and $\index[\eta](\zero) = A$ - %and $\index[\eta](1) = (X \setminus B)$. - - - %Then $\eta$ is a urysohnchain in $X$. - - % Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. - % - % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence - % and for all $i \in \indexset[\zeta]$ we have - % $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ - % and $A \subseteq \index[\zeta](i)$ - % and $\index[\zeta](i) \subseteq (X \setminus B)$ - % and for all $j \in \indexset[\zeta]$ such that - % $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. - % \begin{subproof} - % Omitted. - % \end{subproof} - % - % - % +% 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} +% % +% % +% % % % % diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 838b121..83e3aa4 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -367,10 +367,10 @@ \end{subproof} Let $N = \seq{\zero}{k}$. Let $M = \pow{X}$. - Define $V : N \to M$ such that $V(n)=$ + Define $V : N \to M$ such that $V(n)= \begin{cases} - &\at{U}{F(n)} & \text{if} n \in N - \end{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} @@ -445,11 +445,11 @@ $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) =$ + 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} + 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}. -- cgit v1.2.3 From 29f32e2031eafa087323d79d812a1b38ac78f977 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 23 Sep 2024 01:20:05 +0200 Subject: working commit --- library/nat.tex | 22 +-- library/topology/real-topological-space.tex | 2 +- library/topology/urysohn.tex | 140 +++++++-------- library/topology/urysohn2.tex | 254 +++++++++++++++++++++------- 4 files changed, 278 insertions(+), 140 deletions(-) (limited to 'library/topology/urysohn.tex') 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/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index b2e5ea9..c76fd46 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -11,7 +11,7 @@ \import{function.tex} -\section{The canonical topology on $\mathbb{R}$} +\section{Topology Reals} \begin{definition}\label{topological_basis_reals_eps_ball} $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index ff6a231..ae03273 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -36,7 +36,7 @@ The first tept will be a formalisation of chain constructions. % $\overline{A_{i-1}} \subset \interior{A_{i}}$. % In this case we call the chain legal. -\begin{definition}\label{one_to_n_set} +\begin{definition}\label{urysohnone_one_to_n_set} $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. \end{definition} @@ -48,7 +48,7 @@ The first tept will be a formalisation of chain constructions. % together with the existence of an indexing function. % %%----------------------- -\begin{struct}\label{sequence} +\begin{struct}\label{urysohnone_sequence} A sequence $X$ is a onesorted structure equipped with \begin{enumerate} \item $\indexx$ @@ -57,8 +57,8 @@ The first tept will be a formalisation of chain constructions. \end{enumerate} such that \begin{enumerate} - \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$. - \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$. + \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} @@ -67,12 +67,12 @@ The first tept will be a formalisation of chain constructions. -\begin{definition}\label{cahin_of_subsets} +\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{chain_of_n_subsets} +\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]$. @@ -84,7 +84,7 @@ The first tept will be a formalisation of chain constructions. % and also for the subproof of continuity of the limit. -% \begin{definition}\label{legal_chain} +% \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 @@ -106,49 +106,49 @@ The first tept will be a formalisation of chain constructions. \subsection{staircase function} -\begin{definition}\label{minimum} +\begin{definition}\label{urysohnone_minimum} $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$. \end{definition} -\begin{definition}\label{maximum} +\begin{definition}\label{urysohnone_maximum} $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$. \end{definition} -\begin{definition}\label{intervalclosed} +\begin{definition}\label{urysohnone_intervalclosed} $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. \end{definition} -\begin{definition}\label{intervalopen} +\begin{definition}\label{urysohnone_intervalopen} $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$. \end{definition} -\begin{struct}\label{staircase_function} +\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{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$. - \item \label{staircase_domain} $\dom{f}$ is a topological space. - \item \label{staricase_def_chain} $C$ is a chain of subsets. - \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. - \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. - \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. - \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$. - \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ + \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{legal_staircase} +\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{urysohnspace} +\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$ @@ -156,49 +156,49 @@ The first tept will be a formalisation of chain constructions. such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. \end{abbreviation} -\begin{definition}\label{urysohnchain} +\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{urysohnchain_without_cardinality} +\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{infinte_sequence} +\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{infinite_product} +\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{refinmant} +\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{two} +\begin{abbreviation}\label{urysohnone_two} $\two = \suc{1}$. \end{abbreviation} -\begin{lemma}\label{two_in_reals} +\begin{lemma}\label{urysohnone_two_in_reals} $\two \in \reals$. \end{lemma} -\begin{lemma}\label{two_in_naturals} +\begin{lemma}\label{urysohnone_two_in_naturals} $\two \in \naturals$. \end{lemma} -\begin{inductive}\label{power_of_two} +\begin{inductive}\label{urysohnone_power_of_two} Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$. \begin{enumerate} \item $(\zero, 1) \in \powerOfTwoSet$. @@ -206,45 +206,45 @@ The first tept will be a formalisation of chain constructions. \end{enumerate} \end{inductive} -\begin{abbreviation}\label{pot} +\begin{abbreviation}\label{urysohnone_pot} $\pot = \powerOfTwoSet$. \end{abbreviation} -\begin{lemma}\label{dom_pot} +\begin{lemma}\label{urysohnone_dom_pot} $\dom{\pot} = \naturals$. \end{lemma} \begin{proof} Omitted. \end{proof} -\begin{lemma}\label{ran_pot} +\begin{lemma}\label{urysohnone_ran_pot} $\ran{\pot} \subseteq \naturals$. \end{lemma} -\begin{axiom}\label{pot1} +\begin{axiom}\label{urysohnone_pot1} $\pot \in \funs{\naturals}{\naturals}$. \end{axiom} -\begin{axiom}\label{pot2} +\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{pot_as_function} +\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{hausdorff_implies_singltons_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{urysohn_set_in_between} +\begin{lemma}\label{urysohnone_urysohn_set_in_between} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \subset B$. @@ -284,7 +284,7 @@ The first tept will be a formalisation of chain constructions. \end{proof} -\begin{proposition}\label{urysohnchain_induction_begin} +\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. @@ -347,7 +347,7 @@ The first tept will be a formalisation of chain constructions. \end{proof} -\begin{proposition}\label{urysohnchain_induction_begin_step_two} +\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. @@ -364,7 +364,7 @@ The first tept will be a formalisation of chain constructions. -\begin{proposition}\label{t_four_propositon} +\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 @@ -376,7 +376,7 @@ The first tept will be a formalisation of chain constructions. -\begin{proposition}\label{urysohnchain_induction_step_existence} +\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$. @@ -390,7 +390,7 @@ The first tept will be a formalisation of chain constructions. % 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{refinmant} + %\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$ @@ -404,7 +404,7 @@ The first tept will be a formalisation of chain constructions. -\begin{proposition}\label{existence_of_staircase_function} +\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$. @@ -416,7 +416,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{abbreviation}\label{refinment_abbreviation} +\begin{abbreviation}\label{urysohnone_refinment_abbreviation} $x \refine y$ iff $x$ is a refinmant of $y$. \end{abbreviation} @@ -424,27 +424,27 @@ The first tept will be a formalisation of chain constructions. -\begin{abbreviation}\label{sequence_of_functions} +\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{sequence_in_reals} +\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{abs_behavior1} +\begin{axiom}\label{urysohnone_abs_behavior1} If $x \geq \zero$ then $\abs{x} = x$. \end{axiom} -\begin{axiom}\label{abs_behavior2} +\begin{axiom}\label{urysohnone_abs_behavior2} If $x < \zero$ then $\abs{x} = \neg{x}$. \end{axiom} -\begin{abbreviation}\label{converge} +\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 @@ -454,7 +454,7 @@ The first tept will be a formalisation of chain constructions. \end{abbreviation} -\begin{definition}\label{limit_of_sequence} +\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$ @@ -463,7 +463,7 @@ The first tept will be a formalisation of chain constructions. we have $\abs{x - \indexx[s](n)} < \epsilon$. \end{definition} -\begin{proposition}\label{existence_of_limit} +\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$. @@ -472,22 +472,22 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{definition}\label{limit_sequence} +\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{realsminus} +\begin{definition}\label{urysohnone_realsminus} $\realsminus = \{r \in \reals \mid r < \zero\}$. \end{definition} -\begin{abbreviation}\label{realsplus} +\begin{abbreviation}\label{urysohnone_realsplus} $\realsplus = \reals \setminus \realsminus$. \end{abbreviation} -\begin{proposition}\label{intervalclosed_subseteq_reals} +\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals} Suppose $a,b \in \reals$. Suppose $a < b$. Then $\intervalclosed{a}{b} \subseteq \reals$. @@ -495,7 +495,7 @@ The first tept will be a formalisation of chain constructions. -\begin{lemma}\label{fraction1} +\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} @@ -503,7 +503,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{lemma}\label{frection2} +\begin{lemma}\label{urysohnone_frection2} Suppose $a,b \in \reals$. Suppose $a < b$. Then $\intervalopen{a}{b}$ is infinite. @@ -512,7 +512,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{lemma}\label{frection3} +\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$. @@ -521,7 +521,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{proposition}\label{fraction4} +\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)}$. @@ -530,7 +530,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{proposition}\label{fraction5} +\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)}$. @@ -539,17 +539,17 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{proposition}\label{fraction6} +\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{epsilonball} +\begin{abbreviation}\label{urysohnone_epsilonball} $\epsBall{a}{\epsilon} = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$. \end{abbreviation} -\begin{proposition}\label{fraction7} +\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}$. @@ -561,11 +561,11 @@ The first tept will be a formalisation of chain constructions. -%\begin{definition}\label{sequencetwo} +%\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{sequence_existence} +%\begin{proposition}\label{urysohnone_sequence_existence} % Suppose $N \subseteq \naturals$. % Suppose $M \subseteq \naturals$. % Suppose $N = M$. @@ -586,7 +586,7 @@ The first tept will be a formalisation of chain constructions. -\begin{theorem}\label{urysohn} +\begin{theorem}\label{urysohnone_urysohn1} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. @@ -599,7 +599,7 @@ The first tept will be a formalisation of chain constructions. 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{urysohnchain_induction_begin}. + 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$ @@ -919,6 +919,6 @@ The first tept will be a formalisation of chain constructions. % \end{subproof} \end{proof} % -%\begin{theorem}\label{safe} +%\begin{theorem}\label{urysohnone_safe} % Contradiction. %\end{theorem} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index ce6d742..08841da 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -40,7 +40,7 @@ \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 $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. + $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} @@ -49,11 +49,11 @@ \end{definition} \begin{definition}\label{urysohn_finer_set} - $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$. + $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 - $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$. + $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} @@ -92,6 +92,46 @@ $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} @@ -659,33 +699,26 @@ \end{proof} -\begin{definition}\label{staircase} - $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$. -\end{definition} - -\begin{definition}\label{staircase_sequence} - $S$ is staircase sequence of $U$ 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 $U$. -\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{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{definition}\label{staircase_limit_function} -% $f$ is a limit function of 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{proposition}\label{staircase_limit_is_continuous} -% Suppose $X$ is a urysohnspace. -% Suppose $U$ is a lifted urysohnchain of $X$. -% Suppose $S$ is staircase sequence of $U$. -% Suppose $f$ is the limit function of a staircase $S$. -% Then $f$ is continuous. -%\end{proposition} +\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. @@ -712,8 +745,26 @@ 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} @@ -721,8 +772,8 @@ 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. + 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]$. @@ -796,46 +847,133 @@ \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$. + 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$. + 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}$. + Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. + Therefore $x \notin (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$. + Then $g(x) = 1$ . + \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.} + \begin{byCase} + \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.} + $g(x) = \zero$. + \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$. + \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} +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} -% -%Ideen: -%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat -% -%zulässig und verfeinerung von ketten als predicat definieren. -% -%limits und punkt konvergenz als prädikat. -% -% -%Vor dem Beweis vor dem eigentlichen Beweis. -%die abgeleiteten Funktionen -% -%\derivedstiarcasefunction on A -% -%abbreviation: \at{f}{n} = f_{n} -% -% -%TODO: -%Reals ist ein topologischer Raum -% -- cgit v1.2.3 From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 23 Sep 2024 03:05:41 +0200 Subject: Abgabe --- library/algebra/group.tex | 2 +- library/algebra/monoid.tex | 2 +- library/cardinal.tex | 2 +- library/numbers.tex | 2 +- library/topology/basis.tex | 2 +- library/topology/continuous.tex | 2 ++ library/topology/metric-space.tex | 4 ++-- library/topology/real-topological-space.tex | 2 +- library/topology/separation.tex | 2 ++ library/topology/topological-space.tex | 2 +- library/topology/urysohn.tex | 4 ++-- library/topology/urysohn2.tex | 18 ++++++++++++++---- 12 files changed, 29 insertions(+), 15 deletions(-) (limited to 'library/topology/urysohn.tex') diff --git a/library/algebra/group.tex b/library/algebra/group.tex index 7de1051..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 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 044e5d1..5682619 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -1,4 +1,4 @@ -\section{Cardinality} +\section{Cardinality}\label{form_sec_cardinality} \import{set.tex} \import{ordinal.tex} diff --git a/library/numbers.tex b/library/numbers.tex index ac0a683..d3af3f1 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -4,7 +4,7 @@ \import{ordinal.tex} -\section{The real numbers} +\section{The numbers}\label{form_sec_numbers} \begin{signature} $\reals$ is a set. diff --git a/library/topology/basis.tex b/library/topology/basis.tex index 052c551..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 diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex index a9bc58e..95c4d0a 100644 --- a/library/topology/continuous.tex +++ b/library/topology/continuous.tex @@ -3,6 +3,8 @@ \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} diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 0ed7bab..031aa0f 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -4,10 +4,10 @@ \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 $\reaaals$ and + $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and for all $x,y,z \in M$ we have $f(x,x) = \zero$ and $f(x,y) = f(y,x)$ and diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index c76fd46..db7ee94 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -11,7 +11,7 @@ \import{function.tex} -\section{Topology Reals} +\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\}$. diff --git a/library/topology/separation.tex b/library/topology/separation.tex index 0c68290..aaa3907 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -1,6 +1,8 @@ \import{topology/topological-space.tex} \import{set.tex} +\subsection{Separation}\label{form_sec_separation} + % T0 separation \begin{definition}\label{is_kolmogorov} $X$ is Kolmogorov iff diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index f8bcb93..409e107 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -2,7 +2,7 @@ \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 diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index ae03273..cd85fbc 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -13,7 +13,7 @@ \import{set/fixpoint.tex} \import{set/product.tex} -\section{Urysohns Lemma} +\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. @@ -22,7 +22,7 @@ %Chains of sets. -The first tept will be a formalisation of chain constructions. +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$. diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 08841da..a1a3ba0 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -15,7 +15,7 @@ \import{topology/real-topological-space.tex} \import{set/equinumerosity.tex} -\section{Urysohns Lemma} +\section{Urysohns Lemma}\label{form_sec_urysohn} @@ -891,15 +891,25 @@ \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}$. - Therefore $x \notin \closure{\at{U'}{\min{\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})$. - Then $g(x) = 1$ . + 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}$.} - $g(x) = \zero$. + 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} -- cgit v1.2.3