diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/numbers.tex | 19 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 2 | ||||
| -rw-r--r-- | library/topology/real-topological-space.tex | 73 | ||||
| -rw-r--r-- | library/topology/urysohn2.tex | 73 |
4 files changed, 149 insertions, 18 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index cb3d5cf..b7de307 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -245,12 +245,31 @@ Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$. \end{proposition} +%\begin{proposition}\label{natural_disstro_oneline} +% Suppose $n,m,k \in \naturals$. +% Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. +%\end{proposition} +%\begin{proof} +% Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. +% $\zero \in P$. +% $P \subseteq \naturals$. +% It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. +% Fix $n \in P$. +% It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +% Fix $m' \in \naturals$. +% Fix $k' \in \naturals$. +% $n \in \naturals$. +% $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + m' + k' = (((n \rmul m') + (n \rmul k')) + m') + k' = (m' + ((n \rmul m') + (n \rmul k'))) + k' = ((m' + (n \rmul m')) + (n \rmul k')) + k' = (((n \rmul m') + m') + (n \rmul k')) + k' = ((n \rmul m') + m') + ((n \rmul k') + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$. +%\end{proof} + \begin{proposition}\label{natural_disstro} Suppose $n,m,k \in \naturals$. Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$. \end{proposition} \begin{proof} + %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$. Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$. + $\zero \in P$. $P \subseteq \naturals$. It suffices to show that for all $n \in P$ we have $\suc{n} \in P$. diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index bcc5b8c..0ed7bab 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -7,7 +7,7 @@ \section{Metric Spaces} \begin{definition}\label{metric} - $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and + $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ 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 239965c..db46732 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -17,10 +17,73 @@ $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. \end{definition} -\begin{theorem}\label{reals_as_topo_space} - Suppose $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$. - Then $\reals$ is a topological space. +\begin{axiom}\label{reals_carrier_reals} + $\carrier[\reals] = \reals$. +\end{axiom} + +\begin{theorem}\label{topological_basis_reals_is_prebasis} + $\topoBasisReals$ is a topological prebasis for $\reals$. \end{theorem} \begin{proof} - Omitted. -\end{proof}
\ No newline at end of file + We show that $\unions{\topoBasisReals} \subseteq \reals$. + \begin{subproof} + It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$. + Fix $x \in \unions{\topoBasisReals}$. + \end{subproof} + We show that $\reals \subseteq \unions{\topoBasisReals}$. + \begin{subproof} + It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$. + Fix $x \in \reals$. + \end{subproof} +\end{proof} + +\begin{theorem}\label{topological_basis_reals_is_basis} + $\topoBasisReals$ is a topological basis for $\reals$. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}. + Let $B = \topoBasisReals$. + It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$. + Fix $U \in B$. + Fix $V \in B$. + Fix $x \in U, V$. +\end{proof} + +\begin{axiom}\label{topological_space_reals} + $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$. +\end{axiom} + +\begin{theorem}\label{reals_is_topological_space} + $\reals$ is a topological space. +\end{theorem} +\begin{proof} + $\topoBasisReals$ is a topological basis for $\reals$. + Let $B = \topoBasisReals$. + We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$. + \begin{subproof} + It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$. + Fix $A \in \opens[\reals]$. + Follows by \cref{powerset_elim,topological_space_reals,genopens}. + \end{subproof} + We show that $\reals \in\opens[\reals]$. + \begin{subproof} + $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $\unions{B} \in \genOpens{B}{\reals}$. + $\reals \subseteq \unions{B}$. + \end{subproof} + We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,inters_in_genopens}. + \end{subproof} + We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$. + \begin{subproof} + Follows by \cref{topological_space_reals,union_in_genopens}. + \end{subproof} + $\carrier[\reals] = \reals$. + Follows by \cref{topological_space}. +\end{proof} + +\begin{proposition}\label{open_interval_is_open} + Suppose $a,b \in \reals$. + Then $\intervalopen{a}{b} \in \opens[\reals]$. +\end{proposition}
\ No newline at end of file diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 396255e..838b121 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -152,16 +152,23 @@ \begin{proposition}\label{no_natural_between_n_and_suc_n} For all $n,m \in \naturals$ we have not $n < m < \suc{n}$. \end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_is_zero_one_or_greater} + $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} \begin{proposition}\label{naturals_rless_existence_of_lesser_natural} For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$. \end{proposition} \begin{proof}[Proof by \in-induction on $n$] Assume $n \in \naturals$. - We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$. - \begin{subproof} - Trivial. - \end{subproof} + \begin{byCase} \caseOf{$n = \zero$.} @@ -196,9 +203,17 @@ We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$. \begin{subproof}[Proof by \in-induction on $m$] Assume $m \in \naturals$. - %\begin{byCase} - % - %\end{byCase} + \begin{byCase} + \caseOf{$\suc{m}=n$.} + \caseOf{$\suc{m}\neq n$.} + \begin{byCase} + \caseOf{$n = \zero$.} + \caseOf{$n \neq \zero$.} + Take $l \in \naturals$ such that $\suc{l} = n$. + Omitted. + + \end{byCase} + \end{byCase} \end{subproof} \end{subproof} @@ -323,17 +338,51 @@ For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$. \end{proposition} +\begin{proposition}\label{bijection_naturals_order} + For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + \begin{proposition}\label{existence_normal_ordered_urysohn} Let $X$ be a urysohn space. Suppose $U$ is a urysohnchain of $X$. Suppose $\dom{U}$ is finite. - Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered. + Suppose $U$ is inhabited. + Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered. \end{proposition} \begin{proof} - Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}. - There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$. - - + Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}. + \begin{byCase} + \caseOf{$n = \zero$.} + Omitted. + \caseOf{$n \neq \zero$.} + Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. + We have $\dom{U} \subseteq \naturals$. + $\dom{U}$ is inhabited. + We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. + \begin{subproof} + Omitted. + \end{subproof} + Let $N = \seq{\zero}{k}$. + Let $M = \pow{X}$. + Define $V : N \to M$ such that $V(n)=$ + \begin{cases} + &\at{U}{F(n)} & \text{if} n \in N + \end{cases} + $\dom{V} = \seq{\zero}{k}$. + We show that $V$ is a urysohnchain of $X$. + \begin{subproof} + Trivial. + \end{subproof} + We show that $F$ is consistent on $U$ to $V$. + \begin{subproof} + Trivial. + \end{subproof} + $V$ is normal ordered. + \end{byCase} + \end{proof} |