From 3d6ce5e9d5e63a5e5ed833516c62ad056e506775 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 4 Jun 2024 15:29:13 +0200 Subject: Proof of teeone_implies_singletons_closed The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing. --- library/topology/separation.tex | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) (limited to 'library/topology/separation.tex') diff --git a/library/topology/separation.tex b/library/topology/separation.tex index f70cb50..f055495 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -73,10 +73,39 @@ \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$. + %Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. Ambigus Phrase. if Omitted is ereased. \end{proposition} \begin{proof} - Omitted. + %Omitted. + %Fix $x \in 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$. + 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} + + + + + % Let $U_{y} \in \opens[X]$ such that $x \neq y \in X$. Error: unexpected '{' expecting digit + %For all $y$ there exists $U$ such that $x \neq y$ and $y \in U$ and $U \in \opens[X]$. + % 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. -- cgit v1.2.3 From 3502f06c933df7e6177634a519d8c17c2a4d2d57 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 4 Jun 2024 15:49:18 +0200 Subject: Proof of teetwo_space_is_teeone_space --- library/topology/separation.tex | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'library/topology/separation.tex') diff --git a/library/topology/separation.tex b/library/topology/separation.tex index f055495..530a51f 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -99,10 +99,6 @@ For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. Follows by set extensionality. \end{subproof} - - - - % Let $U_{y} \in \opens[X]$ such that $x \neq y \in X$. Error: unexpected '{' expecting digit %For all $y$ there exists $U$ such that $x \neq y$ and $y \in U$ and $U \in \opens[X]$. @@ -149,5 +145,13 @@ 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} -- cgit v1.2.3 From cfc0b3c9081c242d7bdefe61fc841f31e7a7a257 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 11 Jun 2024 21:49:06 +0200 Subject: proof of complement_interior_eq_closure_complement and some more about clousures(unsatable) --- library/topology/separation.tex | 10 --- library/topology/topological-space.tex | 136 ++++++++++++++++++++++++++++++++- 2 files changed, 135 insertions(+), 11 deletions(-) (limited to 'library/topology/separation.tex') diff --git a/library/topology/separation.tex b/library/topology/separation.tex index 530a51f..535a51f 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -75,11 +75,8 @@ Let $X$ be a \teeone-space. Assume $x \in \carrier[X]$. Then $\{x\}$ is closed in $X$. - %Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. Ambigus Phrase. if Omitted is ereased. \end{proposition} \begin{proof} - %Omitted. - %Fix $x \in 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$. For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. @@ -99,13 +96,6 @@ For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. Follows by set extensionality. \end{subproof} - % Let $U_{y} \in \opens[X]$ such that $x \neq y \in X$. Error: unexpected '{' expecting digit - %For all $y$ there exists $U$ such that $x \neq y$ and $y \in U$ and $U \in \opens[X]$. - - % 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]. \end{proof} % % Conversely, if \{x\} is open, then for any y distinct from x we can use diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 2bbdf09..2590287 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -217,12 +217,146 @@ \end{proof} +%Def: $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$. + +\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}\label{subseteq_of_all_then_subset_of_union} + Let $A,F$ be sets. + Suppose for all $X \in F$ we have $A \subseteq X$. + Then $A \subseteq \unions{F}$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$F$ is empty.} Trivial. + \caseOf{$F$ is inhabited.} + There exist $X \in F$ such that $X \subseteq \unions{F}$. + $A \subseteq X \subseteq \unions{F}$. + \end{byCase} +\end{proof} + +\begin{proposition}\label{subseteq_inters_iff_to_left} + Let $A,F$ be sets. + 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$.} + 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} + + %It suffices to show that for all $a \in A$ we have $x \in \inters{F}$. % This have been proven!!! But it shouldn't. + +% we show that there exist $Y \in F$ such that $a \in Y$. +% \begin{subproof} + +% \begin{byCase} +% \caseOf{$a = \emptyset$.} +% $\emptyset \subseteq \inters{F}$. +% $\emptyset \in \emptyset$. +% \caseOf{$a \neq \emptyset$.} Omitted. +% \end{byCase} + + %cases by a = \emptyset + %case a \neq \emptyset +% \end{subproof} +\end{proof} + +%------------------------ Only example ------------------------------------- +\begin{proposition}\label{subseteq_inters_iff_new} + $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$. +\end{proposition} +%\begin{proof} +% We show that if $A \subseteq \inters{F}$ then for all $X \in F$ we have $A \subseteq X$. +% \begin{subproof} + %It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$. + %Fix $a \in A$. + %Fix $X \in F$. %TODO: Missmatched Assume! + +% It suffices to show that for all $a,X$ such that $a \in A$ and $X \in F$ we have $a \in X$. +% Follows by \cref{inters}. +% \end{subproof} +% We show that for all $X \in F$ such that $A \subseteq X$ we have $A \subseteq \inters{F}$. +% \begin{subproof} +% Omitted. +% \end{subproof} +%\end{proof} + +\begin{proposition}\label{set_is_subseteq_to_closure_of_the_set} + $A \subseteq \closure{A}{X}$. +\end{proposition} +\begin{proof} + %$\closures{A}{X}$ is inhabited. %TODO: Inhabited why does "subseteq_inters_iff" has inhabited as assumtion?? + For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$. + Therefore $A \subseteq \inters{\closures{A}{X}}$. +\end{proof} + +\begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_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}$. + +\end{proof} + \begin{proposition}%[Complement of interior equals closure of complement] \label{complement_interior_eq_closure_complement} + Let $X$ be a topological space. $\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]$. + For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \in A \implies x \notin B$. + For all $x \in X$ such that $A \union B = X$ and $A \inter B = \emptyset$ we have $x \notin A \implies x \in B$. + $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$. + %$(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. %TODO: + $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]$. %TODO: + 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}$. %TODO: + + %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}$. + % \begin{byCase} + % \caseOf{$x \in \carrier[X] \setminus A$.} + % Trivial. + % \caseOf{$x \in \carrier[X] \setminus A \inter \interior{A}{X}$.} + % $\carrier[X] \setminus \closure{A}{X} \in \opens[X]$. + % $\interior{A}{X} \in \opens[X]$. + % Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X} \in \opens[X]$. + % %$\carrier[X] \setminus \closure{A}{X}$ is open. TODO: is open throws an error! + % %$\interior{A}{X}$ is open. + % %Therefore $\carrier[X] \setminus \closure{A}{X} \inter \interior{A}{X}$ is open. + % + % \end{byCase} + %\end{subproof} + %Suffices reduction by \cref ::::: reduction => goal. + + + %Omitted. % Use general De Morgan's Law in Pow|X| \end{proof} \begin{definition}[Frontier]\label{frontier} -- cgit v1.2.3 From 9563a18e455469bc64a9a8f61a95fb33f506bed0 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 18 Jun 2024 17:07:15 +0200 Subject: Definition of T3 and regular spaces. --- library/topology/separation.tex | 43 ++++++++++++++++++++++++++++++++++ library/topology/topological-space.tex | 26 ++++++-------------- 2 files changed, 50 insertions(+), 19 deletions(-) (limited to 'library/topology/separation.tex') diff --git a/library/topology/separation.tex b/library/topology/separation.tex index 535a51f..3268bb9 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -145,3 +145,46 @@ $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. \end{subproof} \end{proof} + +\begin{definition}\label{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{definition}\label{regular_space} + $X$ is a regular space iff $X$ is a topological space and $X$ is regular. +\end{definition} + + +\begin{definition}\label{teethree} + $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ . +\end{definition} + +\begin{definition}\label{teethree_space} + $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . +\end{definition} + +\begin{proposition}\label{teethree_space_is_teetwo_space} + Let $X$ be a \teethree-space. + Then $X$ is a \teetwo-space. +\end{proposition} +\begin{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]$. + + %There exist $U' \in \opens[X]$ such that $x\in U'\not\ni y$ or $x\notin U'\ni y$ by \cref{}. + %There exist $C \in \closeds{X}$ such that $y \in C \not\ni 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} + Omitted. + \end{subproof} + $y \in V$. + Follows by assumption. +\end{proof} + +% 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$. \ No newline at end of file diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 7ff588d..c40aba4 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -239,18 +239,12 @@ Then $A \subseteq \unions{F}$. \end{proposition} \begin{proof} - \begin{byCase} - %\caseOf{$F$ is empty.} - %For all $X$ we have $X \notin F$. - %If $X \in F$ and $A \in X$ then $A \in F$. - %Contradiction by assumption. - %Omitted. - \caseOf{$F$ is inhabited.} - There exist $X \in F$ such that $X \subseteq \unions{F}$. - $A \subseteq X \subseteq \unions{F}$. - \end{byCase} + 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!! @@ -379,10 +373,6 @@ 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} @@ -426,17 +416,15 @@ \end{byCase} \end{proof} -\begin{definition}\label{set_of_closeds} - $\closeds[X] = \{ Y \in \pow{\carrier[X]} \mid \text{$Y$ is closed in $X$}\}$. -\end{definition} + \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$. + 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,set_of_closeds,inters_subseteq_elem,closures}. + Follows by \cref{closure,closeds,inters_subseteq_elem,closures}. \end{proof} \begin{proposition}\label{complement_interior_eq_closure_complement} -- cgit v1.2.3 From 6839f79e775d8ffa36d421f4e3c08528323eaf17 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Thu, 20 Jun 2024 12:59:41 +0200 Subject: [Report] Task failed and was proven in the same time. The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following: time stack exec zf -- --log library/topology/separation.tex -t 30 --dump ./dump [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))). [Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))). [Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))). [Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))). [Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)). [Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))). [Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))). Verification failed: prover found countermodel fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))). fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)). fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)). real 0m14.914s user 0m37.867s sys 0m1.956s --- library/topology/separation.tex | 101 +++++++++++++++++++++++++++++++++------- 1 file changed, 85 insertions(+), 16 deletions(-) (limited to 'library/topology/separation.tex') diff --git a/library/topology/separation.tex b/library/topology/separation.tex index 3268bb9..c53b6a8 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} @@ -146,28 +146,65 @@ \end{subproof} \end{proof} -\begin{definition}\label{regular} +\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{definition}\label{regular_space} +\begin{abbreviation}\label{regular_space} $X$ is a regular space iff $X$ is a topological space and $X$ is regular. -\end{definition} +\end{abbreviation} -\begin{definition}\label{teethree} +\begin{abbreviation}\label{teethree} $X$ is \teethree\ iff $X$ is regular and $X$ is \teezero\ . -\end{definition} +\end{abbreviation} -\begin{definition}\label{teethree_space} +\begin{abbreviation}\label{teethree_space} $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . -\end{definition} +\end{abbreviation} + +\begin{proposition}\label{eqvilance_teethree_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} + + We show that if $X$ is \teethree\ then 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$. + \begin{subproof} + 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]$. + There exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$ by \cref{is_regular}. + $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$. + Particularly, $N \in \neighbourhoods{x}{X}$. + \end{subproof} + We show that if 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$ then $X$ is \teethree\ . + \begin{subproof} + Omitted. + \end{subproof} +\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$. @@ -175,16 +212,48 @@ 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]$. - %There exist $U' \in \opens[X]$ such that $x\in U'\not\ni y$ or $x\notin U'\ni y$ by \cref{}. - %There exist $C \in \closeds{X}$ such that $y \in C \not\ni 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} - Omitted. + 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$. + $y \in V$ by assumption. Follows by assumption. -\end{proof} -% 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$. \ No newline at end of file + +%\end{proof} -- cgit v1.2.3 From c19415b970d502d662eb10c403728fa41cdbe03e Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 25 Jun 2024 00:06:14 +0200 Subject: [Stable] Implented continuous.tex and omitted some proves All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex --- library/topology/continuous.tex | 29 ++++++++++ library/topology/separation.tex | 98 +++++++++++++++++++++------------- library/topology/topological-space.tex | 17 ++++-- 3 files changed, 103 insertions(+), 41 deletions(-) create mode 100644 library/topology/continuous.tex (limited to 'library/topology/separation.tex') 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/separation.tex b/library/topology/separation.tex index c53b6a8..0c68290 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -77,25 +77,26 @@ Then $\{x\}$ is closed in $X$. \end{proposition} \begin{proof} - 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$. - 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} + Omitted. + %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 @@ -163,38 +164,59 @@ $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . \end{abbreviation} -\begin{proposition}\label{eqvilance_teethree_closed_neighbourhood_in_open} +\begin{proposition}\label{teethree_implies_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$. + 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} - We show that if $X$ is \teethree\ then 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$. +\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} - 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]$. - There exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$ by \cref{is_regular}. - $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$. - Particularly, $N \in \neighbourhoods{x}{X}$. + %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 $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$ then $X$ is \teethree\ . + + 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} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 8da29d3..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} @@ -175,6 +177,9 @@ 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} $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$. @@ -297,7 +302,8 @@ \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}$. + 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} @@ -381,6 +387,7 @@ 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'})$. @@ -389,7 +396,7 @@ $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)$. + 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}$. @@ -522,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} -- 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/separation.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