diff options
| -rw-r--r-- | library/algebra/group.tex | 10 | ||||
| -rw-r--r-- | library/everything.tex | 1 | ||||
| -rw-r--r-- | library/topology/urysohn.tex | 182 | ||||
| -rw-r--r-- | library/topology/urysohn2.tex | 183 |
4 files changed, 312 insertions, 64 deletions
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/everything.tex b/library/everything.tex index b966197..94dd6d8 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -30,6 +30,7 @@ \import{topology/disconnection.tex} \import{topology/separation.tex} \import{numbers.tex} +\import{topology/urysohn2.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index b8a5fa5..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)$. @@ -100,6 +105,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 +135,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} @@ -220,6 +236,52 @@ 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. @@ -311,13 +373,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 +618,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,14 +647,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} @@ -658,6 +729,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} @@ -677,11 +749,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} @@ -690,51 +763,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$. @@ -841,7 +917,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} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index ea49a6c..c0b46c4 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -15,6 +15,34 @@ \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{definition}\label{sequence} + $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$. +\end{definition} \begin{abbreviation}\label{urysohnspace} @@ -26,13 +54,81 @@ \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]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. +\end{definition} + + +\begin{definition}\label{urysohnchain}%<-- zulässig + $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$. +\end{definition} + + +\begin{definition}\label{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{proposition}\label{iff_sequence} + Suppose $X$ is a function. + Suppose $\dom{X} \subseteq \naturals$. + Then $X$ is a sequence. +\end{proposition} + + + + + +\begin{theorem}\label{urysohnsetinbeetween} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $\closure{A}{X} \subseteq \interior{B}{X}$. + Suppose $\carrier[X]$ is inhabited. + There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$. +\end{theorem} +\begin{proof} + Omitted. +\end{proof} + + \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -42,21 +138,86 @@ and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous. \end{theorem} \begin{proof} - - - Define $f : X \to \reals$ such that $f(x) = $ + Let $X' = \carrier[X]$. + Let $N = \{\zero, 1\}$. + $1 = \suc{\zero}$. + $1 \in \naturals$ and $\zero \in \naturals$. + $N \subseteq \naturals$. + Let $A' = (X' \setminus B)$. + $B \subseteq X'$ by \cref{powerset_elim,closeds}. + $A \subseteq X'$. + Therefore $A \subseteq A'$. + Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$ \begin{cases} - &(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 + &A &\text{if} n = \zero \\ + &A' &\text{if} n = 1 \end{cases} + $U_0$ is a function. + $\dom{U_0} = N$. + $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. + $U_0$ is a sequence. + We have $1, \zero \in N$. + We show that $U_0$ is a chain of subsets in $X$. + \begin{subproof} + We have $\dom{U_0} \subseteq \naturals$. + We have for all $n \in \dom{U_0}$ we have $\at{U_0}{n} \subseteq \carrier[X]$ by \cref{topological_prebasis_iff_covering_family,union_as_unions,union_absorb_subseteq_left,subset_transitive,setminus_subseteq}. + We have $\dom{U_0} = \{\zero, 1\}$. + + It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$. + + Fix $n \in \dom{U_0}$. + Fix $m \in \dom{U_0}$. + + \begin{byCase} + \caseOf{$n \neq \zero$.} + Trivial. + \caseOf{$n = \zero$.} + \begin{byCase} + \caseOf{$m = \zero$.} + Trivial. + \caseOf{$m \neq \zero$.} + We have $A \subseteq A'$. + We have $\at{U_0}{\zero} = A$ by assumption. + We have $\at{U_0}{1}= A'$ by assumption. + \end{byCase} + \end{byCase} + + \end{subproof} + $U_0$ is a urysohnchain of $X$. + + %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain. + + - Trivial. - \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 +% + |