theory Topology_ZF_7 imports Topology_ZF_5
begin
This theory develops the theory of connection properties in topological spaces, including connected and disconnected spaces, hyperconnected spaces, sober spaces, and ultraconnected spaces.
Connection Properties
Another type of topological properties are the connection properties. These properties establish if the space is formed of several pieces or just one.
A space is connected iff there is no clopen set other that the empty set and the total set.
definition
\( T \text{ is connected } \equiv \forall U.\ (U\in T \wedge (U \text{ is closed in }T)) \longrightarrow U=0\vee U=\bigcup T \)
The indiscrete topology on a set is always connected.
lemma indiscrete_connected:
shows \( \{0,X\} \text{ is connected } \) unfolding IsConnected_def, IsClosed_defThe anti-property of connectedness is called total-diconnectedness.
definition
\( IsTotDis \equiv ANTI(IsConnected) \)
A set is in the connectedness spectrum iff it has cardinality at most one.
lemma conn_spectrum:
shows \( (A\text{ is in the spectrum of }IsConnected) \longleftrightarrow A\preceq 1 \)proof assume \( A\text{ is in the spectrum of }IsConnected \)
then have \( \forall T.\ (T\text{ is a topology }\wedge \bigcup T\approx A) \longrightarrow (T\text{ is connected }) \) using Spec_def
moreover
{
have \( Pow(A)\text{ is a topology } \) using Pow_is_top
moreover have \( \bigcup (Pow(A))=A \)
then have \( \bigcup (Pow(A))\approx A \)
ultimately have \( Pow(A) \text{ is connected } \)
assume \( A\neq 0 \)
then obtain \( E \) where \( E\in A \)
then have \( \{E\}\in Pow(A) \)
moreover
have \( A-\{E\}\in Pow(A) \)
ultimately have \( \{E\}\in Pow(A)\wedge \{E}\text{ is closed in }Pow(A\} \) unfolding IsClosed_def
with \( Pow(A) \text{ is connected } \) have \( \{E\}=A \) unfolding IsConnected_def
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
moreover {
}
ultimately show \( A\preceq 1 \)
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( \bigcup T=0 \)
with \( T\text{ is a topology } \) have \( T=\{0\} \) using empty_open
then have \( T\text{ is connected } \) unfolding IsConnected_def
moreover {
}
ultimately have \( T\text{ is connected } \)
assume \( \bigcup T\neq 0 \)
moreover
from \( A\preceq 1 \), \( \bigcup T\approx A \) have \( \bigcup T\preceq 1 \) using eq_lepoll_trans
ultimately obtain \( E \) where \( \bigcup T=\{E\} \) using lepoll_1_is_sing
moreover
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( T\subseteq Pow(\{E\}) \)
then have \( T\subseteq \{0,\{E\}\} \)
with \( T\text{ is a topology } \) have \( \{0\}\subseteq T \), \( T\subseteq \{0,\{E\}\} \) using empty_open
then have \( T\text{ is connected } \) unfolding IsConnected_def
then show \( A\text{ is in the spectrum of }IsConnected \) unfolding Spec_def
qed
The discrete space is a first example of totally-disconnected space.
lemma discrete_tot_dis:
shows \( Pow(X) \{is totally-disconnected\} \)proof{
}
}
fix \( A \)
assume \( A\in Pow(X) \) and con: \( (Pow(X)\text{ restricted to }A)\text{ is connected } \)
from \( A\in Pow(X) \) have res: \( (Pow(X)\text{ restricted to }A)=Pow(A) \) unfolding RestrictedTo_def
{
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
then have \( A\text{ is in the spectrum of }IsConnected \) using conn_spectrum
moreover {
}
ultimately have \( A\text{ is in the spectrum of }IsConnected \)
assume \( A\neq 0 \)
then obtain \( E \) where \( E\in A \)
then have \( \{E\}\in Pow(A) \)
moreover
have \( A-\{E\}\in Pow(A) \)
ultimately have \( \{E\}\in Pow(A)\wedge \{E}\text{ is closed in }Pow(A\} \) unfolding IsClosed_def
with con, res have \( \{E\}=A \) unfolding IsConnected_def
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
then have \( A\text{ is in the spectrum of }IsConnected \) using conn_spectrum
then show \( thesis \) unfolding IsTotDis_def, antiProperty_def
qed
An space is hyperconnected iff every two non-empty open sets meet.
definition
\( T\text{ is hyperconnected } \equiv \forall U V.\ U\in T \wedge V\in T \wedge U\cap V=0 \longrightarrow U=0\vee V=0 \)
Every hyperconnected space is connected.
lemma HConn_imp_Conn:
assumes \( T\text{ is hyperconnected } \)
shows \( T\text{ is connected } \)proof{
}
fix \( U \)
assume \( U\in T \), \( U \text{ is closed in }T \)
then have \( \bigcup T-U\in T \), \( U\in T \) using IsClosed_def
moreover
have \( (\bigcup T-U)\cap U=0 \)
moreover note assms
ultimately have \( U=0\vee (\bigcup T-U)=0 \) using IsHConnected_def
with \( U\in T \) have \( U=0\vee U=\bigcup T \)
then show \( thesis \) using IsConnected_def
qed
The indiscrete topology is hyperconnected.
lemma Indiscrete_HConn:
shows \( \{0,X}\text{ is hyperconnected \} \) unfolding IsHConnected_defA first example of an hyperconnected space but not indiscrete, is the cofinite topology on the natural numbers.
lemma Cofinite_nat_HConn:
assumes \( \neg (X\prec nat) \)
shows \( (CoFinite X)\text{ is hyperconnected } \)proof{
}
}
fix \( U \) \( V \)
assume \( U\in (CoFinite X) \), \( V\in (CoFinite X) \), \( U\cap V=0 \)
then have eq: \( (X-U)\prec nat\vee U=0 \), \( (X-V)\prec nat\vee V=0 \) unfolding Cofinite_def, CoCardinal_def
from \( U\cap V=0 \) have un: \( (X-U)\cup (X-V)=X \)
{
assume AS: \( (X-U)\prec nat \), \( (X-V)\prec nat \)
have \( (X-U)\prec nat \Longrightarrow (X-V)\prec nat \Longrightarrow (X-U)\cup (X-V)\prec nat \) using less_less_imp_un_less, InfCard_nat
with un have \( X\prec nat \) using AS
then have \( False \) using assms
with eq(1,2) have \( U=0\vee V=0 \)
then show \( (CoFinite X)\text{ is hyperconnected } \) using IsHConnected_def
qed
A set is in the hyperconnectedness spectrum iff it has cardinality at most one.
lemma HConn_spectrum:
shows \( (A\text{ is in the spectrum of }IsHConnected) \longleftrightarrow A\preceq 1 \)proof assume \( A\text{ is in the spectrum of }IsHConnected \)
then have \( \forall T.\ (T\text{ is a topology }\wedge \bigcup T\approx A) \longrightarrow (T\text{ is hyperconnected }) \) using Spec_def
moreover
{
have \( Pow(A)\text{ is a topology } \) using Pow_is_top
moreover have \( \bigcup (Pow(A))=A \)
then have \( \bigcup (Pow(A))\approx A \)
ultimately have HC_Pow: \( Pow(A)\text{ is hyperconnected } \)
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
moreover {
}
ultimately show \( A\preceq 1 \)
assume \( A\neq 0 \)
then obtain \( e \) where \( e\in A \)
then have \( \{e\}\in Pow(A) \)
moreover
have \( A-\{e\}\in Pow(A) \)
moreover have \( \{e\}\cap (A-\{e\})=0 \)
moreover note HC_Pow
ultimately have \( A-\{e\}=0 \) unfolding IsHConnected_def
with \( e\in A \) have \( A=\{e\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( \bigcup T=0 \)
with \( T\text{ is a topology } \) have \( T=\{0\} \) using empty_open
then have \( T\text{ is hyperconnected } \) unfolding IsHConnected_def
moreover {
}
ultimately have \( T\text{ is hyperconnected } \)
assume \( \bigcup T\neq 0 \)
moreover
from \( A\preceq 1 \), \( \bigcup T\approx A \) have \( \bigcup T\preceq 1 \) using eq_lepoll_trans
ultimately obtain \( E \) where \( \bigcup T=\{E\} \) using lepoll_1_is_sing
moreover
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( T\subseteq Pow(\{E\}) \)
then have \( T\subseteq \{0,\{E\}\} \)
with \( T\text{ is a topology } \) have \( \{0\}\subseteq T \), \( T\subseteq \{0,\{E\}\} \) using empty_open
then have \( T\text{ is hyperconnected } \) unfolding IsHConnected_def
then show \( A\text{ is in the spectrum of }IsHConnected \) unfolding Spec_def
qed
In the following results we will show that anti-hyperconnectedness is a separation property between \(T_1\) and \(T_2\). We will show also that both implications are proper.
First, the closure of a point in every topological space is always hyperconnected. This is the reason why every anti-hyperconnected space must be \(T_1\): every singleton must be closed.
lemma (in topology0) cl_point_imp_HConn:
assumes \( x\in \bigcup T \)
shows \( (T\text{ restricted to } \text{Closure}(\{x\},T))\text{ is hyperconnected } \)proof from assms have sub: \( \text{Closure}(\{x\},T)\subseteq \bigcup T \) using Top_3_L11
then have tot: \( \bigcup (T\text{ restricted to } \text{Closure}(\{x\},T))= \text{Closure}(\{x\},T) \) unfolding RestrictedTo_def
{
fix \( A \) \( B \)
assume AS: \( A\in (T\text{ restricted to } \text{Closure}(\{x\},T)) \), \( B\in (T\text{ restricted to } \text{Closure}(\{x\},T)) \), \( A\cap B=0 \)
then have \( B\subseteq \bigcup ((T\text{ restricted to } \text{Closure}(\{x\},T))) \), \( A\subseteq \bigcup ((T\text{ restricted to } \text{Closure}(\{x\},T))) \)
with tot have \( B\subseteq \text{Closure}(\{x\},T) \), \( A\subseteq \text{Closure}(\{x\},T) \)
from AS(1,2) obtain \( UA \) \( UB \) where UAUB: \( UA\in T \), \( UB\in T \), \( A=UA\cap \text{Closure}(\{x\},T) \), \( B=UB\cap \text{Closure}(\{x\},T) \) unfolding RestrictedTo_def
then have \( \text{Closure}(\{x\},T)-A= \text{Closure}(\{x\},T)-(UA\cap \text{Closure}(\{x\},T)) \), \( \text{Closure}(\{x\},T)-B= \text{Closure}(\{x\},T)-(UB\cap \text{Closure}(\{x\},T)) \)
then have \( \text{Closure}(\{x\},T)-A= \text{Closure}(\{x\},T)-(UA) \), \( \text{Closure}(\{x\},T)-B= \text{Closure}(\{x\},T)-(UB) \)
with sub have \( \text{Closure}(\{x\},T)-A= \text{Closure}(\{x\},T)\cap (\bigcup T-UA) \), \( \text{Closure}(\{x\},T)-B= \text{Closure}(\{x\},T)\cap (\bigcup T-UB) \)
moreover
from UAUB have \( (\bigcup T-UA)\text{ is closed in }T \), \( (\bigcup T-UB)\text{ is closed in }T \) using Top_3_L9
moreover have \( \text{Closure}(\{x\},T)\text{ is closed in }T \) using cl_is_closed, assms
ultimately have \( ( \text{Closure}(\{x\},T)-A)\text{ is closed in }T \), \( ( \text{Closure}(\{x\},T)-B)\text{ is closed in }T \) using Top_3_L5(1)
moreover {
}
ultimately have \( \text{Closure}(\{x\},T)\subseteq ( \text{Closure}(\{x\},T)-A) \vee \text{Closure}(\{x\},T)\subseteq ( \text{Closure}(\{x\},T)-B) \) using Top_3_L13
have \( x\in \text{Closure}(\{x\},T) \) using cl_contains_set, assms
moreover
from AS(3) have \( x\notin A\vee x\notin B \)
ultimately have \( x\in ( \text{Closure}(\{x\},T)-A)\vee x\in ( \text{Closure}(\{x\},T)-B) \)
then have \( A\cap \text{Closure}(\{x\},T)=0 \vee B\cap \text{Closure}(\{x\},T)=0 \)
with \( B\subseteq \text{Closure}(\{x\},T) \), \( A\subseteq \text{Closure}(\{x\},T) \) have \( A=0\vee B=0 \) using cl_contains_set, assms
then show \( thesis \) unfolding IsHConnected_def
qed
A consequence is that every totally-disconnected space is \(T_1\).
lemma (in topology0) tot_dis_imp_T1:
assumes \( T\{is totally-disconnected\} \)
shows \( T\text{ is }T_1 \)proof{
}
fix \( x \) \( y \)
assume \( y\in \bigcup T \), \( x\in \bigcup T \), \( y\neq x \)
then have \( (T\text{ restricted to } \text{Closure}(\{x\},T))\text{ is hyperconnected } \) using cl_point_imp_HConn
then have \( (T\text{ restricted to } \text{Closure}(\{x\},T))\text{ is connected } \) using HConn_imp_Conn
moreover
from \( x\in \bigcup T \) have \( \text{Closure}(\{x\},T)\subseteq \bigcup T \) using Top_3_L11(1)
moreover note assms
ultimately have \( \text{Closure}(\{x\},T)\text{ is in the spectrum of }IsConnected \) unfolding IsTotDis_def, antiProperty_def
then have \( \text{Closure}(\{x\},T)\preceq 1 \) using conn_spectrum
moreover
from \( x\in \bigcup T \) have \( x\in \text{Closure}(\{x\},T) \) using cl_contains_set
moreover from lepoll_1_is_sing have \( \text{Closure}(\{x\},T)\preceq 1 \Longrightarrow x\in \text{Closure}(\{x\},T) \Longrightarrow \text{Closure}(\{x\},T) =\{x\} \)
ultimately have \( \text{Closure}(\{x\},T)=\{x\} \)
with \( x\in \bigcup T \) have \( \text{ x}{is closed in} } \) using Top_3_L8
then have \( \bigcup T-\{x\}\in T \) unfolding IsClosed_def
moreover
from \( y\in \bigcup T \), \( y\neq x \) have \( y\in \bigcup T-\{x\}\wedge x\notin \bigcup T-\{x\} \)
ultimately have \( \exists U\in T.\ y\in U\wedge x\notin U \)
then show \( thesis \) unfolding isT1_def
qed
In the literature, there exists a class of spaces called sober spaces; where the only non-empty closed hyperconnected subspaces are the closures of points and closures of different singletons are different.
definition
\( T\{is sober\} \equiv \forall A\in Pow(\bigcup T)-\{0\}.\ (A\text{ is closed in }T \wedge ((T\text{ restricted to }A)\text{ is hyperconnected })) \longrightarrow (\exists x\in \bigcup T.\ A= \text{Closure}(\{x\},T) \wedge (\forall y\in \bigcup T.\ A= \text{Closure}(\{y\},T) \longrightarrow y=x) ) \)
Being sober is weaker than being anti-hyperconnected.
theorem (in topology0) anti_HConn_imp_sober:
assumes \( T\{is anti-\}IsHConnected \)
shows \( T\{is sober\} \)proof{
}
fix \( A \)
assume \( A\in Pow(\bigcup T)-\{0\} \), \( A\text{ is closed in }T \), \( (T\text{ restricted to }A)\text{ is hyperconnected } \)
with assms have \( A\text{ is in the spectrum of }IsHConnected \) unfolding antiProperty_def
then have \( A\preceq 1 \) using HConn_spectrum
moreover
from this, \( A\in Pow(\bigcup T)-\{0\} \) have \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
ultimately have \( A=\{x\} \) using lepoll_1_is_sing
with \( A\text{ is closed in }T \) have \( \text{ x}{is closed in} } \)
moreover
from \( x\in A \), \( A\in Pow(\bigcup T)-\{0\} \) have \( \{x\}\in Pow(\bigcup T) \)
ultimately have \( \text{Closure}(\{x\},T)=\{x\} \) unfolding Closure_def, ClosedCovers_def
with \( A=\{x\} \) have \( A= \text{Closure}(\{x\},T) \)
moreover {
}
fix \( y \)
assume \( y\in \bigcup T \), \( A= \text{Closure}(\{y\},T) \)
then have \( \{y\}\subseteq \text{Closure}(\{y\},T) \) using cl_contains_set
with \( A= \text{Closure}(\{y\},T) \) have \( y\in A \)
with \( A=\{x\} \) have \( y=x \)
then have \( \forall y\in \bigcup T.\ A= \text{Closure}(\{y\},T) \longrightarrow y=x \)
moreover note \( \{x\}\in Pow(\bigcup T) \)
ultimately have \( \exists x\in \bigcup T.\ A= \text{Closure}(\{x\},T)\wedge (\forall y\in \bigcup T.\ A= \text{Closure}(\{y\},T) \longrightarrow y=x) \)
then show \( thesis \) using IsSober_def
qed
Every sober space is \(T_0\).
lemma (in topology0) sober_imp_T0:
assumes \( T\{is sober\} \)
shows \( T\text{ is }T_0 \)proof{
}
fix \( x \) \( y \)
assume AS: \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \), \( \forall U\in T.\ x\in U \longleftrightarrow y\in U \)
from \( x\in \bigcup T \) have clx: \( \text{Closure}(\{x\},T) \text{ is closed in }T \) using cl_is_closed
with \( x\in \bigcup T \) have \( (\bigcup T- \text{Closure}(\{x\},T))\in T \) using Top_3_L11(1) unfolding IsClosed_def
moreover
from \( x\in \bigcup T \) have \( x\in \text{Closure}(\{x\},T) \) using cl_contains_set
moreover note AS(1,4)
ultimately have \( y\notin (\bigcup T- \text{Closure}(\{x\},T)) \)
with AS(2) have \( y\in \text{Closure}(\{x\},T) \)
with clx have ineq1: \( \text{Closure}(\{y\},T)\subseteq \text{Closure}(\{x\},T) \) using Top_3_L13
from \( y\in \bigcup T \) have cly: \( \text{Closure}(\{y\},T) \text{ is closed in }T \) using cl_is_closed
with \( y\in \bigcup T \) have \( (\bigcup T- \text{Closure}(\{y\},T))\in T \) using Top_3_L11(1) unfolding IsClosed_def
moreover
from \( y\in \bigcup T \) have \( y\in \text{Closure}(\{y\},T) \) using cl_contains_set
moreover note AS(2,4)
ultimately have \( x\notin (\bigcup T- \text{Closure}(\{y\},T)) \)
with AS(1) have \( x\in \text{Closure}(\{y\},T) \)
with cly have \( \text{Closure}(\{x\},T)\subseteq \text{Closure}(\{y\},T) \) using Top_3_L13
with ineq1 have eq: \( \text{Closure}(\{x\},T)= \text{Closure}(\{y\},T) \)
from \( x\in \bigcup T \), \( x\in \text{Closure}(\{x\},T) \) have \( \text{Closure}(\{x\},T)\in Pow(\bigcup T)-\{0\} \) using Top_3_L11(1)
moreover
note assms, clx, \( x\in \bigcup T \)
ultimately have \( \exists t\in \bigcup T.\ ( \text{Closure}(\{x\},T) = \text{Closure}(\{t\}, T) \wedge (\forall y\in \bigcup T.\ \text{Closure}(\{x\},T) = \text{Closure}(\{y\}, T) \longrightarrow y = t)) \) unfolding IsSober_def using cl_point_imp_HConn
then obtain \( t \) where t_def: \( t\in \bigcup T \), \( \text{Closure}(\{x\},T) = \text{Closure}(\{t\}, T) \), \( \forall y\in \bigcup T.\ \text{Closure}(\{x\},T) = \text{Closure}(\{y\}, T) \longrightarrow y = t \)
with eq, \( y\in \bigcup T \) have \( y=t \)
moreover
from t_def, \( x\in \bigcup T \) have \( x=t \)
ultimately have \( y=x \)
with \( x\neq y \) have \( False \)
then have \( \forall x y.\ x\in \bigcup T\wedge y\in \bigcup T\wedge x\neq y \longrightarrow (\exists U\in T.\ (x\in U\wedge y\notin U)\vee (y\in U\wedge x\notin U)) \)
then show \( thesis \) using isT0_def
qed
Every \(T_2\) space is anti-hyperconnected.
theorem (in topology0) T2_imp_anti_HConn:
assumes \( T\text{ is }T_2 \)
shows \( T\{is anti-\}IsHConnected \)proof{
}
}
fix \( TT \)
assume \( TT\text{ is a topology } \), \( TT\text{ is hyperconnected } \), \( TT\text{ is }T_2 \)
{
assume \( \bigcup TT=0 \)
then have \( \bigcup TT\preceq 1 \) using empty_lepollI
then have \( (\bigcup TT)\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
moreover {
}
}
ultimately have \( (\bigcup TT)\text{ is in the spectrum of }IsHConnected \)
assume \( \bigcup TT\neq 0 \)
then obtain \( x \) where \( x\in \bigcup TT \)
{
fix \( y \)
assume \( y\in \bigcup TT \), \( x\neq y \)
with \( TT\text{ is }T_2 \), \( x\in \bigcup TT \) obtain \( U \) \( V \) where \( U\in TT \), \( V\in TT \), \( x\in U \), \( y\in V \), \( U\cap V=0 \) unfolding isT2_def
with \( TT\text{ is hyperconnected } \) have \( False \) using IsHConnected_def
with \( x\in \bigcup TT \) have \( \bigcup TT=\{x\} \)
then have \( \bigcup TT\approx 1 \) using singleton_eqpoll_1
then have \( \bigcup TT\preceq 1 \) using eqpoll_imp_lepoll
then have \( (\bigcup TT)\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
then have \( \forall T.\ ((T\text{ is a topology }\wedge (T\text{ is hyperconnected })\wedge (T\text{ is }T_2))\longrightarrow ((\bigcup T)\text{ is in the spectrum of }IsHConnected)) \)
moreover
qed
note here_T2
moreover from Q_P_imp_Spec have \( \forall T.\ T\text{ is a topology } \wedge T\text{ is hyperconnected } \wedge T\text{ is }T_2 \longrightarrow (\bigcup T) \text{ is in the spectrum of }IsHConnected \Longrightarrow isT2\text{ is hereditary } \Longrightarrow \forall T.\ T\text{ is a topology } \longrightarrow T\text{ is }T_2 \longrightarrow ANTI(IsHConnected,T) \)
ultimately have \( \forall T.\ T\text{ is a topology } \longrightarrow ((T\text{ is }T_2)\longrightarrow (T\{is anti-\}IsHConnected)) \)
then show \( thesis \) using assms, topSpaceAssum
Every anti-hyperconnected space is \(T_1\).
theorem anti_HConn_imp_T1:
assumes \( T\{is anti-\}IsHConnected \)
shows \( T\text{ is }T_1 \)proof{
}
}
}
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
{
assume AS: \( \forall U\in T.\ x\notin U\vee y\in U \)
from \( x\in \bigcup T \), \( y\in \bigcup T \) have \( \{x,y\}\in Pow(\bigcup T) \)
then have sub: \( (T\{restricted to}\{x,y\})\subseteq Pow(\{x,y\}\} \) using RestrictedTo_def
{
fix \( U \) \( V \)
assume H: \( U\in T\{restricted to}\{x,y\\} \), \( V\in (T\{restricted to}\{x,y\}\} \), \( U\cap V=0 \)
with AS have \( x\in U\longrightarrow y\in U \), \( x\in V\longrightarrow y\in V \) unfolding RestrictedTo_def
with H(1,2), sub have \( x\in U\longrightarrow U=\{x,y\} \), \( x\in V\longrightarrow V=\{x,y\} \)
with H, sub have \( x\in U\longrightarrow (U=\{x,y\}\wedge V=0) \), \( x\in V\longrightarrow (V=\{x,y\}\wedge U=0) \)
then have \( (x\in U\vee x\in V)\longrightarrow (U=0\vee V=0) \)
moreover
from sub, H have \( (x\notin U\wedge x\notin V)\longrightarrow (U=0\vee V=0) \)
ultimately have \( U=0\vee V=0 \)
then have \( (T\{restricted to}\{x,y\})\text{ is hyperconnected \} \) unfolding IsHConnected_def
with assms, \( \{x,y\}\in Pow(\bigcup T) \) have \( \{x,y}\text{ is in the spectrum of }IsHConnecte\} \) unfolding antiProperty_def
then have \( \{x,y\}\preceq 1 \) using HConn_spectrum
moreover
have \( x\in \{x,y\} \)
moreover from lepoll_1_is_sing have \( \{x,y\}\preceq 1 \Longrightarrow x\in \{x,y\} \Longrightarrow \{x,y\} = \{x\} \)
ultimately have \( \{x,y\}=\{x\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
then have \( y=x \)
with \( x\neq y \) have \( False \)
then have \( \exists U\in T.\ x\in U\wedge y\notin U \)
then show \( thesis \) using isT1_def
qed
There is at least one topological space that is \(T_1\), but not anti-hyperconnected. This space is the cofinite topology on the natural numbers.
lemma Cofinite_not_anti_HConn:
shows \( \neg ((CoFinite nat)\{is anti-\}IsHConnected) \) and \( (CoFinite nat)\text{ is }T_1 \)proof{
}
assume \( (CoFinite nat)\{is anti-\}IsHConnected \)
moreover
have \( \bigcup (CoFinite nat)=nat \) unfolding Cofinite_def using union_cocardinal
moreover have \( (CoFinite nat)\text{ restricted to }nat=(CoFinite nat) \) using subspace_cocardinal unfolding Cofinite_def
moreover have \( \neg (nat\prec nat) \)
then have \( (CoFinite nat)\text{ is hyperconnected } \) using Cofinite_nat_HConn
ultimately have \( nat\text{ is in the spectrum of }IsHConnected \) unfolding antiProperty_def
then have \( nat\preceq 1 \) using HConn_spectrum
moreover
have \( 1\in nat \)
then have \( 1\prec nat \) using n_lesspoll_nat
ultimately have \( nat\prec nat \) using lesspoll_trans1
then have \( False \)
then show \( \neg ((CoFinite nat)\{is anti-\}IsHConnected) \)
next
show \( (CoFinite nat)\text{ is }T_1 \) using cocardinal_is_T1, InfCard_nat unfolding Cofinite_def
qed
The join-topology build from the cofinite topology on the natural numbers, and the excluded set topology on the natural numbers excluding \( \{0,1\} \); is just the union of both.
lemma join_top_cofinite_excluded_set:
shows \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\})=(CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \)proof have Pa: \( (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \{is a subbase for}\{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\\} \) using Top_subbase(2)
have coftop: \( (CoFinite nat)\text{ is a topology } \) unfolding Cofinite_def using CoCar_is_topology, InfCard_nat
moreover
have \( \text{ExcludedSet}(nat,\{0,1\})\text{ is a topology } \) using excludedset_is_topology
moreover have exuni: \( \bigcup \text{ExcludedSet}(nat,\{0,1\})=nat \) using union_excludedset
moreover have cofuni: \( \bigcup (CoFinite nat)=nat \) using union_cocardinal unfolding Cofinite_def
ultimately have \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\}) = (\text{The } T.\ (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \text{ is a subbase for } T) \) using joinT_def
moreover
from same_subbase_same_top have \( \bigwedge T.\ (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \{is a subbase for}\{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \Longrightarrow \)
\( (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \text{ is a subbase for }T \Longrightarrow \)
\( \{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} = \} \)
then have \( \bigwedge T.\ (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \text{ is a subbase for }T \Longrightarrow \)
\( T=\{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \) using sym, Pa
with Pa have \( (\text{The } T.\ (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \text{ is a subbase for } T) = \{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \) by (rule the_equality )
ultimately have equal: \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\}) =\{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \)
have \( \bigcup (CoFinite nat)\in CoFinite nat \) using CoCar_is_topology, InfCard_nat unfolding Cofinite_def, IsATopology_def
with cofuni have n: \( nat\in CoFinite nat \)
{
fix \( U \)
assume \( U\in \{\bigcup A.\ A\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \)
then obtain \( AU \) where \( U=\bigcup AU \) and base: \( AU\in Pow(\{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\}) \)
have \( (CoFinite nat)\subseteq Pow(\bigcup (CoFinite nat)) \)
moreover
have \( \text{ExcludedSet}(nat,\{0,1\})\subseteq Pow(\bigcup \text{ExcludedSet}(nat,\{0,1\})) \)
moreover note cofuni, exuni
ultimately have sub: \( (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})\subseteq Pow(nat) \)
from base have \( \forall S\in AU.\ S\in \{\bigcap B.\ B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\} \)
then have \( \forall S\in AU.\ \exists B\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})).\ S=\bigcap B \)
then have eq: \( \forall S\in AU.\ \exists B\in Pow((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})).\ S=\bigcap B \) unfolding FinPow_def
{
fix \( S \)
assume \( S\in AU \)
with eq obtain \( B \) where \( B\in Pow((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})) \), \( S=\bigcap B \)
with sub have \( B\in Pow(Pow(nat)) \)
{
fix \( x \)
assume \( x\in \bigcap B \)
then have \( \forall N\in B.\ x\in N \), \( B\neq 0 \)
with \( B\in Pow(Pow(nat)) \) have \( x\in nat \)
with \( S=\bigcap B \) have \( S\in Pow(nat) \)
then have \( \forall S\in AU.\ S\in Pow(nat) \)
with \( U=\bigcup AU \) have \( U\in Pow(nat) \)
{
assume \( 0\in U\vee 1\in U \)
with \( U=\bigcup AU \) obtain \( S \) where \( S\in AU \), \( 0\in S\vee 1\in S \)
with base obtain \( BS \) where \( S=\bigcap BS \) and bsbase: \( BS\in \text{FinPow}((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})) \)
with \( 0\in S\vee 1\in S \) have \( \forall M\in BS.\ 0\in M\vee 1\in M \)
then have \( \forall M\in BS.\ M\notin \text{ExcludedSet}(nat,\{0,1\})-\{nat\} \) unfolding ExcludedPoint_def, ExcludedSet_def
moreover
note bsbase, n
ultimately have \( BS\in \text{FinPow}(CoFinite nat) \) unfolding FinPow_def
moreover
from \( 0\in S\vee 1\in S \) have \( S\neq 0 \)
with \( S=\bigcap BS \) have \( BS\neq 0 \)
moreover note coftop
moreover from topology0.fin_inter_open_open have \( topology0(CoFinite nat) \Longrightarrow BS\neq 0 \Longrightarrow BS\in \text{FinPow}(CoFinite nat) \Longrightarrow \bigcap BS\in CoFinite nat \)
ultimately have \( \bigcap BS\in CoFinite nat \) using topology0_CoCardinal, InfCard_nat unfolding Cofinite_def
with \( S=\bigcap BS \) have \( S\in CoFinite nat \)
with \( 0\in S\vee 1\in S \) have \( nat-S\prec nat \) unfolding Cofinite_def, CoCardinal_def
moreover
from \( U=\bigcup AU \), \( S\in AU \) have \( S\subseteq U \)
then have \( nat-U\subseteq nat-S \)
then have \( nat-U\preceq nat-S \) using subset_imp_lepoll
ultimately have \( nat-U\prec nat \) using lesspoll_trans1
with \( U\in Pow(nat) \) have \( U\in CoFinite nat \) unfolding Cofinite_def, CoCardinal_def
with \( U\in Pow(nat) \) have \( U\in (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \)
with \( U\in Pow(nat) \) have \( U\in (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \) unfolding ExcludedSet_def
then have \( (\{\bigcup A .\ A \in Pow(\{\bigcap B .\ B \in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}))\})\}) \subseteq (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \)
moreover {
}
qed
fix \( U \)
assume \( U\in (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \)
then have \( \{U\}\in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\})) \) unfolding FinPow_def
then have \( \{U\}\in Pow(\{\bigcap B .\ B \in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}))\}) \)
moreover
have \( U=\bigcup \{U\} \)
ultimately have \( U\in \{\bigcup A .\ A \in Pow(\{\bigcap B .\ B \in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \)
then have \( (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})\subseteq \{\bigcup A .\ A \in Pow(\{\bigcap B .\ B \in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \)
ultimately have \( (CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})=\{\bigcup A .\ A \in Pow(\{\bigcap B .\ B \in \text{FinPow}((CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}))\})\} \)
with equal show \( thesis \)
The previous topology in not \(T_2\), but is anti-hyperconnected.
theorem join_Cofinite_ExclPoint_not_T2:
shows \( \neg ((joinT \{CoFinite nat, \text{ExcludedSet}(nat,\{0,1\})\})\text{ is }T_2) \) and \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\})\{is anti-\} IsHConnected \)proof have \( (CoFinite nat) \subseteq (CoFinite nat) \cup \text{ExcludedSet}(nat,\{0,1\}) \)
have \( \bigcup ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))=(\bigcup (CoFinite nat))\cup (\bigcup \text{ExcludedSet}(nat,\{0,1\})) \)
moreover
{
have \( \ldots =nat \) unfolding Cofinite_def using union_cocardinal, union_excludedset
ultimately have tot: \( \bigcup ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))=nat \)
assume \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\}) \text{ is }T_2 \)
then have t2: \( ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\text{ is }T_2 \) using join_top_cofinite_excluded_set
with tot have \( \exists U\in ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})).\ \exists V\in ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\})).\ 0\in U\wedge 1\in V\wedge U\cap V=0 \) using isT2_def
then obtain \( U \) \( V \) where \( U \in (CoFinite nat) \vee (0 \notin U\wedge 1\notin U) \), \( V \in (CoFinite nat) \vee (0 \notin V\wedge 1\notin V) \), \( 0\in U \), \( 1\in V \), \( U\cap V=0 \) unfolding ExcludedSet_def
then have \( U\in (CoFinite nat) \), \( V\in (CoFinite nat) \)
with \( 0\in U \), \( 1\in V \) have \( U\cap V\neq 0 \) using Cofinite_nat_HConn, IsHConnected_def
with \( U\cap V=0 \) have \( False \)
then show \( \neg ((joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\})\text{ is }T_2) \)
{
fix \( A \)
assume AS: \( A\in Pow(\bigcup ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))) \), \( (((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\text{ restricted to }A)\text{ is hyperconnected } \)
with tot have \( A\in Pow(nat) \)
then have sub: \( A\cap nat=A \)
have \( ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\text{ restricted to }A=((CoFinite nat)\text{ restricted to }A)\cup (\text{ExcludedSet}(nat,\{0,1\})\text{ restricted to }A) \) unfolding RestrictedTo_def
also
{
from sub have \( \ldots =(CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\}) \) using subspace_excludedset, subspace_cocardinal unfolding Cofinite_def
finally have \( ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\text{ restricted to }A=(CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\}) \)
with AS(2) have eq: \( ((CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\}))\text{ is hyperconnected } \)
assume \( \{0,1\}\cap A=0 \)
then have \( (CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\})=Pow(A) \) using empty_excludedset unfolding Cofinite_def, CoCardinal_def
with eq have \( Pow(A)\text{ is hyperconnected } \)
then have \( Pow(A)\text{ is connected } \) using HConn_imp_Conn
moreover
have \( Pow(A)\{is anti-\}IsConnected \) using discrete_tot_dis unfolding IsTotDis_def
moreover have \( \bigcup (Pow(A))\in Pow(\bigcup (Pow(A))) \)
moreover have \( Pow(A)\text{ restricted to }\bigcup (Pow(A))=Pow(A) \) unfolding RestrictedTo_def
ultimately have \( (\bigcup (Pow(A)))\text{ is in the spectrum of }IsConnected \) unfolding antiProperty_def
then have \( A\text{ is in the spectrum of }IsConnected \)
then have \( A\preceq 1 \) using conn_spectrum
then have \( A\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
moreover {
}
}
ultimately have \( A\text{ is in the spectrum of }IsHConnected \)
assume AS: \( \{0,1\}\cap A\neq 0 \)
{
assume \( A=\{0\}\vee A=\{1\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
then have \( A\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
moreover {
}
}
ultimately have \( A\text{ is in the spectrum of }IsHConnected \)
assume AS2: \( \neg (A=\{0\}\vee A=\{1\}) \)
{
assume AS3: \( A\subseteq \{0,1\} \)
have I: \( \bigcup (CoFinite A)=A \) using union_cocardinal unfolding Cofinite_def
have II: \( (CoFinite A)\text{ is a topology } \) using CoCar_is_topology, InfCard_nat unfolding Cofinite_def
from AS, AS2, AS3 have A_def: \( A=\{0,1\} \)
then have \( \text{ExcludedSet}(A,\{0,1\})=\text{ExcludedSet}(A,A) \)
moreover
have \( \text{ExcludedSet}(A,A)=\{0,A\} \) unfolding ExcludedSet_def
ultimately have \( \text{ExcludedSet}(A,\{0,1\})=\{0,A\} \)
moreover
have \( 0\in (CoFinite A) \) using empty_open, CoCar_is_topology, InfCard_nat unfolding Cofinite_def
moreover from I, II have \( A\in (CoFinite A) \) unfolding Cofinite_def, IsATopology_def
ultimately have \( (CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\})=(CoFinite A) \)
with eq have \( (CoFinite A)\text{ is hyperconnected } \)
with A_def have hyp: \( (CoFinite \{0,1\})\text{ is hyperconnected } \)
have \( \{0\}\approx 1 \), \( \{1\}\approx 1 \) using singleton_eqpoll_1
moreover
have \( 1\prec nat \) using n_lesspoll_nat
ultimately have \( \{0\}\prec nat \), \( \{1\}\prec nat \) using eq_lesspoll_trans
moreover
have \( \{0,1\}-\{1\}=\{0\} \), \( \{0,1\}-\{0\}=\{1\} \)
ultimately have \( \{1\}\in (CoFinite \{0,1\}) \), \( \{0\}\in (CoFinite \{0,1\}) \), \( \{1\}\cap \{0\}=0 \) unfolding Cofinite_def, CoCardinal_def
with hyp have \( False \) unfolding IsHConnected_def
then obtain \( t \) where \( t\in A \), \( t\neq 0 \), \( t\neq 1 \)
then have \( \{t\}\in \text{ExcludedSet}(A,\{0,1\}) \) unfolding ExcludedSet_def
moreover {
}
ultimately have \( \{t\}\in ((CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\})) \), \( A-\{t\}\in ((CoFinite A)\cup \text{ExcludedSet}(A,\{0,1\})) \), \( \{t\}\cap (A-\{t\})=0 \)
have \( \{t\}\approx 1 \) using singleton_eqpoll_1
moreover
have \( 1\prec nat \) using n_lesspoll_nat
ultimately have \( \{t\}\prec nat \) using eq_lesspoll_trans
moreover
from this, \( t\in A \) have \( A-(A-\{t\})=\{t\} \)
ultimately have \( A-\{t\}\in (CoFinite A) \) unfolding Cofinite_def, CoCardinal_def
with eq have \( A-\{t\}=0 \) unfolding IsHConnected_def
with \( t\in A \) have \( A=\{t\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
then have \( A\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
then have \( ((CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}))\{is anti-\}IsHConnected \) unfolding antiProperty_def
then show \( (joinT \{CoFinite nat, \text{ExcludedSet}(nat,\{0,1\})\})\{is anti-\}IsHConnected \) using join_top_cofinite_excluded_set
qed
Let's show that anti-hyperconnected is in fact \(T_1\) and sober. The trick of the proof lies in the fact that if a subset is hyperconnected, its closure is so too (the closure of a point is then always hyperconnected because singletons are in the spectrum); since the closure is closed, we can apply the sober property on it.
theorem (in topology0) T1_sober_imp_anti_HConn:
assumes \( T\text{ is }T_1 \) and \( T\{is sober\} \)
shows \( T\{is anti-\}IsHConnected \)proof{
}
}
fix \( A \)
assume AS: \( A\in Pow(\bigcup T) \), \( (T\text{ restricted to }A)\text{ is hyperconnected } \)
{
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
then have \( A\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
moreover {
}
}
ultimately have \( A\text{ is in the spectrum of }IsHConnected \)
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
{
assume \( \neg ((T\text{ restricted to } \text{Closure}(A,T))\text{ is hyperconnected }) \)
then obtain \( U \) \( V \) where UV_def: \( U\in (T\text{ restricted to } \text{Closure}(A,T)) \), \( V\in (T\text{ restricted to } \text{Closure}(A,T)) \), \( U\cap V=0 \), \( U\neq 0 \), \( V\neq 0 \) using IsHConnected_def
then obtain \( UCA \) \( VCA \) where \( UCA\in T \), \( VCA\in T \), \( U=UCA\cap \text{Closure}(A,T) \), \( V=VCA\cap \text{Closure}(A,T) \) unfolding RestrictedTo_def
from \( A\in Pow(\bigcup T) \) have \( A\subseteq \text{Closure}(A,T) \) using cl_contains_set
then have \( UCA\cap A\subseteq UCA\cap \text{Closure}(A,T) \), \( VCA\cap A\subseteq VCA\cap \text{Closure}(A,T) \)
with \( U=UCA\cap \text{Closure}(A,T) \), \( V=VCA\cap \text{Closure}(A,T) \), \( U\cap V=0 \) have \( (UCA\cap A)\cap (VCA\cap A)=0 \)
moreover
from \( UCA\in T \), \( VCA\in T \) have \( UCA\cap A\in (T\text{ restricted to }A) \), \( VCA\cap A\in (T\text{ restricted to }A) \) unfolding RestrictedTo_def
moreover note AS(2)
ultimately have \( UCA\cap A=0\vee VCA\cap A=0 \) using IsHConnected_def
with \( A\subseteq \text{Closure}(A,T) \) have \( A\subseteq \text{Closure}(A,T)-UCA\vee A\subseteq \text{Closure}(A,T)-VCA \)
moreover {
}
ultimately have \( \text{Closure}(A,T)\subseteq \text{Closure}(A,T)-UCA\vee \text{Closure}(A,T)\subseteq \text{Closure}(A,T)-VCA \) using Top_3_L13
have \( \text{Closure}(A,T)-UCA= \text{Closure}(A,T)\cap (\bigcup T-UCA) \), \( \text{Closure}(A,T)-VCA= \text{Closure}(A,T)\cap (\bigcup T-VCA) \) using Top_3_L11(1), AS(1)
moreover
from this, \( UCA\in T \), \( VCA\in T \) have \( (\bigcup T-UCA)\text{ is closed in }T \), \( (\bigcup T-VCA)\text{ is closed in }T \), \( \text{Closure}(A,T)\text{ is closed in }T \) using Top_3_L9, cl_is_closed, AS(1)
ultimately have \( ( \text{Closure}(A,T)-UCA)\text{ is closed in }T \), \( ( \text{Closure}(A,T)-VCA)\text{ is closed in }T \) using Top_3_L5(1)
then have \( UCA\cap \text{Closure}(A,T)=0\vee VCA\cap \text{Closure}(A,T)=0 \)
with \( U=UCA\cap \text{Closure}(A,T) \), \( V=VCA\cap \text{Closure}(A,T) \) have \( U=0\vee V=0 \)
with \( U\neq 0 \), \( V\neq 0 \) have \( False \)
then have \( (T\text{ restricted to } \text{Closure}(A,T))\text{ is hyperconnected } \)
moreover
have \( \text{Closure}(A,T)\text{ is closed in }T \) using cl_is_closed, AS(1)
moreover from \( x\in A \) have \( \text{Closure}(A,T)\neq 0 \) using cl_contains_set, AS(1)
moreover from AS(1) have \( \text{Closure}(A,T)\subseteq \bigcup T \) using Top_3_L11(1)
ultimately have \( \text{Closure}(A,T)\in Pow(\bigcup T)-\{0\} \), \( (T \text{ restricted to } \text{Closure}(A, T))\text{ is hyperconnected } \), \( \text{Closure}(A, T) \text{ is closed in } T \)
moreover
note assms(2)
ultimately have \( \exists x\in \bigcup T.\ ( \text{Closure}(A,T)= \text{Closure}(\{x\},T)\wedge (\forall y\in \bigcup T.\ \text{Closure}(A,T) = \text{Closure}(\{y\}, T) \longrightarrow y = x)) \) unfolding IsSober_def
then obtain \( y \) where \( y\in \bigcup T \), \( \text{Closure}(A,T)= \text{Closure}(\{y\},T) \)
moreover {
}
fix \( z \)
assume \( z\in (\bigcup T)-\{y\} \)
with assms(1), \( y\in \bigcup T \) obtain \( U \) where \( U\in T \), \( z\in U \), \( y\notin U \) using isT1_def
then have \( U\in T \), \( z\in U \), \( U\subseteq (\bigcup T)-\{y\} \)
then have \( \exists U\in T.\ z\in U \wedge U\subseteq (\bigcup T)-\{y\} \)
then have \( \forall z\in (\bigcup T)-\{y\}.\ \exists U\in T.\ z\in U \wedge U\subseteq (\bigcup T)-\{y\} \)
then have \( \bigcup T-\{y\}\in T \) using open_neigh_open
with \( y\in \bigcup T \) have \( \{y\} \text{ is closed in }T \) using IsClosed_def
with \( y\in \bigcup T \) have \( \text{Closure}(\{y\},T)=\{y\} \) using Top_3_L8
with \( \text{Closure}(A,T)= \text{Closure}(\{y\},T) \) have \( \text{Closure}(A,T)=\{y\} \)
moreover have \( A\subseteq \bigcup T \Longrightarrow A\subseteq \text{Closure}(A,T) \) using cl_contains_set
moreover note AS(1)
ultimately have \( A\subseteq \{y\} \)
with \( A\neq 0 \) have \( A=\{y\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
then have \( A\text{ is in the spectrum of }IsHConnected \) using HConn_spectrum
then show \( thesis \) using antiProperty_def
qed
A space is anti-hyperconnected if and only if it is both \(T_1\) and sober.
theorem (in topology0) anti_HConn_iff_T1_sober:
shows \( (T\{is anti-\}IsHConnected) \longleftrightarrow (T\{is sober\}\wedge T\text{ is }T_1) \) using T1_sober_imp_anti_HConn, anti_HConn_imp_T1, anti_HConn_imp_soberA space is ultraconnected iff every two non-empty closed sets meet.
definition
\( T\text{ is ultraconnected }\equiv \forall A B.\ A\text{ is closed in }T\wedge B\text{ is closed in }T\wedge A\cap B=0 \longrightarrow A=0\vee B=0 \)
Every ultraconnected space is trivially normal.
lemma (in topology0) UConn_imp_normal:
assumes \( T\text{ is ultraconnected } \)
shows \( T\text{ is normal } \)proof{
}
fix \( A \) \( B \)
assume AS: \( A\text{ is closed in }T \), \( B\text{ is closed in }T \), \( A\cap B=0 \)
with assms have \( A=0\vee B=0 \) using IsUConnected_def
with AS(1,2) have \( (A\subseteq 0\wedge B\subseteq \bigcup T)\vee (A\subseteq \bigcup T\wedge B\subseteq 0) \) unfolding IsClosed_def
moreover
have \( 0\in T \) using empty_open, topSpaceAssum
moreover have \( \bigcup T\in T \) using topSpaceAssum unfolding IsATopology_def
ultimately have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U\wedge B\subseteq V\wedge U\cap V=0 \)
then show \( thesis \) unfolding IsNormal_def
qed
Every ultraconnected space is connected.
lemma UConn_imp_Conn:
assumes \( T\text{ is ultraconnected } \)
shows \( T\text{ is connected } \)proof{
}
fix \( U \) \( V \)
assume \( U\in T \), \( U\text{ is closed in }T \)
then have \( \bigcup T-(\bigcup T-U)=U \)
with \( U\in T \) have \( (\bigcup T-U)\text{ is closed in }T \) unfolding IsClosed_def
with \( U\text{ is closed in }T \), assms have \( U=0\vee \bigcup T-U=0 \) unfolding IsUConnected_def
with \( U\in T \) have \( U=0\vee U=\bigcup T \)
then show \( thesis \) unfolding IsConnected_def
qed
A set is in the ultraconnectedness spectrum iff it has cardinality at most one.
lemma UConn_spectrum:
shows \( (A\text{ is in the spectrum of }IsUConnected) \longleftrightarrow A\preceq 1 \)proof assume A_spec: \( (A\text{ is in the spectrum of }IsUConnected) \)
{
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
moreover {
}
}
ultimately show \( A\preceq 1 \)
assume \( A\neq 0 \)
from A_spec have \( \forall T.\ (T\text{ is a topology }\wedge \bigcup T\approx A) \longrightarrow (T\text{ is ultraconnected }) \) unfolding Spec_def
moreover
have \( Pow(A)\text{ is a topology } \) using Pow_is_top
moreover have \( \bigcup Pow(A)=A \)
then have \( \bigcup Pow(A)\approx A \)
ultimately have ult: \( Pow(A)\text{ is ultraconnected } \)
from \( A\neq 0 \) obtain \( b \) where \( b\in A \)
then have \( \{b}\text{ is closed in }Pow(A\} \) unfolding IsClosed_def
{
fix \( c \)
assume \( c\in A \), \( c\neq b \)
then have \( \{c}\text{ is closed in }Pow(A\} \), \( \{c\}\cap \{b\}=0 \) unfolding IsClosed_def
with ult, \( \{b}\text{ is closed in }Pow(A\} \) have \( False \) using IsUConnected_def
with \( b\in A \) have \( A=\{b\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( \bigcup T=0 \)
with \( T\text{ is a topology } \) have \( T=\{0\} \) using empty_open
then have \( T\text{ is ultraconnected } \) unfolding IsUConnected_def, IsClosed_def
moreover {
}
ultimately have \( T\text{ is ultraconnected } \)
assume \( \bigcup T\neq 0 \)
moreover
from \( A\preceq 1 \), \( \bigcup T\approx A \) have \( \bigcup T\preceq 1 \) using eq_lepoll_trans
ultimately obtain \( E \) where eq: \( \bigcup T=\{E\} \) using lepoll_1_is_sing
moreover
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( T\subseteq Pow(\{E\}) \)
then have \( T\subseteq \{0,\{E\}\} \)
with \( T\text{ is a topology } \) have TT: \( \{0\}\subseteq T \), \( T\subseteq \{0,\{E\}\} \) using empty_open
from eq have \( E\in \bigcup T \)
then obtain \( U \) where U: \( E\in U \), \( U\in T \)
from TT(2), U have \( U=\{E\} \)
with U(2), TT have \( T=\{0,\{E\}\} \)
then have \( T\text{ is ultraconnected } \) unfolding IsUConnected_def, IsClosed_def
then show \( A\text{ is in the spectrum of }IsUConnected \) unfolding Spec_def
qed
This time, anti-ultraconnected is an old property.
theorem (in topology0) anti_UConn:
shows \( (T\{is anti-\}IsUConnected) \longleftrightarrow T\text{ is }T_1 \)proof assume \( T\text{ is }T_1 \)
{
fix \( TT \)
{
assume \( TT\text{ is a topology } \), \( TT\text{ is }T_1 \), \( TT\text{ is ultraconnected } \)
{
assume \( \bigcup TT=0 \)
then have \( \bigcup TT\preceq 1 \) using empty_lepollI
then have \( ((\bigcup TT)\text{ is in the spectrum of }IsUConnected) \) using UConn_spectrum
moreover {
}
}
}
}
ultimately have \( (\bigcup TT)\text{ is in the spectrum of }IsUConnected \)
assume \( \bigcup TT\neq 0 \)
then obtain \( t \) where \( t\in \bigcup TT \)
{
fix \( x \)
assume p: \( x\in \bigcup TT \)
{
fix \( y \)
assume \( y\in (\bigcup TT)-\{x\} \)
with \( TT\text{ is }T_1 \), p obtain \( U \) where \( U\in TT \), \( y\in U \), \( x\notin U \) using isT1_def
then have \( U\in TT \), \( y\in U \), \( U\subseteq (\bigcup TT)-\{x\} \)
then have \( \exists U\in TT.\ y\in U \wedge U\subseteq (\bigcup TT)-\{x\} \)
then have \( \forall y\in (\bigcup TT)-\{x\}.\ \exists U\in TT.\ y\in U \wedge U\subseteq (\bigcup TT)-\{x\} \)
with \( TT\text{ is a topology } \) have \( \bigcup TT-\{x\}\in TT \) using open_neigh_open unfolding topology0_def
with p have \( \{x\} \text{ is closed in }TT \) using IsClosed_def
then have reg: \( \forall x\in \bigcup TT.\ \text{ x}{is closed in}T } \)
with \( t\in \bigcup TT \) have t_cl: \( \text{ t}{is closed in}T } \)
{
fix \( y \)
assume \( y\in \bigcup TT \)
with reg have \( \text{ y}{is closed in}T } \)
with \( TT\text{ is ultraconnected } \), t_cl have \( y=t \) unfolding IsUConnected_def
with \( t\in \bigcup TT \) have \( \bigcup TT=\{t\} \)
then have \( \bigcup TT\approx 1 \) using singleton_eqpoll_1
then have \( \bigcup TT\preceq 1 \) using eqpoll_imp_lepoll
then have \( (\bigcup TT)\text{ is in the spectrum of }IsUConnected \) using UConn_spectrum
then have \( (TT\text{ is a topology }\wedge TT\text{ is }T_1\wedge (TT\text{ is ultraconnected }))\longrightarrow ((\bigcup TT)\text{ is in the spectrum of }IsUConnected) \)
then have \( \forall TT.\ (TT\text{ is a topology }\wedge (TT\text{ is ultraconnected })\wedge TT\text{ is }T_1)\longrightarrow ((\bigcup TT)\text{ is in the spectrum of }IsUConnected) \)
moreover
note here_T1
ultimately have \( \forall T.\ T\text{ is a topology } \longrightarrow ((T\text{ is }T_1)\longrightarrow (T\{is anti-\}IsUConnected)) \) by (rule Q_P_imp_Spec )
with topSpaceAssum have \( (T\text{ is }T_1)\longrightarrow (T\{is anti-\}IsUConnected) \)
with \( T\text{ is }T_1 \) show \( T\{is anti-\}IsUConnected \)
next
assume ASS: \( T\{is anti-\}IsUConnected \)
{
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
then have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
{
assume AS: \( \forall U\in T.\ x\in U\longrightarrow y\in U \)
{
assume \( \{y}\text{ is closed in }(T\{restricted to}\{x,y\}\\} \)
moreover
from \( x\neq y \) have \( \{x,y\}-\{y\}=\{x\} \)
moreover note tot
ultimately have \( \{x\}\in (T\{restricted to}\{x,y\}\} \) unfolding IsClosed_def
then obtain \( U \) where \( U\in T \), \( \{x\}=\{x,y\}\cap U \) unfolding RestrictedTo_def
moreover
from \( x\neq y \) have \( y\notin \{x\} \), \( y\in \{x,y\} \)
with \( \{x\}=\{x,y\}\cap U \) have \( y\notin U \)
moreover have \( x\in \{x\} \)
with \( \{x\}=\{x,y\}\cap U \) have \( x\in U \)
ultimately have \( x\in U \), \( y\notin U \), \( U\in T \)
with AS have \( False \)
then have y_no_cl: \( \neg (\{y}\text{ is closed in }(T\{restricted to}\{x,y\})\\} \)
{
fix \( A \) \( B \)
assume cl: \( A\text{ is closed in }(T\{restricted to}\{x,y\}\} \), \( B\text{ is closed in }(T\{restricted to}\{x,y\}\} \), \( A\cap B=0 \)
with tot have \( A\subseteq \{x,y\} \), \( B\subseteq \{x,y\} \), \( A\cap B=0 \) unfolding IsClosed_def
then have \( x\in A\longrightarrow x\notin B \), \( y\in A\longrightarrow y\notin B \), \( A\subseteq \{x,y\} \), \( B\subseteq \{x,y\} \)
{
assume \( x\in A \)
with \( x\in A\longrightarrow x\notin B \), \( B\subseteq \{x,y\} \) have \( B\subseteq \{y\} \)
then have \( B=0\vee B=\{y\} \)
with y_no_cl, cl(2) have \( B=0 \)
moreover {
}
ultimately have \( A=0\vee B=0 \)
assume \( x\notin A \)
with \( A\subseteq \{x,y\} \) have \( A\subseteq \{y\} \)
then have \( A=0\vee A=\{y\} \)
with y_no_cl, cl(1) have \( A=0 \)
then have \( (T\{restricted to}\{x,y\})\text{ is ultraconnected \} \) unfolding IsUConnected_def
with ASS, \( x\in \bigcup T \), \( y\in \bigcup T \) have \( \{x,y}\text{ is in the spectrum of }IsUConnecte\} \) unfolding antiProperty_def
then have \( \{x,y\}\preceq 1 \) using UConn_spectrum
moreover
have \( x\in \{x,y\} \)
moreover from lepoll_1_is_sing have \( \{x,y\}\preceq 1 \Longrightarrow x\in \{x,y\} \Longrightarrow \{x,y\}=\{x\} \)
ultimately have \( \{x\}=\{x,y\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
then have \( y=x \)
with \( x\neq y \) have \( False \)
then have \( \exists U\in T.\ x\in U\wedge y\notin U \)
then show \( T\text{ is }T_1 \) unfolding isT1_def
qed
It is natural that separation axioms and connection axioms are anti-properties of each other; as the concepts of connectedness and separation are opposite.
To end this section, let's try to characterize anti-sober spaces.
lemma sober_spectrum:
shows \( (A\text{ is in the spectrum of }IsSober) \longleftrightarrow A\preceq 1 \)proof assume AS: \( A\text{ is in the spectrum of }IsSober \)
{
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
moreover {
}
}
}
ultimately show \( A\preceq 1 \)
assume \( A\neq 0 \)
note AS
moreover
have top: \( \{0,A}\text{ is a topology \} \) unfolding IsATopology_def
moreover have \( \bigcup \{0,A\}=A \)
then have \( \bigcup \{0,A\}\approx A \)
ultimately have \( \{0,A}\{is sober\\} \) using Spec_def
moreover
{
have \( \{0,A}\text{ is hyperconnected \} \) using Indiscrete_HConn
moreover have \( \{0,A}\text{ restricted to }A=\{0,A\\} \) unfolding RestrictedTo_def
moreover have \( A\{is closed in}\{0,A\\} \) unfolding IsClosed_def
moreover note \( A\neq 0 \)
ultimately have \( \exists x\in A.\ A= \text{Closure}(\{x\},\{0,A\})\wedge (\forall y\in \bigcup \{0, A\}.\ A = \text{Closure}(\{y\}, \{0, A\}) \longrightarrow y = x) \) unfolding IsSober_def
then obtain \( x \) where \( x\in A \), \( A= \text{Closure}(\{x\},\{0,A\}) \) and reg: \( \forall y\in A.\ A = \text{Closure}(\{y\}, \{0, A\}) \longrightarrow y = x \)
fix \( y \)
assume \( y\in A \)
with top have \( \text{Closure}(\{y\},\{0,A\})\{is closed in}\{0,A\\} \) using cl_is_closed, topology0_def
moreover
from \( y\in A \), top have \( y\in \text{Closure}(\{y\},\{0,A\}) \) using cl_contains_set, topology0_def
ultimately have \( A- \text{Closure}(\{y\},\{0,A\})\in \{0,A\} \), \( \text{Closure}(\{y\},\{0,A\})\cap A\neq 0 \) unfolding IsClosed_def
then have D: \( A- \text{Closure}(\{y\},\{0,A\})=A\vee A- \text{Closure}(\{y\},\{0,A\})=0 \)
from \( y\in A \), \( y\in \text{Closure}(\{y\},\{0,A\}) \) have y: \( y\in A \), \( y\notin A- \text{Closure}(\{y\},\{0,A\}) \)
{
assume \( A- \text{Closure}(\{y\},\{0,A\})=A \)
with y have \( False \)
with D have \( A- \text{Closure}(\{y\},\{0,A\})=0 \)
moreover
from \( y\in A \), top have \( \text{Closure}(\{y\},\{0,A\})\subseteq A \) using topology0_def, Top_3_L11(1)
then have \( A-(A- \text{Closure}(\{y\},\{0,A\}))= \text{Closure}(\{y\},\{0,A\}) \)
ultimately have \( A= \text{Closure}(\{y\},\{0,A\}) \)
with reg have \( \forall y\in A.\ x=y \)
with \( x\in A \) have \( A=\{x\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( \bigcup T=0 \)
then have \( T\{is sober\} \) unfolding IsSober_def
moreover {
}
}
ultimately have \( T\{is sober\} \)
assume \( \bigcup T\neq 0 \)
then obtain \( x \) where \( x\in \bigcup T \)
moreover
from \( \bigcup T\approx A \), \( A\preceq 1 \) have \( \bigcup T\preceq 1 \) using eq_lepoll_trans
ultimately have \( \bigcup T=\{x\} \) using lepoll_1_is_sing
moreover
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( T\subseteq Pow(\{x\}) \)
then have \( T\subseteq \{0,\{x\}\} \)
moreover
{
from \( T\text{ is a topology } \) have \( 0\in T \) using empty_open
moreover from \( T\text{ is a topology } \) have \( \bigcup T\in T \) unfolding IsATopology_def
with \( \bigcup T=\{x\} \) have \( \{x\}\in T \)
ultimately have T_def: \( T=\{0,\{x\}\} \)
then have dd: \( Pow(\bigcup T)-\{0\}=\{\{x\}\} \)
fix \( B \)
assume \( B\in Pow(\bigcup T)-\{0\} \)
with dd have B_def: \( B=\{x\} \)
from \( T\text{ is a topology } \) have \( (\bigcup T)\text{ is closed in }T \) using topology0_def, Top_3_L1
with \( \bigcup T=\{x\} \), \( T\text{ is a topology } \) have \( \text{Closure}(\{x\},T)=\{x\} \) using Top_3_L8 unfolding topology0_def
with B_def have \( B= \text{Closure}(\{x\},T) \)
moreover {
}
fix \( y \)
assume \( y\in \bigcup T \)
with \( \bigcup T=\{x\} \) have \( y=x \)
then have \( (\forall y\in \bigcup T.\ B = \text{Closure}(\{y\}, T) \longrightarrow y = x) \)
moreover note \( x\in \bigcup T \)
ultimately have \( (\exists x\in \bigcup T.\ B = \text{Closure}(\{x\}, T) \wedge (\forall y\in \bigcup T.\ B = \text{Closure}(\{y\}, T) \longrightarrow y = x)) \)
then have \( T\{is sober\} \) unfolding IsSober_def
then show \( A \text{ is in the spectrum of } IsSober \) unfolding Spec_def
qed
A space anti-sober is just an indiscrete space.
theorem (in topology0) anti_sober:
shows \( (T\{is anti-\}IsSober) \longleftrightarrow T=\{0,\bigcup T\} \)proof assume \( T=\{0,\bigcup T\} \)
{
fix \( A \)
assume \( A\in Pow(\bigcup T) \), \( (T\text{ restricted to }A)\{is sober\} \)
{
assume \( A=0 \)
then have \( A\preceq 1 \) using empty_lepollI
then have \( A\text{ is in the spectrum of }IsSober \) using sober_spectrum
moreover {
}
}
}
ultimately have \( A\text{ is in the spectrum of }IsSober \)
assume \( A\neq 0 \)
have \( \bigcup T\in \{0,\bigcup T\} \), \( 0\in \{0,\bigcup T\} \)
with \( T=\{0,\bigcup T\} \) have \( (\bigcup T)\in T \), \( 0\in T \)
with \( A\in Pow(\bigcup T) \) have \( \{0,A\}\subseteq (T\text{ restricted to }A) \) unfolding RestrictedTo_def
moreover
have \( \forall B\in \{0,\bigcup T\}.\ B=0\vee B=\bigcup T \)
with \( T=\{0,\bigcup T\} \) have \( \forall B\in T.\ B=0\vee B=\bigcup T \)
with \( A\in Pow(\bigcup T) \) have \( T\text{ restricted to }A\subseteq \{0,A\} \) unfolding RestrictedTo_def
ultimately have top_def: \( T\text{ restricted to }A=\{0,A\} \)
moreover
{
have \( A\{is closed in}\{0,A\\} \) unfolding IsClosed_def
moreover have \( \{0,A}\text{ is hyperconnected \} \) using Indiscrete_HConn
moreover have \( A\subseteq \bigcup T \Longrightarrow T\text{ restricted to }A = (T\text{ restricted to }A)\text{ restricted to }A \) using subspace_of_subspace
with \( A\in Pow(\bigcup T) \) have \( (T\text{ restricted to }A)\text{ restricted to }A=T\text{ restricted to }A \)
moreover note \( A\neq 0 \), \( A\in Pow(\bigcup T) \)
ultimately have \( A\in Pow(\bigcup (T\text{ restricted to }A))-\{0\} \), \( A\text{ is closed in }(T\text{ restricted to }A) \), \( ((T\text{ restricted to }A)\text{ restricted to }A)\text{ is hyperconnected } \)
with \( (T\text{ restricted to }A)\{is sober\} \) have \( \exists x\in \bigcup (T\text{ restricted to }A).\ A= \text{Closure}(\{x\},T\text{ restricted to }A)\wedge (\forall y\in \bigcup (T\text{ restricted to }A).\ A= \text{Closure}(\{y\},T\text{ restricted to }A) \longrightarrow y=x) \) unfolding IsSober_def
with top_def have \( \exists x\in A.\ A= \text{Closure}(\{x\},\{0,A\})\wedge (\forall y\in A.\ A= \text{Closure}(\{y\},\{0,A\}) \longrightarrow y=x) \)
then obtain \( x \) where \( x\in A \), \( A= \text{Closure}(\{x\},\{0,A\}) \) and reg: \( \forall y\in A.\ A= \text{Closure}(\{y\},\{0,A\}) \longrightarrow y=x \)
fix \( y \)
assume \( y\in A \)
from Ptopology_is_a_topology(1) have \( \{A}\text{ is a partition of }A \Longrightarrow (PTopology A \{A\})\text{ is a topology \} \)
with \( A\neq 0 \) have top: \( \{0,A}\text{ is a topology \} \) using indiscrete_ptopology, indiscrete_partition
with \( y\in A \) have \( \text{Closure}(\{y\},\{0,A\})\{is closed in}\{0,A\\} \) using cl_is_closed, topology0_def
moreover
from \( y\in A \), top have \( y\in \text{Closure}(\{y\},\{0,A\}) \) using cl_contains_set, topology0_def
ultimately have \( A- \text{Closure}(\{y\},\{0,A\})\in \{0,A\} \), \( \text{Closure}(\{y\},\{0,A\})\cap A\neq 0 \) unfolding IsClosed_def
then have D: \( A- \text{Closure}(\{y\},\{0,A\})=A\vee A- \text{Closure}(\{y\},\{0,A\})=0 \)
from \( y\in A \), \( y\in \text{Closure}(\{y\},\{0,A\}) \) have y: \( y\in A \), \( y\notin A- \text{Closure}(\{y\},\{0,A\}) \)
{
assume \( A- \text{Closure}(\{y\},\{0,A\})=A \)
with y have \( False \)
with D have \( A- \text{Closure}(\{y\},\{0,A\})=0 \)
moreover
from \( y\in A \), top have \( \text{Closure}(\{y\},\{0,A\})\subseteq A \) using topology0_def, Top_3_L11(1)
then have \( A-(A- \text{Closure}(\{y\},\{0,A\}))= \text{Closure}(\{y\},\{0,A\}) \)
ultimately have \( A= \text{Closure}(\{y\},\{0,A\}) \)
with reg, \( x\in A \) have \( A=\{x\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
then have \( A\text{ is in the spectrum of }IsSober \) using sober_spectrum
then show \( T\{is anti-\}IsSober \) using antiProperty_def
next
assume \( T\{is anti-\}IsSober \)
{
fix \( A \)
assume \( A\in T \), \( A\neq 0 \), \( A\neq \bigcup T \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in \bigcup T-A \), \( x\neq y \)
then have \( \{x\}=\{x,y\}\cap A \)
with \( A\in T \) have \( \{x\}\in T\{restricted to}\{x,y\\} \) unfolding RestrictedTo_def
{
assume \( \{y\}\in T\{restricted to}\{x,y\\} \)
from \( y\in \bigcup T-A \), \( x\in A \), \( A\in T \) have \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
with \( x\neq y \), \( \{y\}\in T\{restricted to}\{x,y\\} \), \( \{x\}\in T\{restricted to}\{x,y\\} \) have \( (T\{restricted to}\{x,y\})\{is T_2\\} \) unfolding isT2_def
then have \( (T\{restricted to}\{x,y\})\{is sober\\} \) using T2_imp_anti_HConn, Top_1_L4, topology0_def, anti_HConn_iff_T1_sober
moreover {
}
}
}
}
}
}
ultimately have \( (T\{restricted to}\{x,y\})\{is sober\\} \)
assume as: \( \{y\}\notin T\{restricted to}\{x,y\\} \)
from \( y\in \bigcup T-A \), \( x\in A \), \( A\in T \) have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
note as
moreover
{
from \( y\in \bigcup T-A \), \( x\in A \), \( A\in T \) have \( T\{restricted to}\{x,y\}\subseteq Pow(\{x,y\}\} \) unfolding RestrictedTo_def
then have \( T\{restricted to}\{x,y\}\subseteq \{0,\{x\},\{y\},\{x,y\}\\} \)
moreover note \( \{x\}\in T\{restricted to}\{x,y\\} \), empty_open, Top_1_L4
moreover from Top_1_L4 have \( \bigcup (T\{restricted to}\{x,y\})\in T\{restricted to}\{x,y\\\} \) unfolding IsATopology_def
with tot have \( \{x,y\}\in T\{restricted to}\{x,y\\} \)
ultimately have top_d_def: \( T\{restricted to}\{x,y\}=\{0,\{x\},\{x,y\}\\} \)
fix \( B \)
assume \( B\in Pow(\{x,y\})-\{0\} \), \( B\text{ is closed in }(T\{restricted to}\{x,y\}\} \)
with top_d_def have \( (\bigcup (T\{restricted to}\{x,y\}))-B\in \{0,\{x\},\{x,y\}\\} \) unfolding IsClosed_def
moreover
from \( B\in Pow(\{x,y\})-\{0\} \) have \( B\in \{\{x\},\{y\},\{x,y\}\} \)
moreover note tot
ultimately have \( \{x,y\}-B\in \{0,\{x\},\{x,y\}\} \)
from topology0.cl_contains_set have \( \{x\}\subseteq \bigcup (T\{restricted to}\{x,y\}) \Longrightarrow \{x\} \subseteq \text{Closure}(\{x\},T\{restricted to}\{x,y\}\\} \) using Top_1_L4 unfolding topology0_def
then have xin: \( x\in \text{Closure}(\{x\},T\{restricted to}\{x,y\}\} \) using tot
{
assume \( \{x}\text{ is closed in }(T\{restricted to}\{x,y\}\\} \)
then have \( \{x,y\}-\{x\}\in (T\{restricted to}\{x,y\}\} \) unfolding IsClosed_def using tot
moreover
from \( x\neq y \) have \( \{x,y\}-\{x\}=\{y\} \)
ultimately have \( \{y\}\in (T\{restricted to}\{x,y\}\} \)
with \( \{y\}\notin (T\{restricted to}\{x,y\}\} \) have \( False \)
then have \( \neg (\{x}\text{ is closed in }(T\{restricted to}\{x,y\})\\} \)
moreover
from tot have \( ( \text{Closure}(\{x\},T\{restricted to}\{x,y\}))\text{ is closed in }(T\{restricted to}\{x,y\}\\} \) using cl_is_closed, Top_1_L4, tot unfolding topology0_def
ultimately have \( \neg ( \text{Closure}(\{x\},T\{restricted to}\{x,y\})=\{x\}\} \)
moreover
note xin, tot
moreover from topology0.Top_3_L11(1) have \( \{x\} \subseteq \bigcup (T\{restricted to}\{x,y\}) \Longrightarrow \text{Closure}(\{x\},T\{restricted to}\{x,y\})\subseteq \bigcup (T\{restricted to}\{x,y\}\\\} \) using Top_1_L4 unfolding topology0_def
ultimately have cl_x: \( \text{Closure}(\{x\},T\{restricted to}\{x,y\})=\{x,y\\} \)
from \( x\neq y \) have \( \{y}\text{ is closed in }(T\{restricted to}\{x,y\}\\} \) unfolding IsClosed_def using tot, top_d_def
moreover
{
from topology0.Top_3_L8 have \( \bigwedge A.\ A\subseteq \bigcup (T\{restricted to}\{x,y\}) \Longrightarrow A\text{ is closed in }(T\{restricted to}\{x,y\}) \longleftrightarrow \text{Closure}(A,T\{restricted to}\{x,y\}) = \\\} \) using Top_1_L4 unfolding topology0_def
ultimately have cl_y: \( \text{Closure}(\{y\},T\{restricted to}\{x,y\})=\{y\\} \) using tot
assume \( \{x,y\}-B=0 \)
with \( B\in Pow(\{x,y\})-\{0\} \) have B: \( \{x,y\}=B \)
{
fix \( m \)
assume dis: \( m\in \{x,y\} \) and B_def: \( B= \text{Closure}(\{m\},T\{restricted to}\{x,y\}\} \)
{
assume \( m=y \)
with B_def have \( B= \text{Closure}(\{y\},T\{restricted to}\{x,y\}\} \)
with cl_y have \( B=\{y\} \)
with B have \( \{x,y\}=\{y\} \)
moreover
have \( x\in \{x,y\} \)
ultimately have \( x\in \{y\} \)
with \( x\neq y \) have \( False \)
with dis have \( m=x \)
then have \( (\forall m\in \{x,y\}.\ B= \text{Closure}(\{m\},T\{restricted to}\{x,y\})\longrightarrow m=x \} \)
moreover
have \( B= \text{Closure}(\{x\},T\{restricted to}\{x,y\}\} \) using cl_x, B
ultimately have \( \exists t\in \{x,y\}.\ B= \text{Closure}(\{t\},T\{restricted to}\{x,y\}) \wedge (\forall m\in \{x,y\}.\ B= \text{Closure}(\{m\},T\{restricted to}\{x,y\})\longrightarrow m=t \\} \)
moreover {
}
}
}
}
ultimately have \( \exists t\in \{x,y\}.\ B= \text{Closure}(\{t\},T\{restricted to}\{x,y\}) \wedge (\forall m\in \{x,y\}.\ B= \text{Closure}(\{m\},T\{restricted to}\{x,y\})\longrightarrow m=t \\} \)
assume \( \{x,y\}-B\neq 0 \)
with \( \{x,y\}-B\in \{0,\{x\},\{x,y\}\} \) have or: \( \{x,y\}-B=\{x\}\vee \{x,y\}-B=\{x,y\} \)
{
assume \( \{x,y\}-B=\{x\} \)
then have \( x\in \{x,y\}-B \)
with \( B\in \{\{x\},\{y\},\{x,y\}\} \), \( x\neq y \) have B: \( B=\{y\} \)
{
fix \( m \)
assume dis: \( m\in \{x,y\} \) and B_def: \( B= \text{Closure}(\{m\},T\{restricted to}\{x,y\}\} \)
{
assume \( m=x \)
with B_def have \( B= \text{Closure}(\{x\},T\{restricted to}\{x,y\}\} \)
with cl_x have \( B=\{x,y\} \)
with B have \( \{x,y\}=\{y\} \)
moreover
have \( x\in \{x,y\} \)
ultimately have \( x\in \{y\} \)
with \( x\neq y \) have \( False \)
with dis have \( m=y \)
moreover
have \( B= \text{Closure}(\{y\},T\{restricted to}\{x,y\}\} \) using cl_y, B
ultimately have \( \exists t\in \{x,y\}.\ B= \text{Closure}(\{t\},T\{restricted to}\{x,y\}) \wedge (\forall m\in \{x,y\}.\ B= \text{Closure}(\{m\},T\{restricted to}\{x,y\})\longrightarrow m=t \\} \)
moreover {
}
ultimately have \( \exists t\in \{x,y\}.\ B= \text{Closure}(\{t\},T\{restricted to}\{x,y\}) \wedge (\forall m\in \{x,y\}.\ B= \text{Closure}(\{m\},T\{restricted to}\{x,y\})\longrightarrow m=t \\} \)
assume \( \{x,y\}-B\neq \{x\} \)
with or have \( \{x,y\}-B=\{x,y\} \)
then have \( x\in \{x,y\}-B \), \( y\in \{x,y\}-B \)
with \( B\in \{\{x\},\{y\},\{x,y\}\} \), \( x\neq y \) have \( False \)
then have \( (T\{restricted to}\{x,y\})\{is sober\\} \) unfolding IsSober_def using tot
with \( T\{is anti-\}IsSober \), \( x\in A \), \( A\in T \), \( y\in \bigcup T-A \) have \( \{x,y}\text{ is in the spectrum of }IsSobe\} \) unfolding antiProperty_def
then have \( \{x,y\}\preceq 1 \) using sober_spectrum
moreover
have \( x\in \{x,y\} \)
moreover have \( \{x,y\}\preceq 1 \Longrightarrow x\in \{x,y\} \Longrightarrow \{x,y\}=\{x\} \) using lepoll_1_is_sing
ultimately have \( \{x,y\}=\{x\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
with \( x\neq y \) have \( False \)
then have \( T\subseteq \{0,\bigcup T\} \)
moreover
qed
have \( 0\in T \) using empty_open, topSpaceAssum
ultimately show \( T=\{0,\bigcup T\} \) using topSpaceAssum unfolding IsATopology_def
end
Definition of IsConnected:
\( T \text{ is connected } \equiv \forall U.\ (U\in T \wedge (U \text{ is closed in }T)) \longrightarrow U=0\vee U=\bigcup T \)
Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge (\bigcup T)\setminus D \in T) \)
Definition of Spec:
\( Spec \equiv \{I\in \mathcal{I} .\ I\triangleleft _pR\} \)
lemma Pow_is_top: shows \( Pow(X) \text{ is a topology } \)
lemma empty_open:
assumes \( T \text{ is a topology } \)
shows \( \emptyset \in T \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
lemma conn_spectrum: shows \( (A\text{ is in the spectrum of }IsConnected) \longleftrightarrow A\preceq 1 \)
Definition of IsTotDis:
\( IsTotDis \equiv ANTI(IsConnected) \)
Definition of antiProperty:
\( T\{is anti-\}P \equiv \forall A\in Pow(\bigcup T).\ P(T\text{ restricted to }A) \longrightarrow (A \text{ is in the spectrum of } P) \)
Definition of IsHConnected:
\( T\text{ is hyperconnected } \equiv \forall U V.\ U\in T \wedge V\in T \wedge U\cap V=0 \longrightarrow U=0\vee V=0 \)
Definition of Cofinite:
\( CoFinite X \equiv \text{CoCardinal}(X,nat) \)
Definition of CoCardinal:
\( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)
lemma less_less_imp_un_less:
assumes \( A\prec Q \) and \( B\prec Q \) and \( \text{InfCard}(Q) \)
shows \( A \cup B\prec Q \) lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T \setminus A) = \bigcup T \setminus int(A) \) lemma (in topology0) Top_3_L9:
assumes \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \) lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \) lemma (in topology0) Top_3_L5:
assumes \( D_1 \text{ is closed in } T \), \( D_2 \text{ is closed in } T \)
shows \( (D_1\cap D_2) \text{ is closed in } T \), \( (D_1\cup D_2) \text{ is closed in } T \) lemma (in topology0) cl_contains_set:
assumes \( A \subseteq \bigcup T \)
shows \( A \subseteq cl(A) \) lemma (in topology0) Top_3_L13:
assumes \( B \text{ is closed in } T \), \( A\subseteq B \)
shows \( cl(A) \subseteq B \) lemma (in topology0) cl_point_imp_HConn:
assumes \( x\in \bigcup T \)
shows \( (T\text{ restricted to } \text{Closure}(\{x\},T))\text{ is hyperconnected } \) lemma HConn_imp_Conn:
assumes \( T\text{ is hyperconnected } \)
shows \( T\text{ is connected } \) lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T \setminus A) = \bigcup T \setminus int(A) \) lemma (in topology0) Top_3_L8:
assumes \( A \subseteq \bigcup T \)
shows \( A \text{ is closed in } T \longleftrightarrow cl(A) = A \)Definition of isT1:
\( T \text{ is }T_1 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ (x\in U \wedge y\notin U))) \)
lemma HConn_spectrum: shows \( (A\text{ is in the spectrum of }IsHConnected) \longleftrightarrow A\preceq 1 \)
Definition of Closure:
\( \text{Closure}(A,T) \equiv \bigcap Closed \text{Covers}(A,T) \)
Definition of ClosedCovers:
\( Closed \text{Covers}(A,T) \equiv \{D \in Pow(\bigcup T).\ D \text{ is closed in } T \wedge A\subseteq D\} \)
Definition of IsSober:
\( T\{is sober\} \equiv \forall A\in Pow(\bigcup T)-\{0\}.\ (A\text{ is closed in }T \wedge ((T\text{ restricted to }A)\text{ is hyperconnected })) \longrightarrow (\exists x\in \bigcup T.\ A= \text{Closure}(\{x\},T) \wedge (\forall y\in \bigcup T.\ A= \text{Closure}(\{y\},T) \longrightarrow y=x) ) \)
Definition of isT0:
\( T \text{ is }T_0 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ (x\in U \wedge y\notin U) \vee (y\in U \wedge x\notin U))) \)
Definition of isT2:
\( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)
lemma union_cocardinal:
assumes \( T\neq 0 \)
shows \( \bigcup \text{CoCardinal}(X,T) = X \) lemma subspace_cocardinal: shows \( \text{CoCardinal}(X,T) \text{ restricted to } Y = \text{CoCardinal}(Y\cap X,T) \)
lemma Cofinite_nat_HConn:
assumes \( \neg (X\prec nat) \)
shows \( (CoFinite X)\text{ is hyperconnected } \) corollary cocardinal_is_T1:
assumes \( \text{InfCard}(K) \)
shows \( \text{CoCardinal}(X,K) \text{ is }T_1 \) theorem Top_subbase:
assumes \( T = \{\bigcup A.\ A\in Pow(\{\bigcap A.\ A \in \text{FinPow}(B)\})\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a subbase for } T \) lemma CoCar_is_topology:
assumes \( InfCard (Q) \)
shows \( \text{CoCardinal}(X,Q) \text{ is a topology } \) theorem excludedset_is_topology: shows \( \text{ExcludedSet}(X,Q) \text{ is a topology } \)
lemma union_excludedset: shows \( \bigcup \text{ExcludedSet}(X,T) = X \)
Definition of joinT:
\( (\forall T\in M.\ T\text{ is a topology } \wedge (\forall Q\in M.\ \bigcup Q=\bigcup T)) \Longrightarrow (joinT M \equiv \text{The } T.\ (\bigcup M)\text{ is a subbase for } T) \)
Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
Definition of ExcludedPoint:
\( \text{ExcludedPoint}(X,p) \equiv \text{ExcludedSet}(X,\{p\}) \)
Definition of ExcludedSet:
\( \text{ExcludedSet}(X,U) \equiv \{F\in Pow(X).\ U \cap F=0\}\cup \{X\} \)
theorem topology0_CoCardinal:
assumes \( \text{InfCard}(T) \)
shows \( topology0(\text{CoCardinal}(X,T)) \) lemma join_top_cofinite_excluded_set: shows \( (joinT \{CoFinite nat,\text{ExcludedSet}(nat,\{0,1\})\})=(CoFinite nat)\cup \text{ExcludedSet}(nat,\{0,1\}) \)
lemma subspace_excludedset: shows \( \text{ExcludedSet}(X,T) \text{ restricted to } Y = \text{ExcludedSet}(Y \cap X, T) \)
lemma empty_excludedset:
assumes \( T\cap X=0 \)
shows \( \text{ExcludedSet}(X,T) = Pow(X) \) lemma discrete_tot_dis: shows \( Pow(X) \{is totally-disconnected\} \)
lemma (in topology0) open_neigh_open:
assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)
shows \( V\in T \) theorem (in topology0) T1_sober_imp_anti_HConn:
assumes \( T\text{ is }T_1 \) and \( T\{is sober\} \)
shows \( T\{is anti-\}IsHConnected \) theorem anti_HConn_imp_T1:
assumes \( T\{is anti-\}IsHConnected \)
shows \( T\text{ is }T_1 \) theorem (in topology0) anti_HConn_imp_sober:
assumes \( T\{is anti-\}IsHConnected \)
shows \( T\{is sober\} \)Definition of IsUConnected:
\( T\text{ is ultraconnected }\equiv \forall A B.\ A\text{ is closed in }T\wedge B\text{ is closed in }T\wedge A\cap B=0 \longrightarrow A=0\vee B=0 \)
Definition of IsNormal:
\( T\text{ is normal } \equiv \forall A.\ A\text{ is closed in }T \longrightarrow (\forall B.\ B\text{ is closed in }T \wedge A\cap B=0 \longrightarrow \)
\( (\exists U\in T.\ \exists V\in T.\ A\subseteq U\wedge B\subseteq V\wedge U\cap V=0)) \)
lemma UConn_spectrum: shows \( (A\text{ is in the spectrum of }IsUConnected) \longleftrightarrow A\preceq 1 \)
theorem Q_P_imp_Spec:
assumes \( \forall T.\ ((T\text{ is a topology }\wedge P(T)\wedge Q(T))\longrightarrow ((\bigcup T)\text{ is in the spectrum of }P)) \) and \( Q\text{ is hereditary } \)
shows \( \forall T.\ T\text{ is a topology } \longrightarrow (Q(T)\longrightarrow (T\{is anti-\}P)) \) lemma Indiscrete_HConn: shows \( \{0,X}\text{ is hyperconnected \} \)
lemma (in topology0) Top_3_L1: shows \( (\bigcup T) \text{ is closed in } T \)
lemma sober_spectrum: shows \( (A\text{ is in the spectrum of }IsSober) \longleftrightarrow A\preceq 1 \)
lemma subspace_of_subspace:
assumes \( A\subseteq B \), \( B\subseteq \bigcup T \)
shows \( T\text{ restricted to }A=(T\text{ restricted to }B)\text{ restricted to }A \) theorem indiscrete_ptopology:
assumes \( X\neq 0 \)
shows \( (PTopology X \{X\})=\{0,X\} \) lemma indiscrete_partition:
assumes \( X\neq 0 \)
shows \( \{X\} \text{ is a partition of } X \) theorem (in topology0) T2_imp_anti_HConn:
assumes \( T\text{ is }T_2 \)
shows \( T\{is anti-\}IsHConnected \) lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
theorem (in topology0) anti_HConn_iff_T1_sober: shows \( (T\{is anti-\}IsHConnected) \longleftrightarrow (T\{is sober\}\wedge T\text{ is }T_1) \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
