diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/everything.tex | 9 | ||||
| -rw-r--r-- | library/numbers.tex | 260 | ||||
| -rw-r--r-- | library/relation.tex | 3 | ||||
| -rw-r--r-- | library/set.tex | 3 | ||||
| -rw-r--r-- | library/topology/basis.tex | 51 | ||||
| -rw-r--r-- | library/topology/continuous.tex | 29 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 77 | ||||
| -rw-r--r-- | library/topology/separation.tex | 171 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 293 |
9 files changed, 717 insertions, 179 deletions
diff --git a/library/everything.tex b/library/everything.tex index 61bccb2..29b97b7 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -16,20 +16,25 @@ \import{relation/uniqueness.tex} \import{function.tex} \import{ordinal.tex} -%\import{nat.tex} +\import{nat.tex} \import{cardinal.tex} \import{algebra/magma.tex} \import{algebra/semigroup.tex} \import{algebra/monoid.tex} \import{algebra/group.tex} + \import{order/order.tex} %\import{order/semilattice.tex} \import{topology/topological-space.tex} \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} -\import{numbers.tex} +%\import{numbers.tex} \begin{proposition}\label{trivial} $x = x$. \end{proposition} + +\begin{proposition}\label{safe} + Contradiction. +\end{proposition} diff --git a/library/numbers.tex b/library/numbers.tex index 5dd06da..f13214d 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -1,17 +1,9 @@ -\import{nat.tex} \import{order/order.tex} \import{relation.tex} +\import{set/suc.tex} \section{The real numbers} -%TODO: Implementing Notion for negativ number such as -x. - -%TODO: -%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher -%\cdot für multiklikation verwenden. -%< für die relation benutzen. -% sup und inf einfügen - \begin{signature} $\reals$ is a set. \end{signature} @@ -21,31 +13,66 @@ \end{signature} \begin{signature} - $x \times y$ is a set. + $x \rmul y$ is a set. \end{signature} +%Structure TODO: +% Take as may axioms as needed - Tarski Axioms of reals +%Implement Naturals -> Integer -> rationals -> reals + + +\subsection{Basic axioms of the reals} + +\begin{axiom}\label{reals_axiom_zero_in_reals} + $\zero \in \reals$. +\end{axiom} + \begin{axiom}\label{one_in_reals} $1 \in \reals$. \end{axiom} -\begin{axiom}\label{reals_axiom_order} - $\lt[\reals]$ is an order on $\reals$. +\begin{axiom}\label{zero_neq_one} + $\zero \neq 1$. \end{axiom} -\begin{axiom}\label{reals_axiom_strictorder} - $\lt[\reals]$ is a strict order. -\end{axiom} +\begin{inductive}\label{naturals_subset_reals} + Define $\naturals \subseteq \reals$ inductively as follows. + \begin{enumerate} + \item $\zero \in \naturals$. + \item If $n\in \naturals$, then $\successor{n} \in \naturals$. + \end{enumerate} +\end{inductive} + +%\begin{axiom}\label{negativ_is_set} +% $\negativ{x}$ is a set. +%\end{axiom} + +%\begin{axiom}\label{negativ_of} +% $\negativ{x} \in \reals$ iff $x\in \reals$. +%\end{axiom} +% +%\begin{axiom}\label{negativ_behavior} +% $x + \negativ{x} = \zero$. +%\end{axiom} + +\begin{definition}\label{reals_definition_order_def} + $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$. +\end{definition} + +%\begin{axiom}\label{reals_axiom_order} +% $\lt[\reals]$ is an order on $\reals$. +%\end{axiom} + +%\begin{abbreviation}\label{lesseq_on_reals} +% $x \leq y$ iff $(x,y) \in \lt[\reals]$. +%\end{abbreviation} \begin{abbreviation}\label{less_on_reals} - $x < y$ iff $(x,y) \in \lt[\reals]$. + $x \leq y$ iff it is wrong that $y < x$. \end{abbreviation} \begin{abbreviation}\label{greater_on_reals} - $x > y$ iff $y < x$. -\end{abbreviation} - -\begin{abbreviation}\label{lesseq_on_reals} - $x \leq y$ iff it is wrong that $x > y$. + $x > y$ iff $y \leq x$. \end{abbreviation} \begin{abbreviation}\label{greatereq_on_reals} @@ -57,25 +84,12 @@ there exist $z \in \reals$ such that $x < z$ and $z < y$. \end{axiom} -\begin{axiom}\label{reals_axiom_order_def} - $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x + z = y$. -\end{axiom} - -\begin{lemma}\label{reals_one_bigger_than_zero} - $\zero < 1$. -\end{lemma} - - \begin{axiom}\label{reals_axiom_assoc} - For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \times y) \times z = x \times (y \times z)$. + For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. \end{axiom} \begin{axiom}\label{reals_axiom_kommu} - For all $x,y \in \reals$ $x + y = y + x$ and $x \times y = y \times x$. -\end{axiom} - -\begin{axiom}\label{reals_axiom_zero_in_reals} - $\zero \in \reals$. + For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$. \end{axiom} \begin{axiom}\label{reals_axiom_zero} @@ -83,78 +97,152 @@ \end{axiom} \begin{axiom}\label{reals_axiom_one} - For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. + For all $x \in \reals$ we have $x \rmul 1 = x$. \end{axiom} \begin{axiom}\label{reals_axiom_add_invers} For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. \end{axiom} - \begin{axiom}\label{reals_axiom_mul_invers} - For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$. + For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$. \end{axiom} \begin{axiom}\label{reals_axiom_disstro1} - For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$. + For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_dedekind_complete} + For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$ + such that $x < z < y$. \end{axiom} \begin{proposition}\label{reals_disstro2} - For all $x,y,z \in \reals$ $(y + z) \times x = (y \times x) + (z \times x)$. + For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$. \end{proposition} +\begin{proof} + Omitted. +\end{proof} \begin{proposition}\label{reals_reducion_on_addition} For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{proposition} -\begin{axiom}\label{reals_axiom_dedekind_complete} - For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$ - such that $x < z < y$. -\end{axiom} + + +%\begin{signature}\label{invers_is_set} +% $\addInv{y}$ is a set. +%\end{signature} + +%\begin{definition}\label{add_inverse} +% $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$. +%\end{definition} + + +%\begin{definition}\label{add_inverse_natural_language} +% $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. +%\end{definition} + +%\begin{lemma}\label{rminus} +% $x \rminus \addInv{x} = \zero$. +%\end{lemma} + +\begin{abbreviation}\label{is_positiv} + $x$ is positiv iff $x > \zero$. +\end{abbreviation} + +\begin{lemma}\label{reals_add_of_positiv} + Let $x,y \in \reals$. + Suppose $x$ is positiv and $y$ is positiv. + Then $x + y$ is positiv. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{reals_mul_of_positiv} + Let $x,y \in \reals$. + Suppose $x$ is positiv and $y$ is positiv. + Then $x \rmul y$ is positiv. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + +\begin{lemma}\label{order_reals_lemma0} + For all $x \in \reals$ we have not $x < x$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{order_reals_lemma1} - For all $x,y,z \in \reals$ such that $\zero < x$ - if $y < z$ - then $(y \times x) < (z \times x)$. + Let $x,y,z \in \reals$. + Suppose $\zero < x$. + Suppose $y < z$. + Then $(y \rmul x) < (z \rmul x)$. \end{lemma} +\begin{proof} + Omitted. + %There exist $k \in \reals$ such that $y + k = z$ and $k > \zero$ by \cref{reals_definition_order_def}. + %\begin{align*} + % (z \rmul x) \\ + % &= ((y + k) \rmul x) \\ + % &= ((y \rmul x) + (k \rmul x)) \explanation{by \cref{reals_disstro2}} + %\end{align*} + %Then $(k \rmul x) > \zero$. + %Therefore $(z \rmul x) > (y \rmul x)$. +\end{proof} \begin{lemma}\label{order_reals_lemma2} - For all $x,y,z \in \reals$ such that $\zero < x$ - if $y < z$ - then $(x \times y) < (x \times z)$. + Let $x,y,z \in \reals$. + Suppose $\zero < x$. + Suppose $y < z$. + Then $(x \rmul y) < (x \rmul z)$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{order_reals_lemma3} - For all $x,y,z \in \reals$ such that $x < \zero$ - if $y < z$ - then $(x \times z) < (x \times y)$. + Let $x,y,z \in \reals$. + Suppose $\zero < x$. + Suppose $y < z$. + Then $(x \rmul z) < (x \rmul y)$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} -\begin{lemma}\label{o4rder_reals_lemma} - For all $x,y \in \reals$ if $x > y$ then $x \geq y$. +\begin{lemma}\label{order_reals_lemma00} + For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$. \end{lemma} + \begin{lemma}\label{order_reals_lemma5} - For all $x,y \in \reals$ if $x < y$ then $x \leq y$. + For all $x,y \in \reals$ such that $x < y$ we have $x \leq y$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{order_reals_lemma6} - For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. + For all $x,y \in \reals$ such that $x \leq y \leq x$ we have $x=y$. \end{lemma} - -\begin{axiom}\label{reals_axiom_minus} - For all $x \in \reals$ $x - x = \zero$. -\end{axiom} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{reals_minus} - Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$. + Assume $x,y \in \reals$. If $x \rminus y = \zero$ then $x=y$. \end{lemma} - -%\begin{definition}\label{reasl_supremum} %expaction "there exists" after \mid -% $\rsup{X} = \{z \mid \text{ $z \in \reals$ and for all $x,y$ such that $x \in X$ and $y,x \in \reals$ and $x < y$ we have $z \leq y$ }\}$. -%\end{definition} +\begin{proof} + Omitted. +\end{proof} \begin{definition}\label{upper_bound} $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$. @@ -168,6 +256,9 @@ %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$. If $x$ is a least upper bound of $X$ and $y$ is a least upper bound of $X$ then $x = y$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{definition}\label{supremum_reals} $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$. @@ -185,11 +276,44 @@ \end{definition} \begin{lemma}\label{infimum_unique} - %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$. If $x$ is a greatest lower bound of $X$ and $y$ is a greatest lower bound of $X$ then $x = y$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{definition}\label{infimum_reals} $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$. \end{definition} + + + +\section{The natural numbers} + + +\begin{abbreviation}\label{def_suc} + $\successor{n} = n + 1$. +\end{abbreviation} + +\begin{inductive}\label{naturals_definition_as_subset_of_reals} + Define $\nat \subseteq \reals$ inductively as follows. + \begin{enumerate} + \item $\zero \in \nat$. + \item If $n\in \nat$, then $\successor{n} \in \nat$. + \end{enumerate} +\end{inductive} + +\begin{lemma}\label{reals_order_suc} + $n < \successor{n}$. +\end{lemma} + +%\begin{proposition}\label{safe} +% Contradiction. +%\end{proposition} + +\section{The integers} + +%\begin{definition} +% $\integers = \{z \in \reals \mid z = \zero or \} $. +%\end{definition}
\ No newline at end of file diff --git a/library/relation.tex b/library/relation.tex index b5aebcd..4c4065f 100644 --- a/library/relation.tex +++ b/library/relation.tex @@ -422,6 +422,9 @@ \begin{proposition}\label{fld_cons} $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$. \end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} \begin{proposition}\label{fld_union} $\fld{(A\union B)} = \fld{A}\union\fld{B}$. diff --git a/library/set.tex b/library/set.tex index 2fd18ea..69b9526 100644 --- a/library/set.tex +++ b/library/set.tex @@ -654,6 +654,9 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio Suppose $(A\inter B)\union C = A\inter (B\union C)$. Then $C\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{union_upper_right,union_upper_left,subseteq_union_iff,subseteq_antisymmetric,subseteq_inter_iff}. +\end{proof} % From Isabelle/ZF equalities theory \begin{proposition}\label{union_inter_crazy} diff --git a/library/topology/basis.tex b/library/topology/basis.tex index 6fa9fbd..052c551 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -56,24 +56,52 @@ $\emptyset \in \genOpens{B}{X}$. \end{lemma} -\begin{lemma}\label{all_is_in_genopens} + + +\begin{lemma}\label{union_in_genopens} Assume $B$ is a topological basis for $X$. - $X \in \genOpens{B}{X}$. + Assume $F\subseteq \genOpens{B}{X}$. + Then $\unions{F}\in\genOpens{B}{X}$. \end{lemma} \begin{proof} - $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. - $\unions{B} \in \genOpens{B}{X}$. - $X \subseteq \unions{B}$. + We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}. + + Show for all $x\in \unions{F}$ there exists $W \in B$ + such that $x\in W$ and $W \subseteq \unions{F}$. + \begin{subproof} + Fix $x \in \unions{F}$. + There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}. + $V \in \genOpens{B}{X}$. + There exists $W \in B$ such that $x \in W \subseteq V$. + Then $W \subseteq \unions{F}$. + \end{subproof} + Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}. \end{proof} -\begin{lemma}\label{union_in_genopens} +\begin{lemma}\label{basis_is_in_genopens} Assume $B$ is a topological basis for $X$. - For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$. + $B \subseteq \genOpens{B}{X}$. \end{lemma} \begin{proof} - Omitted. + We show for all $V \in B$ $V \in \genOpens{B}{X}$. + \begin{subproof} + Fix $V \in B$. + For all $x \in V$ $x \in V \subseteq V$. + $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $V \in \pow{X}$. + $V \in \genOpens{B}{X}$. + \end{subproof} \end{proof} +\begin{lemma}\label{all_is_in_genopens} + Assume $B$ is a topological basis for $X$. + $X \in \genOpens{B}{X}$. +\end{lemma} +\begin{proof} + $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $\unions{B} \in \genOpens{B}{X}$. + $X \subseteq \unions{B}$. +\end{proof} \begin{lemma}\label{inters_in_genopens} Assume $B$ is a topological basis for $X$. @@ -92,16 +120,13 @@ Then $x\in A,C$. There exists $V' \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}. There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}. - There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$. + There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$ by \cref{topological_basis}. Show $W \subseteq (A\inter C)$. \begin{subproof} - %$W \subseteq v'$ and $W \subseteq V''$. For all $y \in W$ we have $y \in V'$ and $y \in V''$. \end{subproof} \end{subproof} - %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$ - %such that $x\in W$ and $W \subseteq (A\inter C)$. - $(A\inter C) \in \genOpens{B}{X}$. + $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}. \end{proof} diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex new file mode 100644 index 0000000..6a32353 --- /dev/null +++ b/library/topology/continuous.tex @@ -0,0 +1,29 @@ +\import{topology/topological-space.tex} +\import{relation.tex} + +\begin{definition}\label{continuous} + $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. +\end{definition} + +\begin{proposition}\label{continuous_definition_by_closeds} + Let $X$ be a topological space. + Let $Y$ be a topological space. + Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. +\end{proposition} +\begin{proof} + Omitted. + %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. + %\begin{subproof} + % Suppose $f$ is continuous. + % Fix $U \in \closeds{Y}$. + % $\carrier[Y] \setminus U$ is open in $Y$. + % Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$. + % Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$. + % $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + %\end{subproof} + %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 1c6a0ca..bcc5b8c 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -21,44 +21,16 @@ -%\begin{definition}\label{induced_topology} -% $O$ is the induced topology of $d$ in $M$ iff -% $O \subseteq \pow{M}$ and -% $d$ is a metric on $M$ and -% for all $x,r,A,B,C$ -% such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$ -% we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$. -%\end{definition} - -%\begin{definition} -% $\projcetfirst{A} = \{a \mid \exists x \in X \text{there exist $x \i } \}$ -%\end{definition} - \begin{definition}\label{set_of_balls} $\balls{d}{M} = \{ O \in \pow{M} \mid \text{there exists $x,r$ such that $r \in \reals$ and $x \in M$ and $O = \openball{r}{x}{d}$ } \}$. \end{definition} -%\begin{definition}\label{toindsas} -% $\metricopens{d}{M} = \{O \in \pow{M} \mid \text{ -% $d$ is a metric on $M$ and -% for all $x,r,A,B,C$ -% such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$ -% we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$. -% } \}$. -% -%\end{definition} - \begin{definition}\label{metricopens} $\metricopens{d}{M} = \genOpens{\balls{d}{M}}{M}$. \end{definition} -\begin{theorem} - Let $d$ be a metric on $M$. - $M$ is a topological space. -\end{theorem} - @@ -93,13 +65,6 @@ \end{lemma} -%\begin{definition}\label{lenght_of_interval} %TODO: take minus if its implemented -% $\lenghtinterval{x}{y} = r$ -%\end{definition} - - - - \begin{lemma}\label{metric_implies_topology} @@ -108,45 +73,3 @@ \end{lemma} - - - -%\begin{struct}\label{metric_space} -% A metric space $M$ is a onesorted structure equipped with -% \begin{enumerate} -% \item $\metric$ -% \end{enumerate} -% such that -% \begin{enumerate} -% \item \label{metric_space_d} $\metric[M]$ is a function from $M \times M$ to $\reals$. -% \item \label{metric_space_distence_of_a_point} $\metric[M](x,x) = \zero$. -% \item \label{metric_space_positiv} for all $x,y \in M$ if $x \neq y$ then $\zero < \metric[M](x,y)$. -% \item \label{metric_space_symetrie} $\metric[M](x,y) = \metric[M](y,x)$. -% \item \label{metric_space_triangle_equation} for all $x,y,z \in M$ $\metric[M](x,y) < \metric[M](x,z) + \metric[M](z,y)$ or $\metric[M](x,y) = \metric[M](x,z) + \metric[M](z,y)$. -% \item \label{metric_space_topology} $M$ is a topological space. -% \item \label{metric_space_opens} for all $x \in M$ for all $r \in \reals$ $\{z \in M \mid \metric[M](x,z) < r\} \in \opens$. -% \end{enumerate} -%\end{struct} - -%\begin{definition}\label{open_ball} -% $\openball{r}{x}{M} = \{z \in M \mid \metric(x,z) < r\}$. -%\end{definition} - -%\begin{proposition}\label{open_ball_is_open} -% Let $M$ be a metric space,let $r \in \reals $, let $x$ be an element of $M$. -% Then $\openball{r}{x}{M} \in \opens[M]$. -%\end{proposition} - - - - - - -%TODO: - Basis indudiert topology lemma -% - Offe Bälle sind basis - -% Was danach kommen soll bleibt offen, vll buch oder in proof wiki -% Trennungsaxiom, - -% Notaionen aufräumen damit das gut gemercht werden kann. - diff --git a/library/topology/separation.tex b/library/topology/separation.tex index f70cb50..0c68290 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -1,5 +1,5 @@ \import{topology/topological-space.tex} - +\import{set.tex} % T0 separation \begin{definition}\label{is_kolmogorov} @@ -73,14 +73,30 @@ \begin{proposition}\label{teeone_implies_singletons_closed} Let $X$ be a \teeone-space. - Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. + Assume $x \in \carrier[X]$. + Then $\{x\}$ is closed in $X$. \end{proposition} \begin{proof} Omitted. - % TODO - % Choose for every y distinct from x and open subset U_y containing y but not x. - % The union U of all the U_y is open. - % {x} is the complement of U in \carrier[X]. + %Let $V = \{ U \in \opens[X] \mid x \notin U\}$. + %For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$ by \cref{carrier_open,teeone}. + %For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. + % + %$\unions{V} \in \opens[X]$. + %For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$. + %We show that $\carrier[X] \setminus \{x\} = \unions{V}$. + %\begin{subproof} + % We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$. + % \begin{subproof} + % Fix $y \in \carrier[X] \setminus \{x\}$. + % $y \neq x$. + % $y \in \carrier[X]$. + % $y \in \unions{V}$. + % \end{subproof} + % For all $y \in \unions{V}$ we have $y \notin \{x\}$. + % For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. + % Follows by set extensionality. + %\end{subproof} \end{proof} % % Conversely, if \{x\} is open, then for any y distinct from x we can use @@ -120,5 +136,146 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - Omitted. % TODO + We show that for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $U\ni x\notin V$ and $V\ni y\notin U$. + \begin{subproof} + $X$ is hausdorff. + For all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. + \end{subproof} +\end{proof} + +\begin{definition}\label{is_regular} + $X$ is regular iff for all $C,p$ such that $p \in \carrier[X]$ and $p \notin C \in \closeds{X}$ we have there exists $U,C \in \opens[X]$ such that $p \in U$ and $C \subseteq V$ and $U \inter V = \emptyset$. +\end{definition} + +\begin{abbreviation}\label{regular_space} + $X$ is a regular space iff $X$ is a topological space and $X$ is regular. +\end{abbreviation} + + +\begin{abbreviation}\label{teethree} + $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ . +\end{abbreviation} + +\begin{abbreviation}\label{teethree_space} + $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . +\end{abbreviation} + +\begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + Suppose $X$ is \teethree\ . + For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. +\end{proposition} +\begin{proof} + Omitted. + %%Suppose $X$ is regular and kolmogorov. + %Fix $U \in \opens[X]$. + %Fix $x \in U$. + %Let $C = \carrier[X] \setminus U$. + %Then $C \in \closeds{X}$. + %$x \notin C$. + %$x \in \carrier[X]$. + %We show that there exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$. + %We show that $B \subseteq (\carrier[X] \setminus A)$. + %$(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$. + %$(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$. + %$x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$. + %Let $N = (\carrier[X] \setminus A)$. + %Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$. + %$N \in \neighbourhoods{x}{X}$. \end{proof} + +\begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. +\end{proposition} +\begin{proof} + We show that if $X$ is \teethree\ then for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. + \begin{subproof} + %For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. + Omitted. + \end{subproof} + + We show that if for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$ then $X$ is \teethree\ . + \begin{subproof} + Omitted. + \end{subproof} +\end{proof} + + +\begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} + Let $X$ be a topological space. + Suppose $X$ is inhabited. + $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. +\end{proposition} +\begin{proof} + Omitted. + %Follows by \cref{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods,teethree_implies_closed_neighbourhood_in_open}. +\end{proof} + + +\begin{proposition}\label{teethree_space_is_teetwo_space} + Let $X$ be a \teethree-space. + Suppose $X$ is inhabited. + Then $X$ is a \teetwo-space. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + For all $x,y \in \carrier[X]$ such that $x \neq y$ we have $x \notin \{y\}$. + It suffices to show that $X$ is hausdorff. + It suffices to show that for all $x \in \carrier[X]$ we have for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$. + Fix $x \in \carrier[X]$. + It suffices to show that for all $y \in \carrier[X]$ such that $y \neq x$ we have there exist $U,V \in \opens[X]$ such that $x\in U$ and $y \in V$ and $U$ is disjoint from $V$. + Fix $y \in \carrier[X]$. + + + We show that there exist $U,V,C$ such that $U,V \in \opens[X]$ and $C\in \closeds{X}$ and $x \in U$ and $y \in C \subseteq V$ and $U$ is disjoint from $V$. + \begin{subproof} + There exist $C' \in \closeds{X}$ such that $x \in \carrier[X]$ and $x \notin C' \in \closeds{X}$ and there exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$. + There exists $U',V' \in \opens[X]$ such that $x \in U'$ and $C' \subseteq V'$ and $U' \inter V' = \emptyset$. + $U'$ is disjoint from $V'$. + $x \in U'$. + $x \notin C' \subseteq V'$. + $U',V' \in \opens[X]$. + $C' \in \closeds{X}$. + We show that there exist $K \in \closeds{X}$ such that $x \notin K \ni y$. + \begin{subproof} + $X$ is Kolmogorov. + For all $x',y'\in\carrier[X]$ such that $x'\neq y'$ there exist $H\in\opens[X]$ such that $x'\in H\not\ni y'$ or $x'\notin H\ni y'$. + we show that there exist $H \in \opens[X]$ such that $x \notin H \ni y$ or $y \notin H \ni x$. + \begin{subproof} + Omitted. + \end{subproof} + $H \subseteq \carrier[X]$ by \cref{opens_type,subseteq}. + Since $\carrier[X] \ni x \notin H$ or $\carrier[X] \ni y \notin H$, we have there exist $c \in H$. + Then $H \neq \carrier[X]$. + Since $y \in H$ or $x \in H$, we have $H \neq \emptyset$. + Let $K = \carrier[X] \setminus H$. + $K$ is inhabited. + $K \in \closeds{X}$ by \cref{complement_of_open_is_closed}. + $x \notin K \ni y$ or $y \notin K \ni x$. + \begin{byCase} + \caseOf{$y \in K$.} Trivial. + \caseOf{$y \notin K$.} + Then there exist $U'',V'' \in \opens[X]$ such that $x \in U''$ and $K \subseteq V''$ and $U'' \inter V'' = \emptyset$ by \cref{is_regular}. + Let $K' = \carrier[X] \setminus U''$. + $x \in K'$. + $K' \in \closeds{X}$. + \end{byCase} + + + \end{subproof} + + Follows by assumption. + \end{subproof} + $y \in V$ by assumption. + Follows by assumption. + + +%\end{proof} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 55bc253..f8bcb93 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -1,5 +1,6 @@ \import{set.tex} \import{set/powerset.tex} +\import{set/cons.tex} \section{Topological spaces} @@ -67,7 +68,8 @@ such that $a\in U\subseteq A$. \end{proposition} \begin{proof} - Take $U\in\interiors{A}{X}$ such that $a\in U$. + Omitted. + %Take $U\in\interiors{A}{X}$ such that $a\in U$. \end{proof} \begin{proposition}[Interior]\label{interior_elem_iff} @@ -161,10 +163,22 @@ \begin{proposition}\label{carrier_is_closed} Let $X$ be a topological space. - Then $\emptyset$ is closed in $X$. + Then $\carrier[X]$ is closed in $X$. \end{proposition} \begin{proof} $\carrier[X]\setminus \carrier[X] = \emptyset$. + Follows by \cref{emptyset_open,is_closed_in}. +\end{proof} + +\begin{proposition}\label{opens_minus_closed_is_open} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Suppose $B$ is closed in $X$. + Then $A \setminus B$ is open in $X$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_eq_emptyset_iff_subseteq,is_closed_in,opens_inter,inter_comm_left,setminus_union,inter_assoc,inter_setminus,inter_lower_left,inter_lower_right,setminus_subseteq,double_complement,setminus_setminus,setminus_eq_inter_complement,setminus_self,setminus_inter,union_comm,emptyset_subseteq,setminus_partition}. \end{proof} \begin{definition}[Closed sets]\label{closeds} @@ -216,31 +230,282 @@ Follows by \cref{inters_singleton,closure}. \end{proof} +\begin{proposition}\label{subseteq_inters_iff_to_right} + Let $A,F$ be sets. + Suppose $A \subseteq \inters{F}$. + Then for all $X \in F$ we have $A \subseteq X$. +\end{proposition} + -\begin{proposition}%[Complement of interior equals closure of complement] -\label{complement_interior_eq_closure_complement} +\begin{proposition}\label{subseteq_of_all_then_subset_of_union} + Let $A,F$ be sets. + Suppose $F$ is inhabited. %TODO: Remove!! + Suppose for all $X \in F$ we have $A \subseteq X$. + Then $A \subseteq \unions{F}$. +\end{proposition} +\begin{proof} + There exist $X \in F$ such that $X \subseteq \unions{F}$. + $A \subseteq X \subseteq \unions{F}$. +\end{proof} + + + +\begin{proposition}\label{subseteq_inters_iff_to_left} + Let $A,F$ be sets. + Suppose $F$ is inhabited. % TODO:Remove!! + Suppose for all $X \in F$ we have $A \subseteq X$. + Then $A \subseteq \inters{F}$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.}Trivial. + \caseOf{$A \neq \emptyset$.} + $F$ is inhabited. + It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. + Fix $a \in A$. + For all $X \in F$ we have $a \in X$. + $A \subseteq \unions{F}$. + $a \in \unions{F}$. + \end{byCase} +\end{proof} + +\begin{proposition}\label{subseteq_inters_iff_new} + Suppose $F$ is inhabited. + $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$. +\end{proposition} + +\begin{proposition}\label{set_is_subseteq_to_closure_of_the_set} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + $A \subseteq \closure{A}{X}$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.} + Trivial. + \caseOf{$A \neq \emptyset$.} + We show that $\carrier[X] \in \closures{A}{X}$. + \begin{subproof} + $\carrier[X]$ is closed in $X$. + $\carrier[X] \in \pow{\carrier[X]}$. + \end{subproof} + $\closures{A}{X}$ is inhabited. + For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$. + Therefore $A \subseteq \inters{\closures{A}{X}}$. + \end{byCase} +\end{proof} + +\begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. +\end{proposition} +\begin{proof} + It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$. + If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$ by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,elem_subseteq,setminus}. + Follows by \cref{subseteq_setminus_cons_elim,cons_absorb,double_complement_union,union_as_unions,set_is_subseteq_to_closure_of_the_set,setminus_subseteq,setminus_intro,closure,setminus_elim_left}. +\end{proof} + +\begin{proposition}\label{complement_of_closed_is_open} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Suppose $A$ is closed in $X$. + Then $\carrier[X] \setminus A$ is open in $X$. +\end{proposition} + +\begin{proposition}\label{complement_of_open_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Then $\carrier[X] \setminus A$ is closed in $X$. +\end{proposition} + +\begin{proposition}\label{intersection_of_closed_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ are closed in $X$. + Suppose $B$ are closed in $X$. + Then $A \inter B$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. + $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) \in \opens[X]$. + $A \inter B = \carrier[X] \setminus ((\carrier[X] \setminus A) \union (\carrier[X] \setminus B))$. +\end{proof} + +\begin{proposition}\label{union_of_closed_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ are closed in $X$. + Suppose $B$ are closed in $X$. + Then $A \union B$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. + $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) \in \opens[X]$. + $A \union B = \carrier[X] \setminus ((\carrier[X] \setminus A) \inter (\carrier[X] \setminus B))$. +\end{proof} + +\begin{proposition}\label{closed_minus_open_is_closed} + Let $X$ be a topological space. + Suppose $A, B \subseteq \carrier[X]$. + Suppose $A$ is open in $X$. + Suppose $B$ is closed in $X$. + Then $B \setminus A$ is closed in $X$. +\end{proposition} + + + +\begin{proposition}\label{intersection_of_closed_is_closed_infinite} + Let $X$ be a topological space. + Suppose $F \subseteq \pow{\carrier[X]}$. + Suppose for all $A \in F$ we have $A$ is closed in $X$. + Suppose $F$ is inhabited. + Then $\inters{F}$ is closed in $X$. +\end{proposition} +\begin{proof} + Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $. + For all $Y \in F'$ we have $Y$ is open in $X$. + $\unions{F'}$ is open in $X$. + $\unions{F'}, \inters{F} \subseteq \carrier[X]$. + We show that $\inters{F} = \carrier[X] \setminus (\unions{F'})$. + \begin{subproof} + We show that for all $a \in \inters{F}$ we have $a \in \carrier[X] \setminus (\unions{F'})$. + \begin{subproof} + Fix $a \in \inters{F}$. + $a \in \carrier[X]$. + For all $A \in F$ we have $a \in A$. + For all $A \in F$ we have $a \notin (\carrier[X] \setminus A)$. + Then $a \notin \unions{F'}$. + Therefore $a \in \carrier[X] \setminus (\unions{F'})$. + \end{subproof} + We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$. + \begin{subproof} + \begin{byCase} + \caseOf{$\inters{F} = \emptyset$.} + $F$ is inhabited. + Take $U$ such that $U \in F$. + Let $F'' = F \setminus \{U\}$. + There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$. + Omitted. + \caseOf{$\inters{F} \neq \emptyset$.} + + Fix $a \in \carrier[X] \setminus (\unions{F'})$. + $\inters{F}$ is inhabited. + $a \in \carrier[X]$. + $a \notin \unions{F'}$. + For all $A \in F'$ we have $a \notin A$. + For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$. + For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$ by \cref{setminus_setminus,inter_absorb_supseteq_left,pow_iff,subseteq}. + For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$. + For all $Y \in F$ we have $a \in Y$. + Therefore $a \in \inters{F}$. + \end{byCase} + \end{subproof} + Follows by set extensionality. + \end{subproof} + Follows by \cref{complement_of_open_is_closed}. +\end{proof} + +\begin{proposition}\label{closure_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\closure{A}{X}$ is closed in $X$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$\closure{A}{X} = \emptyset$.} + Trivial. + \caseOf{$\closure{A}{X} \neq \emptyset$.} + $\closures{A}{X}$ is inhabited. + $\closures{A}{X} \subseteq \pow{\carrier[X]}$. + For all $B \in \closures{A}{X}$ we have $B$ is closed in $X$. + $\inters{\closures{A}{X}}$ is closed in $X$. + \end{byCase} +\end{proof} + + + +\begin{proposition}\label{closure_is_minimal_closed_set} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + For all $Y \in \closeds{X}$ such that $A \subseteq Y$ we have $\closure{A}{X} \subseteq Y$. +\end{proposition} +\begin{proof} + Follows by \cref{closure,closeds,inters_subseteq_elem,closures}. +\end{proof} + +\begin{proposition}\label{interior_is_maximal} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$. +\end{proposition} + +\begin{proposition}\label{complement_interior_eq_closure_complement} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - Omitted. % Use general De Morgan's Law in Pow|X| + We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$. + \begin{subproof} + + Fix $x \in \carrier[X]\setminus\interior{A}{X}$. + Suppose not. + $x \notin \closure{(\carrier[X]\setminus A)}{X}$. + $x \in \carrier[X]$. + $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$. + $x \in A$. + $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$. + $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. + There exist $U \in \opens[X]$ such that $x \in U$ and $U\subseteq A$. + $U \subseteq \interior{A}{X}$. + Contradiction. + \end{subproof} + $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$. + $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. \end{proof} + + \begin{definition}[Frontier]\label{frontier} $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. \end{definition} +\begin{proposition}\label{closure_interior_frontier_is_in_carrier} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$. +\end{proposition} + +\begin{proposition}\label{frontier_is_closed} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. + Then $\frontier{A}{X}$ is closed in $X$. +\end{proposition} +\begin{proof} + $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ by \cref{closure_interior_frontier_is_in_carrier,closure_is_closed,interior_is_open,closed_minus_open_is_closed}. +\end{proof} + +\begin{proposition}\label{setdifference_eq_intersection_with_complement} + Suppose $A,B \subseteq C$. + Then $A \setminus B = A \inter (C \setminus B)$. +\end{proposition} -\begin{proposition}%[Frontier as intersection of closures] -\label{frontier_as_inter} + +\begin{proposition}\label{frontier_as_inter} + Let $X$ be a topological space. + Suppose $A \subseteq \carrier[X]$. $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - % TODO - Omitted. - %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition) - %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement - %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement + \begin{align*} + \frontier{A}{X} \\ + &= \closure{A}{X}\setminus\interior{A}{X} \\ + &= \closure{A}{X} \inter (\carrier[X] \setminus \interior{A}{X}) \explanation{by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}}\\ + &= \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X} \explanation{by \cref{complement_interior_eq_closure_complement}} + \end{align*} \end{proof} \begin{proposition}\label{frontier_of_emptyset} @@ -264,3 +529,7 @@ \begin{definition}\label{neighbourhoods} $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$. \end{definition} + +\begin{definition}\label{neighbourhoods_set} + $\neighbourhoodsSet{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\subseteq U\subseteq N\}$. +\end{definition} |