begin
This theory continues the study of topological spaces, covering separation axioms, hereditability of topological properties, spectra of properties, and anti-properties.
Some results for separation axioms
First we will give a global characterization of \(T_1\)-spaces; which is interesting because it involves the cardinal \(\mathbb{N}\).
A topology is \(T_1\) if and only if it contains the cofinite topology.
lemma (in topology0) T1_cocardinal_coarser:
shows \( (T \text{ is }T_1) \longleftrightarrow (CoFinite (\bigcup T))\subseteq T \)proof{
}
}
}
}
}
{
}
}
qed
assume AS: \( T \text{ is }T_1 \)
{
fix \( x \)
assume p: \( x\in \bigcup T \)
{
fix \( y \)
assume \( y\in (\bigcup T)-\{x\} \)
with AS, p obtain \( U \) where \( U\in T \), \( y\in U \), \( x\notin U \) using isT1_def
then have \( U\in T \), \( y\in U \), \( U\subseteq (\bigcup T)-\{x\} \)
then have \( \exists U\in T.\ y\in U \wedge U\subseteq (\bigcup T)-\{x\} \)
then have \( \forall y\in (\bigcup T)-\{x\}.\ \exists U\in T.\ y\in U \wedge U\subseteq (\bigcup T)-\{x\} \)
then have \( \bigcup T-\{x\}\in T \) using open_neigh_open
with p have \( \{x\} \text{ is closed in }T \) using IsClosed_def
then have pointCl: \( \forall x\in \bigcup T.\ \{x\} \text{ is closed in } T \)
{
fix \( A \)
assume AS2: \( A\in \text{FinPow}(\bigcup T) \)
let \( p = \{\langle x,\{x\}\rangle .\ x\in A\} \)
have \( p\in A\rightarrow \{\{x\}.\ x\in A\} \) using Pi_def unfolding function_def
then have \( p:\text{bij}(A,\{\{x\}.\ x\in A\}) \) unfolding bij_def, inj_def, surj_def using apply_equality
then have \( A\approx \{\{x\}.\ x\in A\} \) unfolding eqpoll_def
with AS2 have \( Finite(\{\{x\}.\ x\in A\}) \) unfolding FinPow_def using eqpoll_imp_Finite_iff
then have \( \{\{x\}.\ x\in A\}\in \text{FinPow}(\{D \in Pow(\bigcup T) .\ D \text{ is closed in } T\}) \) using AS2, pointCl unfolding FinPow_def
then have \( (\bigcup \{\{x\}.\ x\in A\}) \text{ is closed in } T \) using fin_union_cl_is_cl
moreover
have \( \bigcup \{\{x\}.\ x\in A\}=A \)
ultimately have \( A \text{ is closed in } T \)
then have reg: \( \forall A\in \text{FinPow}(\bigcup T).\ A \text{ is closed in } T \)
{
fix \( U \)
assume AS2: \( U \in \text{CoCardinal}(\bigcup T,nat) \)
then have \( U\in Pow(\bigcup T) \), \( U=0 \vee ((\bigcup T)-U)\prec nat \) using CoCardinal_def
then have \( U\in Pow(\bigcup T) \), \( U=0 \vee Finite(\bigcup T-U) \) using lesspoll_nat_is_Finite
then have \( U\in Pow(\bigcup T) \), \( U\in T\vee (\bigcup T-U) \text{ is closed in } T \) using empty_open, topSpaceAssum, reg unfolding FinPow_def
then have \( U\in Pow(\bigcup T) \), \( U\in T\vee (\bigcup T-(\bigcup T-U))\in T \) using IsClosed_def
moreover
from this have \( (\bigcup T-(\bigcup T-U))=U \)
ultimately have \( U\in T \)
then show \( (CoFinite (\bigcup T))\subseteq T \) using Cofinite_def
assume \( (CoFinite (\bigcup T))\subseteq T \)
then have AS: \( \text{CoCardinal}(\bigcup T,nat) \subseteq T \) using Cofinite_def
{
fix \( x \) \( y \)
assume AS2: \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
have \( Finite(\{y\}) \)
then obtain \( n \) where \( \{y\}\approx n \), \( n\in nat \) using Finite_def
then have \( \{y\}\prec nat \) using n_lesspoll_nat, eq_lesspoll_trans
then have \( \{y\} \text{ is closed in } \text{CoCardinal}(\bigcup T,nat) \) using closed_sets_cocardinal, AS2(2)
then have \( (\bigcup T)-\{y\}\in \text{CoCardinal}(\bigcup T,nat) \) using union_cocardinal, IsClosed_def
with AS have \( (\bigcup T)-\{y\}\in T \)
moreover
from this, AS2(1,3) have \( x\in ((\bigcup T)-\{y\}) \wedge y\notin ((\bigcup T)-\{y\}) \)
ultimately have \( (\bigcup T)-\{y\}\in T \wedge x\in ((\bigcup T)-\{y\}) \wedge y\notin ((\bigcup T)-\{y\}) \)
then have \( \exists V.\ V\in T\wedge x\in V\wedge y\notin V \) by (rule exI )
then have \( \exists V\in T.\ x\in V\wedge y\notin V \)
then show \( T \text{ is }T_1 \) using isT1_def
In the previous proof, it is obvious that we don't need to check if ever cofinite set is open. It is enough to check if every singleton is closed.
corollary (in topology0) T1_iff_singleton_closed:
shows \( (T \text{ is }T_1) \longleftrightarrow (\forall x\in \bigcup T.\ \{x}\text{ is closed in }T\} \)proof assume AS: \( T \text{ is }T_1 \)
{
fix \( x \)
assume p: \( x\in \bigcup T \)
{
fix \( y \)
assume \( y\in (\bigcup T)-\{x\} \)
with AS, p obtain \( U \) where \( U\in T \), \( y\in U \), \( x\notin U \) using isT1_def
then have \( U\in T \), \( y\in U \), \( U\subseteq (\bigcup T)-\{x\} \)
then have \( \exists U\in T.\ y\in U \wedge U\subseteq (\bigcup T)-\{x\} \)
then have \( \forall y\in (\bigcup T)-\{x\}.\ \exists U\in T.\ y\in U \wedge U\subseteq (\bigcup T)-\{x\} \)
then have \( \bigcup T-\{x\}\in T \) using open_neigh_open
with p have \( \{x\} \text{ is closed in }T \) using IsClosed_def
then show pointCl: \( \forall x\in \bigcup T.\ \{x\} \text{ is closed in } T \)
next
assume pointCl: \( \forall x\in \bigcup T.\ \{x\} \text{ is closed in } T \)
{
fix \( A \)
assume AS2: \( A\in \text{FinPow}(\bigcup T) \)
let \( p = \{\langle x,\{x\}\rangle .\ x\in A\} \)
have \( p\in A\rightarrow \{\{x\}.\ x\in A\} \) using Pi_def unfolding function_def
then have \( p:\text{bij}(A,\{\{x\}.\ x\in A\}) \) unfolding bij_def, inj_def, surj_def using apply_equality
then have \( A\approx \{\{x\}.\ x\in A\} \) unfolding eqpoll_def
with AS2 have \( Finite(\{\{x\}.\ x\in A\}) \) unfolding FinPow_def using eqpoll_imp_Finite_iff
then have \( \{\{x\}.\ x\in A\}\in \text{FinPow}(\{D \in Pow(\bigcup T) .\ D \text{ is closed in } T\}) \) using AS2, pointCl unfolding FinPow_def
then have \( (\bigcup \{\{x\}.\ x\in A\}) \text{ is closed in } T \) using fin_union_cl_is_cl
moreover
have \( \bigcup \{\{x\}.\ x\in A\}=A \)
ultimately have \( A \text{ is closed in } T \)
then have reg: \( \forall A\in \text{FinPow}(\bigcup T).\ A \text{ is closed in } T \)
{
fix \( U \)
assume AS2: \( U\in \text{CoCardinal}(\bigcup T,nat) \)
then have \( U\in Pow(\bigcup T) \), \( U=0 \vee ((\bigcup T)-U)\prec nat \) using CoCardinal_def
then have \( U\in Pow(\bigcup T) \), \( U=0 \vee Finite(\bigcup T-U) \) using lesspoll_nat_is_Finite
then have \( U\in Pow(\bigcup T) \), \( U\in T\vee (\bigcup T-U) \text{ is closed in } T \) using empty_open, topSpaceAssum, reg unfolding FinPow_def
then have \( U\in Pow(\bigcup T) \), \( U\in T\vee (\bigcup T-(\bigcup T-U))\in T \) using IsClosed_def
moreover
from this have \( (\bigcup T-(\bigcup T-U))=U \)
ultimately have \( U\in T \)
then have \( (CoFinite (\bigcup T))\subseteq T \) using Cofinite_def
then show \( T \text{ is }T_1 \) using T1_cocardinal_coarser
qed
Secondly, let's show that the CoCardinal X Q topologies for different sets \(Q\) are all ordered as the partial order of sets. (The order is linear when considering only cardinals)
lemma order_cocardinal_top:
assumes \( Q1\preceq Q2 \)
shows \( \text{CoCardinal}(X,Q1) \subseteq \text{CoCardinal}(X,Q2) \)proof fix \( x \)
assume \( x \in \text{CoCardinal}(X,Q1) \)
then have \( x\in Pow(X) \), \( x=0\vee (X-x)\prec Q1 \) using CoCardinal_def
with assms have \( x\in Pow(X) \), \( x=0\vee (X-x)\prec Q2 \) using lesspoll_trans2
then show \( x\in \text{CoCardinal}(X,Q2) \) using CoCardinal_def
qed
Any cocardinal topology defined with respect to an infinite cardinal is \(T_1\).
corollary cocardinal_is_T1:
assumes \( \text{InfCard}(K) \)
shows \( \text{CoCardinal}(X,K) \text{ is }T_1 \)proof have \( nat\leq K \) using InfCard_def, assms
then have \( nat\subseteq K \) using le_imp_subset
then have \( nat\preceq K \), \( K\neq 0 \) using subset_imp_lepoll
then have \( \text{CoCardinal}(X,nat) \subseteq \text{CoCardinal}(X,K) \), \( \bigcup \text{CoCardinal}(X,K)=X \) using order_cocardinal_top, union_cocardinal
then show \( thesis \) using T1_cocardinal_coarser, topology0_CoCardinal, assms, Cofinite_def
qed
In \(T_2\)-spaces, filters and nets have at most one limit point.
lemma (in topology0) T2_imp_unique_limit_filter:
assumes \( T \text{ is }T_2 \), \( \mathfrak{F} \text{ is a filter on }\bigcup T \), \( \mathfrak{F} \rightarrow _F x \), \( \mathfrak{F} \rightarrow _F y \)
shows \( x=y \)proof{
}
assume \( x\neq y \)
from assms(3,4) have \( x\in \bigcup T \), \( y\in \bigcup T \) using FilterConverges_def, assms(2)
with \( x\neq y \) have \( \exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0 \) using assms(1), isT2_def
then obtain \( U \) \( V \) where \( x\in U \), \( y\in V \), \( U\cap V=0 \), \( U\in T \), \( V\in T \)
then have \( U\in \{A\in Pow(\bigcup T).\ x\in \text{Interior}(A,T)\} \), \( V\in \{A\in Pow(\bigcup T).\ y\in \text{Interior}(A,T)\} \) using Top_2_L3
then have \( U\in \mathfrak{F} \), \( V\in \mathfrak{F} \) using FilterConverges_def, assms(2), assms(3,4)
then have \( U\cap V\in \mathfrak{F} \) using IsFilter_def, assms(2)
with \( U\cap V=0 \) have \( 0\in \mathfrak{F} \)
then have \( False \) using IsFilter_def, assms(2)
then show \( thesis \)
qed
In \(T_2\)-spaces, nets also have at most one limit point.
lemma (in topology0) T2_imp_unique_limit_net:
assumes \( T \text{ is }T_2 \), \( N \text{ is a net on }\bigcup T \), \( N \rightarrow _N x \), \( N \rightarrow _N y \)
shows \( x=y \)proof have \( (Filter N.\ .\ (\bigcup T)) \text{ is a filter on } (\bigcup T) \), \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \), \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F y \) using filter_of_net_is_filter(1), net_conver_filter_of_net_conver, assms(2), assms(3,4)
with assms(1) show \( thesis \) using T2_imp_unique_limit_filter
qed
In fact, \(T_2\)-spaces are characterized by this property. For this proof we build a filter containing the union of two filters.
lemma (in topology0) unique_limit_filter_imp_T2:
assumes \( \forall x\in \bigcup T.\ \forall y\in \bigcup T.\ \forall \mathfrak{F} .\ ((\mathfrak{F} \text{ is a filter on }\bigcup T) \wedge (\mathfrak{F} \rightarrow _F x) \wedge (\mathfrak{F} \rightarrow _F y)) \longrightarrow x=y \)
shows \( T \text{ is }T_2 \)proof{
}
}
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
{
assume \( \forall U\in T.\ \forall V\in T.\ (x\in U \wedge y\in V) \longrightarrow U\cap V\neq 0 \)
let \( Ux = \{A\in Pow(\bigcup T).\ x\in int(A)\} \)
let \( Uy = \{A\in Pow(\bigcup T).\ y\in int(A)\} \)
let \( FF = Ux \cup Uy \cup \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
have sat: \( FF \text{ satisfies the filter base condition } \)proof
{
}
}
}
fix \( A \) \( B \)
assume as: \( A\in FF \), \( B\in FF \)
{
assume \( A\in Ux \)
{
assume \( B\in Ux \)
with \( x\in \bigcup T \), \( A\in Ux \) have \( A\cap B\in Ux \) using neigh_filter(1), IsFilter_def
then have \( A\cap B\in FF \)
moreover {
}
moreover {
}
ultimately have \( A\cap B\in FF \) using as(2)
assume \( B\in Uy \)
with \( A\in Ux \) have \( A\cap B\in FF \)
assume \( B\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then obtain \( AA \) \( BB \) where \( B=AA\cap BB \), \( AA\in Ux \), \( BB\in Uy \)
with \( x\in \bigcup T \), \( A\in Ux \) have \( A\cap B=(A\cap AA)\cap BB \), \( A\cap AA\in Ux \) using neigh_filter(1), IsFilter_def
with \( BB\in Uy \) have \( A\cap B\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then have \( A\cap B\in FF \)
moreover {
}
}
moreover {
}
}
ultimately have \( A\cap B\in FF \) using as(1)
assume \( A\in Uy \)
{
assume \( B\in Uy \)
with \( y\in \bigcup T \), \( A\in Uy \) have \( A\cap B\in Uy \) using neigh_filter(1), IsFilter_def
then have \( A\cap B\in FF \)
moreover {
}
moreover {
}
ultimately have \( A\cap B\in FF \) using as(2)
assume \( B\in Ux \)
with \( A\in Uy \) have \( B\cap A\in FF \)
moreover
have \( A\cap B=B\cap A \)
ultimately have \( A\cap B\in FF \)
assume \( B\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then obtain \( AA \) \( BB \) where \( B=AA\cap BB \), \( AA\in Ux \), \( BB\in Uy \)
with \( y\in \bigcup T \), \( A\in Uy \) have \( A\cap B=AA\cap (A\cap BB) \), \( A\cap BB\in Uy \) using neigh_filter(1), IsFilter_def
with \( AA\in Ux \) have \( A\cap B\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then have \( A\cap B\in FF \)
assume \( A\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then obtain \( AA \) \( BB \) where AB: \( A=AA\cap BB \), \( AA\in Ux \), \( BB\in Uy \)
{
assume \( B\in Uy \)
with \( BB\in Uy \), \( y\in \bigcup T \) have B: \( B\cap BB\in Uy \) using neigh_filter(1), IsFilter_def
moreover
from \( A=AA\cap BB \) have \( A\cap B=AA\cap (B\cap BB) \)
ultimately have \( A\cap B\in FF \) using AB(2), B
moreover {
}
moreover {
}
ultimately have \( A\cap B\in FF \) using as(2)
assume \( B\in Ux \)
with \( AA\in Ux \), \( x\in \bigcup T \) have BA: \( B\cap AA\in Ux \) using neigh_filter(1), IsFilter_def
moreover
from \( A=AA\cap BB \) have \( A\cap B=(B\cap AA)\cap BB \)
ultimately have \( A\cap B\in FF \) using AB(3)
assume \( B\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then obtain \( AA2 \) \( BB2 \) where \( B=AA2\cap BB2 \), \( AA2\in Ux \), \( BB2\in Uy \)
from \( B=AA2\cap BB2 \), \( A=AA\cap BB \) have \( A\cap B=(AA\cap AA2)\cap (BB\cap BB2) \)
moreover
from \( AA\in Ux \), \( AA2\in Ux \), \( x\in \bigcup T \) have \( AA\cap AA2\in Ux \) using neigh_filter(1), IsFilter_def
moreover from \( BB\in Uy \), \( BB2\in Uy \), \( y\in \bigcup T \) have \( BB\cap BB2\in Uy \) using neigh_filter(1), IsFilter_def
ultimately have \( A\cap B\in FF \)
then have \( \exists D\in FF.\ D\subseteq A\cap B \) unfolding Bex_def
then have \( \forall A\in FF.\ \forall B\in FF.\ \exists D\in FF.\ D\subseteq A\cap B \)
moreover
}
qed
from \( x\in \bigcup T \) have \( \bigcup T\in Ux \) using neigh_filter(1), IsFilter_def
then have \( FF\neq 0 \)
moreover {
assume \( 0\in FF \)
moreover
from \( x\in \bigcup T \) have \( 0\notin Ux \) using neigh_filter(1), IsFilter_def
moreover from \( y\in \bigcup T \) have \( 0\notin Uy \) using neigh_filter(1), IsFilter_def
ultimately have \( 0\in \{A\cap B.\ \langle A,B\rangle \in Ux \times Uy\} \)
then obtain \( A \) \( B \) where \( 0=A\cap B \), \( A\in Ux \), \( B\in Uy \)
then have \( x\in int(A) \), \( y\in int(B) \)
moreover
from this, \( 0=A\cap B \) have \( int(A)\cap int(B)=0 \) using Top_2_L1
moreover have \( int(A)\in T \), \( int(B)\in T \) using Top_2_L2
moreover note \( \forall U\in T.\ \forall V\in T.\ x\in U\wedge y\in V \longrightarrow U\cap V\neq 0 \)
ultimately have \( False \)
then have \( 0\notin FF \)
ultimately show \( thesis \) using SatisfiesFilterBase_def
moreover
have \( FF\subseteq Pow(\bigcup T) \)
moreover have \( FF \subseteq Pow(\bigcup T) \Longrightarrow \)
\( FF \text{ satisfies the filter base condition } \Longrightarrow \)
\( ((FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\}) \wedge (\bigcup \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\}) = \bigcup T) \longleftrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} = \{A \in Pow(\bigcup T) .\ \exists D\in FF.\ D \subseteq A\} \) by (rule base_unique_filter_set2 )
then have \( FF \subseteq Pow(\bigcup T) \Longrightarrow \)
\( FF \text{ satisfies the filter base condition } \Longrightarrow \)
\( ((FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\}) \wedge (\bigcup \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\}) = \bigcup T) \)
ultimately have bas: \( FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \), \( \bigcup \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\}=\bigcup T \)
then have fil: \( \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \text{ is a filter on } \bigcup T \) using basic_filter, sat
have \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in FF.\ D\subseteq U) \)
have R: \( \bigwedge x.\ \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \text{ is a filter on } \bigcup T \Longrightarrow FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \Longrightarrow \forall U\in Pow(\bigcup T).\ \)
\( x \in int(U) \longrightarrow (\exists D\in FF.\ D \subseteq U) \Longrightarrow x \in \bigcup T \Longrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F x\text{ in }T \) by (rule convergence_filter_base2 )
then have \( \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \text{ is a filter on } \bigcup T \Longrightarrow FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \Longrightarrow \forall U\in Pow(\bigcup T).\ \)
\( x \in int(U) \longrightarrow (\exists D\in FF.\ D \subseteq U) \Longrightarrow x \in \bigcup T \Longrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F x\text{ in }T \)
with fil, bas(1) have \( \forall U\in Pow(\bigcup T).\ x \in int(U) \longrightarrow (\exists D\in FF.\ D \subseteq U) \Longrightarrow x \in \bigcup T \Longrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F x\text{ in }T \)
with \( x\in \bigcup T \) have \( \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F x \)
moreover {
}
moreover
from R have \( \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \text{ is a filter on } \bigcup T \Longrightarrow FF \text{ is a base filter } \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \Longrightarrow \forall U\in Pow(\bigcup T).\ \)
\( y \in int(U) \longrightarrow (\exists D\in FF.\ D \subseteq U) \Longrightarrow y \in \bigcup T \Longrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F y\text{ in }T \)
with fil, bas(1) have I: \( \forall U\in Pow(\bigcup T).\ \)
\( y \in int(U) \longrightarrow (\exists D\in FF.\ D \subseteq U) \Longrightarrow y \in \bigcup T \Longrightarrow \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F y\text{ in }T \)
have \( \forall U\in Pow(\bigcup T).\ y\in int(U) \longrightarrow (\exists D\in FF.\ D\subseteq U) \)
with I, \( y\in \bigcup T \) have \( \{A\in Pow(\bigcup T).\ \exists D\in FF.\ D\subseteq A\} \rightarrow _F y \)
note \( x\in \bigcup T \), \( y\in \bigcup T \)
ultimately have \( x=y \) using assms, fil
with \( x\neq y \) have \( False \)
then have \( \exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0 \)
then show \( thesis \) using isT2_def
qed
Uniqueness of net limits is also sufficient for \(T_2\).
lemma (in topology0) unique_limit_net_imp_T2:
assumes \( \forall x\in \bigcup T.\ \forall y\in \bigcup T.\ \forall N.\ ((N \text{ is a net on }\bigcup T) \wedge (N \rightarrow _N x) \wedge (N \rightarrow _N y)) \longrightarrow x=y \)
shows \( T \text{ is }T_2 \)proof{
}
fix \( x \) \( y \) \( \mathfrak{F} \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( \mathfrak{F} \text{ is a filter on }\bigcup T \), \( \mathfrak{F} \rightarrow _F x \), \( \mathfrak{F} \rightarrow _F y \)
then have \( (\text{Net}(\mathfrak{F} )) \text{ is a net on } \bigcup T \), \( (Net \mathfrak{F} ) \rightarrow _N x \), \( (Net \mathfrak{F} ) \rightarrow _N y \) using filter_conver_net_of_filter_conver, net_of_filter_is_net
with \( x\in \bigcup T \), \( y\in \bigcup T \) have \( x=y \) using assms
then have \( \forall x\in \bigcup T.\ \forall y\in \bigcup T.\ \forall \mathfrak{F} .\ ((\mathfrak{F} \text{ is a filter on }\bigcup T) \wedge (\mathfrak{F} \rightarrow _F x) \wedge (\mathfrak{F} \rightarrow _F y)) \longrightarrow x=y \)
then show \( thesis \) using unique_limit_filter_imp_T2
qed
The topology which comes from a filter as in @{thm "top_of_filter"} is not \(T_2\) generally. We will see in this file later on, that the exceptions are a consequence of the spectrum.
corollary filter_T2_imp_card1:
assumes \( (\mathfrak{F} \cup \{0\}) \text{ is }T_2 \), \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \), \( x\in \bigcup \mathfrak{F} \)
shows \( \bigcup \mathfrak{F} =\{x\} \)proof{
}
fix \( y \)
assume \( y\in \bigcup \mathfrak{F} \)
then have \( \mathfrak{F} \rightarrow _F y\text{ in }(\mathfrak{F} \cup \{0\}) \) using lim_filter_top_of_filter, assms(2)
moreover
have \( \mathfrak{F} \rightarrow _F x\text{ in }(\mathfrak{F} \cup \{0\}) \) using lim_filter_top_of_filter, assms(2,3)
moreover have \( \bigcup \mathfrak{F} =\bigcup (\mathfrak{F} \cup \{0\}) \)
moreover have \( topology0(\mathfrak{F} \cup \{0\}) \) using topology0_filter, assms(2)
ultimately have \( y=x \) using T2_imp_unique_limit_filter, assms
then have \( \bigcup \mathfrak{F} \subseteq \{x\} \)
with assms(3) show \( thesis \)
qed
There are more separation axioms that just \(T_0\), \(T_1\) or \(T_2\)
definition
\( 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)) \)
A topological space is \(T_4\) if it is both \(T_1\) and normal.
definition
\( T\{is T_4\} \equiv (T\text{ is }T_1) \wedge (T\text{ is normal }) \)
Every \(T_4\)-space is \(T_3\).
lemma (in topology0) T4_is_T3:
assumes \( T\{is T_4\} \)
shows \( T\text{ is }T_3 \)proof from assms have nor: \( T\text{ is normal } \) using isT4_def
from assms have \( T\text{ is }T_1 \) using isT4_def
then have \( Cofinite (\bigcup T)\subseteq T \) using T1_cocardinal_coarser
{
fix \( A \)
assume AS: \( A\text{ is closed in }T \)
{
fix \( x \)
assume \( x\in \bigcup T-A \)
have \( Finite(\{x\}) \)
then obtain \( n \) where \( \{x\}\approx n \), \( n\in nat \) unfolding Finite_def
then have \( \{x\}\preceq n \), \( n\in nat \) using eqpoll_imp_lepoll
then have \( \{x\}\prec nat \) using n_lesspoll_nat, lesspoll_trans1
with \( x\in \bigcup T-A \) have \( \{x\} \text{ is closed in } (Cofinite (\bigcup T)) \) using Cofinite_def, closed_sets_cocardinal
then have \( \bigcup T-\{x\}\in \text{Cofinite}(\bigcup T) \) unfolding IsClosed_def using union_cocardinal, Cofinite_def
with \( Cofinite (\bigcup T)\subseteq T \) have \( \bigcup T-\{x\}\in T \)
with \( x\in \bigcup T-A \) have \( \text{ x}{is closed in} } \), \( A\cap \{x\}=0 \) using IsClosed_def
with nor, AS have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U\wedge \{x\}\subseteq V\wedge U\cap V=0 \) unfolding IsNormal_def
then have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U\wedge x\in V\wedge U\cap V=0 \)
then have \( \forall x\in \bigcup T-A.\ \exists U\in T.\ \exists V\in T.\ A\subseteq U\wedge x\in V\wedge U\cap V=0 \)
then have \( T\text{ is regular } \) using IsRegular_def
with \( T\text{ is }T_1 \) show \( thesis \) unfolding isT3_def using T1_is_T0
qed
Regularity can be rewritten in terms of existence of certain neighboorhoods.
lemma (in topology0) regular_imp_exist_clos_neig:
assumes \( T\text{ is regular } \) and \( U\in T \) and \( x\in U \)
shows \( \exists V\in T.\ x\in V \wedge cl(V)\subseteq U \)proof from assms(2) have \( (\bigcup T-U)\text{ is closed in }T \) using Top_3_L9
moreover
from assms(2,3) have \( x\in \bigcup T \)
moreover note assms(1,3)
ultimately obtain \( A \) \( B \) where \( A\in T \) and \( B\in T \) and \( A\cap B=0 \) and \( (\bigcup T-U)\subseteq A \) and \( x\in B \) unfolding IsRegular_def
from \( A\cap B=0 \), \( B\in T \) have \( B\subseteq \bigcup T-A \)
with \( A\in T \) have \( cl(B)\subseteq \bigcup T-A \) using Top_3_L9, Top_3_L13
moreover
qed
from \( (\bigcup T-U)\subseteq A \), assms(3) have \( \bigcup T-A\subseteq U \)
moreover note \( x\in B \), \( B\in T \)
ultimately have \( B\in T \wedge x\in B \wedge cl(B)\subseteq U \)
then show \( thesis \)
The converse: existence of closed neighborhood bases implies regularity.
lemma (in topology0) exist_clos_neig_imp_regular:
assumes \( \forall x\in \bigcup T.\ \forall U\in T.\ x\in U \longrightarrow (\exists V\in T.\ x\in V\wedge cl(V)\subseteq U) \)
shows \( T\text{ is regular } \)proof{
}
}
fix \( F \)
assume \( F\text{ is closed in }T \)
{
fix \( x \)
assume \( x\in \bigcup T-F \)
with \( F\text{ is closed in }T \) have \( x\in \bigcup T \), \( \bigcup T-F\in T \), \( F\subseteq \bigcup T \) unfolding IsClosed_def
with assms, \( x\in \bigcup T-F \) have \( \exists V\in T.\ x\in V \wedge cl(V)\subseteq \bigcup T-F \)
then obtain \( V \) where \( V\in T \), \( x\in V \), \( cl(V)\subseteq \bigcup T-F \)
from \( V\in T \) have I: \( \bigcup T-(\bigcup T-V)=V \)
from \( cl(V)\subseteq \bigcup T-F \), \( F\subseteq \bigcup T \) have \( F\subseteq \bigcup T-cl(V) \)
moreover
from Top_3_L11(2) have \( \bigcup T-V \subseteq \bigcup T \Longrightarrow cl(\bigcup T-(\bigcup T-V)) = \bigcup T-int(\bigcup T-V) \)
with I have \( cl(V)=\bigcup T-int(\bigcup T-V) \)
ultimately have \( F\subseteq int(\bigcup T-V) \)
moreover
have \( int(\bigcup T-V)\subseteq \bigcup T-V \) using Top_2_L1
then have \( V\cap (int(\bigcup T-V))=0 \)
moreover note \( x\in V \), \( V\in T \)
ultimately have \( V\in T \), \( int(\bigcup T-V)\in T \), \( F\subseteq int(\bigcup T-V) \wedge x\in V \wedge (int(\bigcup T-V))\cap V=0 \) using Top_2_L2
then have \( \exists U\in T.\ \exists V\in T.\ F\subseteq U \wedge x\in V \wedge U\cap V=0 \)
then have \( \forall x\in \bigcup T-F.\ \exists U\in T.\ \exists V\in T.\ F\subseteq U \wedge x\in V \wedge U\cap V=0 \)
then show \( thesis \) using IsRegular_def
qed
Regularity is equivalent to the existence of closed neighborhood bases at every point.
lemma (in topology0) regular_eq:
shows \( T\text{ is regular } \longleftrightarrow (\forall x\in \bigcup T.\ \forall U\in T.\ x\in U \longrightarrow (\exists V\in T.\ x\in V\wedge cl(V)\subseteq U)) \) using regular_imp_exist_clos_neig, exist_clos_neig_imp_regularA Hausdorff space separates compact spaces from points.
theorem (in topology0) T2_compact_point:
assumes \( T\text{ is }T_2 \), \( A\text{ is compact in }T \), \( x\in \bigcup T \), \( x\notin A \)
shows \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge x\in V \wedge U\cap V=0 \)proof{
}
assume \( A=0 \)
then have \( A\subseteq 0\wedge x\in \bigcup T\wedge (0\cap (\bigcup T)=0) \) using assms(3)
then have \( thesis \) using empty_open, topSpaceAssum unfolding IsATopology_def
moreover {
}
}
}
}
}
ultimately show \( thesis \)
qed
assume noEmpty: \( A\neq 0 \)
let \( U = \{\langle U,V\rangle \in T\times T.\ x\in U\wedge U\cap V=0\} \)
{
fix \( y \)
assume \( y\in A \)
with \( x\notin A \), assms(4) have \( x\neq y \)
moreover
from \( y\in A \) have \( x\in \bigcup T \), \( y\in \bigcup T \) using assms(2,3) unfolding IsCompact_def
ultimately obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( U\cap V=0 \), \( x\in U \), \( y\in V \) using assms(1) unfolding isT2_def
then have \( \exists \langle U,V\rangle \in U.\ y\in V \)
then have \( \forall y\in A.\ \exists \langle U,V\rangle \in U.\ y\in V \)
then have \( A\subseteq \bigcup \{\text{snd}(B).\ B\in U\} \)
moreover
have \( \{\text{snd}(B).\ B\in U\}\in Pow(T) \)
ultimately have \( \exists N\in \text{FinPow}(\{\text{snd}(B).\ B\in U\}).\ A\subseteq \bigcup N \) using assms(2) unfolding IsCompact_def
then obtain \( N \) where ss: \( N\in \text{FinPow}(\{\text{snd}(B).\ B\in U\}) \), \( A\subseteq \bigcup N \)
with \( \{\text{snd}(B).\ B\in U\}\in Pow(T) \) have \( A\subseteq \bigcup N \), \( N\in Pow(T) \) unfolding FinPow_def
then have NN: \( A\subseteq \bigcup N \), \( \bigcup N\in T \) using topSpaceAssum unfolding IsATopology_def
from ss have \( Finite(N) \), \( N\subseteq \{\text{snd}(B).\ B\in U\} \) unfolding FinPow_def
then obtain \( n \) where \( n\in nat \), \( N\approx n \) unfolding Finite_def
then have \( N\preceq n \) using eqpoll_imp_lepoll
from noEmpty, \( A\subseteq \bigcup N \) have NnoEmpty: \( N\neq 0 \)
let \( QQ = \{\langle n,\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\rangle .\ n\in N\} \)
have QQPi: \( QQ:N\rightarrow \{\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}.\ n\in N\} \) unfolding Pi_def, function_def, domain_def
{
fix \( n \)
assume \( n\in N \)
with \( N\subseteq \{\text{snd}(B).\ B\in U\} \) obtain \( B \) where \( n=\text{snd}(B) \), \( B\in U \)
then have \( \text{fst}(B)\in \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\} \)
then have \( \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\neq 0 \)
moreover
from \( n\in N \) have \( \langle n,\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\rangle \in QQ \)
with QQPi have \( QQn=\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\} \) using apply_equality
ultimately have \( QQn\neq 0 \)
then have \( \forall n\in N.\ QQn\neq 0 \)
with \( n\in nat \), \( N\preceq n \) have \( \exists f.\ f\in \text{Pi}(N,\lambda t.\ QQt) \wedge (\forall t\in N.\ ft\in QQt) \) using finite_choice unfolding AxiomCardinalChoiceGen_def
then obtain \( f \) where fPI: \( f\in \text{Pi}(N,\lambda t.\ QQt) \), \( (\forall t\in N.\ ft\in QQt) \)
from NnoEmpty obtain \( q \) where q: \( q:N \)
with fPI(1) have \( fq\in \text{range}(f) \) using apply_rangeI
then have \( \text{range}(f)\neq 0 \)
{
fix \( t \)
assume \( t\in N \)
then have \( ft\in QQt \) using fPI(2)
with \( t\in N \) have \( ft\in \bigcup (QQN) \), \( QQt\subseteq \bigcup (QQN) \) using func_imagedef, QQPi
then have reg: \( \forall t\in N.\ ft\in \bigcup (QQN) \), \( \forall t\in N.\ QQt\subseteq \bigcup (QQN) \)
{
fix \( tt \)
assume \( tt\in f \)
with fPI(1) have \( tt\in Sigma(N, ()(QQ)) \) unfolding Pi_def
then have \( tt\in (\bigcup xa\in N.\ \bigcup y\in QQxa.\ \{\langle xa,y\rangle \}) \) unfolding Sigma_def
then obtain \( xa \) \( y \) where \( xa\in N \), \( y\in QQxa \), \( tt=\langle xa,y\rangle \)
with reg(2) have \( y\in \bigcup (QQN) \)
with \( tt=\langle xa,y\rangle \), \( xa\in N \) have \( tt\in (\bigcup xa\in N.\ \bigcup y\in \bigcup (QQN).\ \{\langle xa,y\rangle \}) \)
then have \( tt\in N\times (\bigcup (QQN)) \) unfolding Sigma_def
then have ffun: \( f:N\rightarrow \bigcup (QQN) \) using fPI(1) unfolding Pi_def
then have \( f\in \text{surj}(N,\text{range}(f)) \) using fun_is_surj
with \( N\preceq n \), \( n\in nat \) have \( \text{range}(f)\preceq N \) using surj_fun_inv_2, nat_into_Ord
with \( N\preceq n \) have \( \text{range}(f)\preceq n \) using lepoll_trans
with \( n\in nat \) have \( Finite(\text{range}(f)) \) using n_lesspoll_nat, lesspoll_nat_is_Finite, lesspoll_trans1
moreover
from ffun have rr: \( \text{range}(f)\subseteq \bigcup (QQN) \) unfolding Pi_def
then have \( \text{range}(f)\subseteq T \)
ultimately have \( \text{range}(f)\in \text{FinPow}(T) \) unfolding FinPow_def
with \( \text{range}(f)\neq 0 \) have \( \bigcap \text{range}(f)\in T \) using fin_inter_open_open
moreover {
}
}
fix \( S \)
assume \( S\in \text{range}(f) \)
with rr have \( S\in \bigcup (QQN) \)
then have \( \exists B\in (QQN).\ S \in B \) using Union_iff
then obtain \( B \) where \( B\in (QQN) \), \( S\in B \)
then have \( \exists rr\in N.\ \langle rr,B\rangle \in QQ \) unfolding image_def
then have \( \exists rr\in N.\ B=\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=rr\}\} \)
with \( S\in B \) obtain \( rr \) where \( \langle S,rr\rangle \in U \)
then have \( x\in S \)
with \( \text{range}(f)\neq 0 \) have \( x\in \bigcap \text{range}(f) \)
moreover {
fix \( y \)
assume \( y\in (\bigcup N)\cap (\bigcap \text{range}(f)) \)
then have reg: \( (\forall S\in \text{range}(f).\ y\in S)\wedge (\exists t\in N.\ y\in t) \)
then obtain \( t \) where \( t\in N \), \( y\in t \)
then have \( \langle t, \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=t\}\}\rangle \in QQ \)
then have \( ft\in \text{range}(f) \) using apply_rangeI, ffun
with reg have yft: \( y\in ft \)
with \( t\in N \), fPI(2) have \( ft\in QQt \)
with \( t\in N \) have \( ft\in \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=t\}\} \) using apply_equality, QQPi
then have \( \langle ft,t\rangle \in U \)
then have \( ft\cap t=0 \)
with \( y\in t \), yft have \( False \)
then have \( (\bigcup N)\cap (\bigcap \text{range}(f))=0 \)
moreover note NN
ultimately have \( thesis \)
A Hausdorff space separates compact spaces from other compact spaces.
theorem (in topology0) T2_compact_compact:
assumes \( T\text{ is }T_2 \), \( A\text{ is compact in }T \), \( B\text{ is compact in }T \), \( A\cap B=0 \)
shows \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge B\subseteq V \wedge U\cap V=0 \)proof{
}
assume \( B=0 \)
then have \( A\subseteq \bigcup T\wedge B\subseteq 0\wedge ((\bigcup T)\cap 0=0) \) using assms(2) unfolding IsCompact_def
moreover
have \( 0\in T \) using empty_open, topSpaceAssum
moreover have \( \bigcup T\in T \) using topSpaceAssum unfolding IsATopology_def
ultimately have \( thesis \)
moreover {
}
}
}
}
}
ultimately show \( thesis \)
qed
assume noEmpty: \( B\neq 0 \)
let \( U = \{\langle U,V\rangle \in T\times T.\ A\subseteq U \wedge U\cap V=0\} \)
{
fix \( y \)
assume \( y\in B \)
then have \( y\in \bigcup T \) using assms(3) unfolding IsCompact_def
with \( y\in B \) have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge y\in V \wedge U\cap V=0 \) using T2_compact_point, assms(1,2,4)
then have \( \exists \langle U,V\rangle \in U.\ y\in V \)
then have \( \forall y\in B.\ \exists \langle U,V\rangle \in U.\ y\in V \)
then have \( B\subseteq \bigcup \{\text{snd}(B).\ B\in U\} \)
moreover
have \( \{\text{snd}(B).\ B\in U\}\in Pow(T) \)
ultimately have \( \exists N\in \text{FinPow}(\{\text{snd}(B).\ B\in U\}).\ B\subseteq \bigcup N \) using assms(3) unfolding IsCompact_def
then obtain \( N \) where ss: \( N\in \text{FinPow}(\{\text{snd}(B).\ B\in U\}) \), \( B\subseteq \bigcup N \)
with \( \{\text{snd}(B).\ B\in U\}\in Pow(T) \) have \( B\subseteq \bigcup N \), \( N\in Pow(T) \) unfolding FinPow_def
then have NN: \( B\subseteq \bigcup N \), \( \bigcup N\in T \) using topSpaceAssum unfolding IsATopology_def
from ss have \( Finite(N) \), \( N\subseteq \{\text{snd}(B).\ B\in U\} \) unfolding FinPow_def
then obtain \( n \) where \( n\in nat \), \( N\approx n \) unfolding Finite_def
then have \( N\preceq n \) using eqpoll_imp_lepoll
from noEmpty, \( B\subseteq \bigcup N \) have NnoEmpty: \( N\neq 0 \)
let \( QQ = \{\langle n,\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\rangle .\ n\in N\} \)
have QQPi: \( QQ:N\rightarrow \{\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}.\ n\in N\} \) unfolding Pi_def, function_def, domain_def
{
fix \( n \)
assume \( n\in N \)
with \( N\subseteq \{\text{snd}(B).\ B\in U\} \) obtain \( B \) where \( n=\text{snd}(B) \), \( B\in U \)
then have \( \text{fst}(B)\in \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\} \)
then have \( \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\neq 0 \)
moreover
from \( n\in N \) have \( \langle n,\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\}\rangle \in QQ \)
with QQPi have \( QQn=\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=n\}\} \) using apply_equality
ultimately have \( QQn\neq 0 \)
then have \( \forall n\in N.\ QQn\neq 0 \)
with \( n\in nat \), \( N\preceq n \) have \( \exists f.\ f\in \text{Pi}(N,\lambda t.\ QQt) \wedge (\forall t\in N.\ ft\in QQt) \) using finite_choice unfolding AxiomCardinalChoiceGen_def
then obtain \( f \) where fPI: \( f\in \text{Pi}(N,\lambda t.\ QQt) \), \( (\forall t\in N.\ ft\in QQt) \)
from NnoEmpty obtain \( q \) where q: \( q:N \)
with fPI(1) have \( fq\in \text{range}(f) \) using apply_rangeI
then have \( \text{range}(f)\neq 0 \)
{
fix \( t \)
assume \( t\in N \)
then have \( ft\in QQt \) using fPI(2)
with \( t\in N \) have \( ft\in \bigcup (QQN) \), \( QQt\subseteq \bigcup (QQN) \) using func_imagedef, QQPi
then have reg: \( \forall t\in N.\ ft\in \bigcup (QQN) \), \( \forall t\in N.\ QQt\subseteq \bigcup (QQN) \)
{
fix \( tt \)
assume \( tt\in f \)
with fPI(1) have \( tt\in Sigma(N, ()(QQ)) \) unfolding Pi_def
then have \( tt\in (\bigcup xa\in N.\ \bigcup y\in QQxa.\ \{\langle xa,y\rangle \}) \) unfolding Sigma_def
then obtain \( xa \) \( y \) where \( xa\in N \), \( y\in QQxa \), \( tt=\langle xa,y\rangle \)
with reg(2) have \( y\in \bigcup (QQN) \)
with \( tt=\langle xa,y\rangle \), \( xa\in N \) have \( tt\in (\bigcup xa\in N.\ \bigcup y\in \bigcup (QQN).\ \{\langle xa,y\rangle \}) \)
then have \( tt\in N\times (\bigcup (QQN)) \) unfolding Sigma_def
then have ffun: \( f:N\rightarrow \bigcup (QQN) \) using fPI(1) unfolding Pi_def
then have \( f\in \text{surj}(N,\text{range}(f)) \) using fun_is_surj
with \( N\preceq n \), \( n\in nat \) have \( \text{range}(f)\preceq N \) using surj_fun_inv_2, nat_into_Ord
with \( N\preceq n \) have \( \text{range}(f)\preceq n \) using lepoll_trans
with \( n\in nat \) have \( Finite(\text{range}(f)) \) using n_lesspoll_nat, lesspoll_nat_is_Finite, lesspoll_trans1
moreover
from ffun have rr: \( \text{range}(f)\subseteq \bigcup (QQN) \) unfolding Pi_def
then have \( \text{range}(f)\subseteq T \)
ultimately have \( \text{range}(f)\in \text{FinPow}(T) \) unfolding FinPow_def
with \( \text{range}(f)\neq 0 \) have \( \bigcap \text{range}(f)\in T \) using fin_inter_open_open
moreover {
}
}
fix \( S \)
assume \( S\in \text{range}(f) \)
with rr have \( S\in \bigcup (QQN) \)
then have \( \exists B\in (QQN).\ S \in B \) using Union_iff
then obtain \( B \) where \( B\in (QQN) \), \( S\in B \)
then have \( \exists rr\in N.\ \langle rr,B\rangle \in QQ \) unfolding image_def
then have \( \exists rr\in N.\ B=\{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=rr\}\} \)
with \( S\in B \) obtain \( rr \) where \( \langle S,rr\rangle \in U \)
then have \( A\subseteq S \)
with \( \text{range}(f)\neq 0 \) have \( A\subseteq \bigcap \text{range}(f) \)
moreover {
fix \( y \)
assume \( y\in (\bigcup N)\cap (\bigcap \text{range}(f)) \)
then have reg: \( (\forall S\in \text{range}(f).\ y\in S)\wedge (\exists t\in N.\ y\in t) \)
then obtain \( t \) where \( t\in N \), \( y\in t \)
then have \( \langle t, \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=t\}\}\rangle \in QQ \)
then have \( ft\in \text{range}(f) \) using apply_rangeI, ffun
with reg have yft: \( y\in ft \)
with \( t\in N \), fPI(2) have \( ft\in QQt \)
with \( t\in N \) have \( ft\in \{\text{fst}(B).\ B\in \{A\in U.\ \text{snd}(A)=t\}\} \) using apply_equality, QQPi
then have \( \langle ft,t\rangle \in U \)
then have \( ft\cap t=0 \)
with \( y\in t \), yft have \( False \)
then have \( (\bigcap \text{range}(f))\cap (\bigcup N)=0 \)
moreover note NN
ultimately have \( thesis \)
A compact Hausdorff space is normal.
corollary (in topology0) T2_compact_is_normal:
assumes \( T\text{ is }T_2 \), \( (\bigcup T)\text{ is compact in }T \)
shows \( T\text{ is normal } \)proof from assms(2) have car_nat: \( (\bigcup T)\text{ is compact of cardinal }nat\{in\}T \) using Compact_is_card_nat
{
fix \( A \) \( B \)
assume \( A\text{ is closed in }T \), \( B\text{ is closed in }T \), \( A\cap B=0 \)
then have com: \( ((\bigcup T)\cap A)\text{ is compact of cardinal }nat\{in\}T \), \( ((\bigcup T)\cap B)\text{ is compact of cardinal }nat\{in\}T \) using compact_closed, car_nat
from \( A\text{ is closed in }T \), \( B\text{ is closed in }T \) have \( (\bigcup T)\cap A=A \), \( (\bigcup T)\cap B=B \) unfolding IsClosed_def
with com have \( A\text{ is compact of cardinal }nat\{in\}T \), \( B\text{ is compact of cardinal }nat\{in\}T \)
then have \( A\text{ is compact in }T \), \( B\text{ is compact in }T \) using Compact_is_card_nat
with \( A\cap B=0 \) have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge B\subseteq V \wedge U\cap V=0 \) using T2_compact_compact, assms(1)
then have I: \( \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)) \)
then show \( thesis \) unfolding IsNormal_def
qed
Hereditability
A topological property is hereditary if whenever a space has it, every subspace also has it.
A topological property is hereditary if every subspace inherits it.
definition
\( P \text{ is hereditary } \equiv \forall T.\ T\text{ is a topology } \wedge P(T) \longrightarrow (\forall A\in Pow(\bigcup T).\ P(T\text{ restricted to }A)) \)
A subspace of a subspace equals the corresponding direct subspace of the original topology.
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 \)proof from assms have S: \( \forall S\in T.\ A\cap (B\cap S)=A\cap S \)
then show \( T \text{ restricted to } A \subseteq T \text{ restricted to } B \text{ restricted to } A \) unfolding RestrictedTo_def
from S show \( T \text{ restricted to } B \text{ restricted to } A \subseteq T \text{ restricted to } A \) unfolding RestrictedTo_def
qed
The separation properties \(T_0\), \(T_1\), \(T_2\) y \(T_3\) are hereditary.
theorem regular_here:
assumes \( T\text{ is regular } \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is regular } \)proof{
}
}
fix \( C \)
assume A: \( C\text{ is closed in }(T\text{ restricted to }A) \)
{
fix \( y \)
assume \( y\in \bigcup (T\text{ restricted to }A) \), \( y\notin C \)
with A have \( (\bigcup (T\text{ restricted to }A))-C\in (T\text{ restricted to }A) \), \( C\subseteq \bigcup (T\text{ restricted to }A) \), \( y\in \bigcup (T\text{ restricted to }A) \), \( y\notin C \) unfolding IsClosed_def
moreover
from this, assms(2) have \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
ultimately have \( A-C\in T\text{ restricted to }A \), \( y\in A \), \( y\notin C \), \( C\in Pow(A) \)
then obtain \( S \) where \( S\in T \), \( A\cap S=A-C \), \( y\in A \), \( y\notin C \) unfolding RestrictedTo_def
then have \( y\in A-C \), \( A\cap S=A-C \)
with \( C\in Pow(A) \) have \( y\in A\cap S \), \( C=A-A\cap S \)
then have \( y\in S \), \( C=A-S \)
with assms(2) have \( y\in S \), \( C\subseteq \bigcup T-S \)
moreover
from \( S\in T \) have \( \bigcup T-(\bigcup T-S)=S \)
moreover from this, \( S\in T \) have \( (\bigcup T-S) \text{ is closed in }T \) using IsClosed_def
ultimately have \( y\in \bigcup T-(\bigcup T-S) \), \( (\bigcup T-S) \text{ is closed in }T \)
with assms(1) have \( \forall y\in \bigcup T-(\bigcup T-S).\ \exists U\in T.\ \exists V\in T.\ (\bigcup T-S)\subseteq U\wedge y\in V\wedge U\cap V=0 \) unfolding IsRegular_def
with \( y\in \bigcup T-(\bigcup T-S) \) have \( \exists U\in T.\ \exists V\in T.\ (\bigcup T-S)\subseteq U\wedge y\in V\wedge U\cap V=0 \)
then obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( \bigcup T-S\subseteq U \), \( y\in V \), \( U\cap V=0 \)
with \( C\subseteq \bigcup T-S \) have \( A\cap U\in (T\text{ restricted to }A) \), \( A\cap V\in (T\text{ restricted to }A) \), \( C\subseteq U \), \( y\in V \), \( (A\cap U)\cap (A\cap V)=0 \) unfolding RestrictedTo_def
moreover
from this, \( C\in Pow(A) \), \( y\in A \) have \( C\subseteq A\cap U \), \( y\in A\cap V \)
ultimately have \( \exists U\in (T\text{ restricted to }A).\ \exists V\in (T\text{ restricted to }A).\ C\subseteq U\wedge y\in V\wedge U\cap V=0 \)
then have \( \forall x\in \bigcup (T\text{ restricted to }A)-C.\ \exists U\in (T\text{ restricted to }A).\ \exists V\in (T\text{ restricted to }A).\ C\subseteq U\wedge x\in V\wedge U\cap V=0 \)
then have \( \forall C.\ C\text{ is closed in }(T\text{ restricted to }A) \longrightarrow (\forall x\in \bigcup (T\text{ restricted to }A)-C.\ \exists U\in (T\text{ restricted to }A).\ \exists V\in (T\text{ restricted to }A).\ C\subseteq U\wedge x\in V\wedge U\cap V=0) \)
then show \( thesis \) using IsRegular_def
qed
Regularity is a hereditary property.
corollary here_regular:
shows \( IsRegular \text{ is hereditary } \) using regular_here, IsHer_defThe \(T_1\) axiom is inherited by subspaces.
theorem T1_here:
assumes \( T\text{ is }T_1 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_1 \)proof from assms(2) have un: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
{
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \), \( x\neq y \)
with \( A\in Pow(\bigcup T) \) have \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
then have \( \exists U\in T.\ x\in U\wedge y\notin U \) using assms(1), isT1_def
then obtain \( U \) where \( U\in T \), \( x\in U \), \( y\notin U \)
with \( x\in A \) have \( A\cap U\in (T\text{ restricted to }A) \), \( x\in A\cap U \), \( y\notin A\cap U \) unfolding RestrictedTo_def
then have \( \exists U\in (T\text{ restricted to }A).\ x\in U\wedge y\notin U \)
with un have \( \forall x y.\ x\in \bigcup (T\text{ restricted to }A) \wedge y\in \bigcup (T\text{ restricted to }A) \wedge x\neq y \longrightarrow (\exists U\in (T\text{ restricted to }A).\ x\in U\wedge y\notin U) \)
then show \( thesis \) using isT1_def
qed
The \(T_1\) property is hereditary.
corollary here_T1:
shows \( isT1 \text{ is hereditary } \) using T1_here, IsHer_defThe conjunction of two hereditary properties is hereditary.
lemma here_and:
assumes \( P \text{ is hereditary } \), \( Q \text{ is hereditary } \)
shows \( (\lambda T.\ P(T) \wedge Q(T)) \text{ is hereditary } \) using assms unfolding IsHer_defThe \(T_3\) property is hereditary.
corollary here_T3:
shows \( isT3 \text{ is hereditary } \) using here_and, here_T1, here_regular, T3_def_alt unfolding IsHer_defThe \(T_2\) axiom is inherited by subspaces.
lemma T2_here:
assumes \( T\text{ is }T_2 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_2 \)proof from assms(2) have un: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
{
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \), \( x\neq y \)
with \( A\in Pow(\bigcup T) \) have \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
then have \( \exists U\in T.\ \exists V\in T.\ x\in U\wedge y\in V\wedge U\cap V=0 \) using assms(1), isT2_def
then obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( x\in U \), \( y\in V \), \( U\cap V=0 \)
with \( x\in A \), \( y\in A \) have \( A\cap U\in (T\text{ restricted to }A) \), \( A\cap V\in (T\text{ restricted to }A) \), \( x\in A\cap U \), \( y\in A\cap V \), \( (A\cap U)\cap (A\cap V)=0 \) unfolding RestrictedTo_def
then have \( \exists U\in (T\text{ restricted to }A).\ \exists V\in (T\text{ restricted to }A).\ x\in U\wedge y\in V\wedge U\cap V=0 \) unfolding Bex_def
with un have \( \forall x y.\ x\in \bigcup (T\text{ restricted to }A) \wedge y\in \bigcup (T\text{ restricted to }A) \wedge x\neq y \longrightarrow (\exists U\in (T\text{ restricted to }A).\ \exists V\in (T\text{ restricted to }A).\ x\in U\wedge y\in V\wedge U\cap V=0) \)
then show \( thesis \) using isT2_def
qed
The \(T_2\) property is hereditary.
corollary here_T2:
shows \( isT2 \text{ is hereditary } \) using T2_here, IsHer_defThe \(T_0\) axiom is inherited by subspaces.
lemma T0_here:
assumes \( T\text{ is }T_0 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_0 \)proof from assms(2) have un: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
{
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \), \( x\neq y \)
with \( A\in Pow(\bigcup T) \) have \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
then have \( \exists U\in T.\ (x\in U\wedge y\notin U)\vee (y\in U\wedge x\notin U) \) using assms(1), isT0_def
then obtain \( U \) where \( U\in T \), \( (x\in U\wedge y\notin U)\vee (y\in U\wedge x\notin U) \)
with \( x\in A \), \( y\in A \) have \( A\cap U\in (T\text{ restricted to }A) \), \( (x\in A\cap U\wedge y\notin A\cap U)\vee (y\in A\cap U\wedge x\notin A\cap U) \) unfolding RestrictedTo_def
then have \( \exists U\in (T\text{ restricted to }A).\ (x\in U\wedge y\notin U)\vee (y\in U\wedge x\notin U) \) unfolding Bex_def
with un have \( \forall x y.\ x\in \bigcup (T\text{ restricted to }A) \wedge y\in \bigcup (T\text{ restricted to }A) \wedge x\neq y \longrightarrow (\exists U\in (T\text{ restricted to }A).\ (x\in U\wedge y\notin U)\vee (y\in U\wedge x\notin U)) \)
then show \( thesis \) using isT0_def
qed
The \(T_0\) property is hereditary.
corollary here_T0:
shows \( isT0 \text{ is hereditary } \) using T0_here, IsHer_defSpectrum and anti-properties
The spectrum of a topological property is a class of sets such that all topologies defined over that set have that property.
The spectrum of a property gives us the list of sets for which the property doesn't give any topological information. Being in the spectrum of a topological property is an invariant in the category of sets and function; mening that equipollent sets are in the same spectra.
definition
\( \text{Spec}(K,P) \equiv \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx K) \longrightarrow P(T)) \)
Equipollent sets lie in the same spectra.
lemma equipollent_spect:
assumes \( A\approx B \), \( B \text{ is in the spectrum of } P \)
shows \( A \text{ is in the spectrum of } P \)proof from assms(2) have \( \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx B) \longrightarrow P(T)) \) using Spec_def
then have \( \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx A) \longrightarrow P(T)) \) using eqpoll_trans, assms(1)
then show \( thesis \) using Spec_def
qed
A set is in the spectrum of a property if and only if any equipollent set is.
theorem eqpoll_iff_spec:
assumes \( A\approx B \)
shows \( (B \text{ is in the spectrum of } P) \longleftrightarrow (A \text{ is in the spectrum of } P) \)proof assume \( B \text{ is in the spectrum of } P \)
with assms, equipollent_spect show \( A \text{ is in the spectrum of } P \)
next
assume \( A \text{ is in the spectrum of } P \)
moreover
qed
from assms have \( B\approx A \) using eqpoll_sym
ultimately show \( B \text{ is in the spectrum of } P \) using equipollent_spect
From the previous statement, we see that the spectrum could be formed only by representative of clases of sets. If \emph{AC} holds, this means that the spectrum can be taken as a set or class of cardinal numbers.
Here is an example of the spectrum. The proof lies in the indiscrite filter \( \{A\} \) that can be build for any set. In this proof, we see that without choice, there is no way to define the sepctrum of a property with cardinals because if a set is not comparable with any ordinal, its cardinal is defined as 0 without the set being empty.
theorem T4_spectrum:
shows \( (A \text{ is in the spectrum of } isT4) \longleftrightarrow A \preceq 1 \)proof assume \( A \text{ is in the spectrum of } isT4 \)
then have reg: \( \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx A) \longrightarrow (T \{is T_4\})) \) using Spec_def
{
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
then have III: \( x\in \bigcup \{A\} \)
from this have II: \( \{A\} \text{ is a filter on }\bigcup \{A\} \) using IsFilter_def
from this have \( (\{A\}\cup \{0\}) \text{ is a topology } \wedge \bigcup (\{A\}\cup \{0\})=A \) using top_of_filter
then have top: \( (\{A\}\cup \{0\}) \text{ is a topology } \), \( \bigcup (\{A\}\cup \{0\})\approx A \) using eqpoll_refl
then have \( (\{A\}\cup \{0\}) \{is T_4\} \) using reg
then have I: \( (\{A\}\cup \{0\}) \text{ is }T_2 \) using T3_is_T2, T4_is_T3, topology0_def, top
from I, II, III have \( \bigcup \{A\}=\{x\} \) by (rule filter_T2_imp_card1 )
then have \( A=\{x\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
moreover
have \( A=0 \longrightarrow A\approx 0 \)
ultimately have \( A\approx 1\vee A\approx 0 \)
then show \( A\preceq 1 \) using empty_lepollI, eqpoll_imp_lepoll, eq_lepoll_trans
next
assume \( A\preceq 1 \)
have \( A=0\vee A\neq 0 \)
then obtain \( E \) where \( A=0\vee E\in A \)
then have \( A\approx 0\vee E\in A \)
with \( A\preceq 1 \) have \( A\approx 0\vee A=\{E\} \) using lepoll_1_is_sing
then have \( A\approx 0\vee A\approx 1 \) using singleton_eqpoll_1
{
fix \( T \)
assume AS: \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( A\approx 0 \)
with AS have \( T\text{ is a topology } \) and empty: \( \bigcup T=0 \) using eqpoll_trans, eqpoll_0_is_0
then have \( T\text{ is }T_2 \) using isT2_def
then have \( T\text{ is }T_1 \) using T2_is_T1
from empty have rr: \( \forall A.\ A\text{ is closed in }T \longrightarrow A=0 \) using IsClosed_def
have \( \exists U\in T.\ \exists V\in T.\ 0\subseteq U\wedge 0\subseteq V\wedge U\cap V=0 \) using empty_open, AS(1)
with rr have \( \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)) \)
then have \( T\text{ is normal } \) using IsNormal_def
with \( T\text{ is }T_1 \) have \( T\{is T_4\} \) using isT4_def
moreover {
}
}
}
moreover
assume \( A\approx 1 \)
with AS have \( T\text{ is a topology } \) and NONempty: \( \bigcup T\approx 1 \) using eqpoll_trans
then have \( \bigcup T\preceq 1 \) using eqpoll_imp_lepoll
moreover {
}
{
assume \( \bigcup T=0 \)
then have \( 0\approx \bigcup T \)
with NONempty have \( 0\approx 1 \) using eqpoll_trans
then have \( 0=1 \) using eqpoll_0_is_0, eqpoll_sym
then have \( False \)
then have \( \bigcup T\neq 0 \)
then obtain \( R \) where \( R\in \bigcup T \)
ultimately have \( \bigcup T=\{R\} \) using lepoll_1_is_sing
fix \( x \) \( y \)
assume \( x\text{ is closed in }T \), \( y\text{ is closed in }T \), \( x\cap y=0 \)
then have \( x\subseteq \bigcup T \), \( y\subseteq \bigcup T \) using IsClosed_def
with \( x\cap y=0 \), \( \bigcup T=\{R\} \) have \( x=0\vee y=0 \)
{
assume \( x=0 \)
with \( y\subseteq \bigcup T \) have \( x\subseteq 0 \), \( y\subseteq \bigcup T \)
moreover
have \( 0\in T \), \( \bigcup T\in T \) using AS(1), IsATopology_def, empty_open
ultimately have \( \exists U\in T.\ \exists V\in T.\ x\subseteq U\wedge y\subseteq V\wedge U\cap V=0 \)
moreover {
}
ultimately have \( (\exists U\in T.\ \exists V\in T.\ x \subseteq U \wedge y \subseteq V \wedge U \cap V = 0) \)
assume \( x\neq 0 \)
with \( x=0\vee y=0 \) have \( y=0 \)
with \( x\subseteq \bigcup T \) have \( x\subseteq \bigcup T \), \( y\subseteq 0 \)
moreover
have \( 0\in T \), \( \bigcup T\in T \) using AS(1), IsATopology_def, empty_open
ultimately have \( \exists U\in T.\ \exists V\in T.\ x\subseteq U\wedge y\subseteq V\wedge U\cap V=0 \)
then have \( T\text{ is normal } \) using IsNormal_def
moreover {
}
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
with \( \bigcup T=\{R\} \) have \( False \)
then have \( \exists U\in T.\ x\in U\wedge y\notin U \)
then have \( T\text{ is }T_1 \) using isT1_def
ultimately have \( T\{is T_4\} \) using isT4_def
note \( A\approx 0\vee A\approx 1 \)
ultimately have \( T\{is T_4\} \)
then have \( \forall T.\ (T\text{ is a topology } \wedge \bigcup T \approx A) \longrightarrow (T\{is T_4\}) \)
then show \( A \text{ is in the spectrum of } isT4 \) using Spec_def
qed
If the topological properties are related, then so are the spectra.
lemma P_imp_Q_spec_inv:
assumes \( \forall T.\ T\text{ is a topology } \longrightarrow (Q(T) \longrightarrow P(T)) \), \( A \text{ is in the spectrum of } Q \)
shows \( A \text{ is in the spectrum of } P \)proof from assms(2) have \( \forall T.\ T\text{ is a topology } \wedge \bigcup T \approx A \longrightarrow Q(T) \) using Spec_def
with assms(1) have \( \forall T.\ T\text{ is a topology } \wedge \bigcup T \approx A \longrightarrow P(T) \)
then show \( thesis \) using Spec_def
qed
Since we already now the spectrum of \(T_4\); if we now the spectrum of \(T_0\), it should be easier to compute the spectrum of \(T_1\), \(T_2\) and \(T_3\).
theorem T0_spectrum:
shows \( (A \text{ is in the spectrum of } isT0) \longleftrightarrow A \preceq 1 \)proof assume \( A \text{ is in the spectrum of } isT0 \)
then have reg: \( \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx A) \longrightarrow (T \text{ is }T_0)) \) using Spec_def
{
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
then have \( x\in \bigcup \{A\} \)
from this have \( \{A\} \text{ is a filter on }\bigcup \{A\} \) using IsFilter_def
from this have \( (\{A\}\cup \{0\}) \text{ is a topology } \wedge \bigcup (\{A\}\cup \{0\})=A \) using top_of_filter
then have \( (\{A\}\cup \{0\}) \text{ is a topology } \wedge \bigcup (\{A\}\cup \{0\})\approx A \) using eqpoll_refl
then have \( (\{A\}\cup \{0\}) \text{ is }T_0 \) using reg
{
fix \( y \)
assume \( y\in A \), \( x\neq y \)
with \( (\{A\}\cup \{0\}) \text{ is }T_0 \) obtain \( U \) where \( U\in \{A\}\cup \{0\} \) and dis: \( (x \in U \wedge y \notin U) \vee (y \in U \wedge x \notin U) \) using isT0_def
then have \( U=A \)
with dis, \( y\in A \), \( x\in \bigcup \{A\} \) have \( False \)
then have \( \forall y\in A.\ y=x \)
with \( x\in \bigcup \{A\} \) have \( A=\{x\} \)
then have \( A\approx 1 \) using singleton_eqpoll_1
moreover
have \( A=0 \longrightarrow A\approx 0 \)
ultimately have \( A\approx 1\vee A\approx 0 \)
then show \( A\preceq 1 \) using empty_lepollI, eqpoll_imp_lepoll, eq_lepoll_trans
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \)
then have \( (T\{is T_4\})\longrightarrow (T\text{ is }T_0) \) using T4_is_T3, T3_is_T2, T2_is_T1, T1_is_T0, topology0_def
then have \( \forall T.\ T\text{ is a topology } \longrightarrow ((T\{is T_4\})\longrightarrow (T\text{ is }T_0)) \)
then have \( (A \text{ is in the spectrum of } isT4) \longrightarrow (A \text{ is in the spectrum of } isT0) \) using P_imp_Q_spec_inv
with \( A\preceq 1 \) show \( (A \text{ is in the spectrum of } isT0) \) using T4_spectrum
qed
The spectrum of \(T_1\) consists exactly of sets of cardinality at most \(1\).
theorem T1_spectrum:
shows \( (A \text{ is in the spectrum of } isT1) \longleftrightarrow A \preceq 1 \)proof have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_1) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT1 \) using P_imp_Q_spec_inv
with T2_is_T1, T3_is_T2, topology0.T4_is_T3 have \( (A \text{ is in the spectrum of } isT4) \longrightarrow (A \text{ is in the spectrum of } isT1) \) using topology0_def
moreover
qed
have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\text{ is }T_1 \longrightarrow T \text{ is }T_0) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT1 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT0 \) using P_imp_Q_spec_inv
then have \( (A \text{ is in the spectrum of } isT1) \longrightarrow (A \text{ is in the spectrum of }isT0) \) using P_imp_Q_spec_inv, T1_is_T0
moreover note T0_spectrum, T4_spectrum
ultimately show \( thesis \)
The spectrum of \(T_2\) consists exactly of sets of cardinality at most \(1\).
theorem T2_spectrum:
shows \( (A \text{ is in the spectrum of } isT2) \longleftrightarrow A \preceq 1 \)proof have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_2) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT2 \) using P_imp_Q_spec_inv
with T3_is_T2, topology0.T4_is_T3 have \( (A \text{ is in the spectrum of } isT4) \longrightarrow (A \text{ is in the spectrum of } isT2) \) using topology0_def
moreover
qed
have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\text{ is }T_2 \longrightarrow T \text{ is }T_1) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT2 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT1 \) using P_imp_Q_spec_inv
with T2_is_T1 have \( (A \text{ is in the spectrum of } isT2) \longrightarrow (A \text{ is in the spectrum of }isT1) \)
moreover note T1_spectrum, T4_spectrum
ultimately show \( thesis \)
The spectrum of \(T_3\) consists exactly of sets of cardinality at most \(1\).
theorem T3_spectrum:
shows \( (A \text{ is in the spectrum of } isT3) \longleftrightarrow A \preceq 1 \)proof have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_3) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT3 \) using P_imp_Q_spec_inv
with topology0.T4_is_T3 have \( (A \text{ is in the spectrum of } isT4) \longrightarrow (A \text{ is in the spectrum of } isT3) \) using topology0_def
moreover
qed
have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\text{ is }T_3 \longrightarrow T \text{ is }T_2) \Longrightarrow \)
\( A \text{ is in the spectrum of } isT3 \Longrightarrow \)
\( A \text{ is in the spectrum of } isT2 \) using P_imp_Q_spec_inv
with T3_is_T2 have \( (A \text{ is in the spectrum of } isT3) \longrightarrow (A \text{ is in the spectrum of }isT2) \) using topology0_def
moreover note T2_spectrum, T4_spectrum
ultimately show \( thesis \)
The spectrum of compactness is exactly the class of finite sets.
theorem compact_spectrum:
shows \( (A \text{ is in the spectrum of } (\lambda T.\ (\bigcup T) \text{ is compact in }T)) \longleftrightarrow Finite(A) \)proof assume \( A \text{ is in the spectrum of } (\lambda T.\ (\bigcup T) \text{ is compact in }T) \)
then have reg: \( \forall T.\ T\text{ is a topology } \wedge \bigcup T\approx A \longrightarrow ((\bigcup T) \text{ is compact in }T) \) using Spec_def
have \( Pow(A)\text{ is a topology } \wedge \bigcup Pow(A)=A \) using Pow_is_top
then have \( Pow(A)\text{ is a topology } \wedge \bigcup Pow(A)\approx A \) using eqpoll_refl
with reg have \( A\text{ is compact in }Pow(A) \)
moreover
{
have \( \{\{x\}.\ x\in A\}\in Pow(Pow(A)) \)
moreover have \( \bigcup \{\{x\}.\ x\in A\}=A \)
ultimately have \( \exists N\in \text{FinPow}(\{\{x\}.\ x\in A\}).\ A\subseteq \bigcup N \) using IsCompact_def
then obtain \( N \) where \( N\in \text{FinPow}(\{\{x\}.\ x\in A\}) \), \( A\subseteq \bigcup N \)
then have \( N\subseteq \{\{x\}.\ x\in A\} \), \( Finite(N) \), \( A\subseteq \bigcup N \) using FinPow_def
fix \( t \)
assume \( t\in \{\{x\}.\ x\in A\} \)
then obtain \( x \) where \( x\in A \), \( t=\{x\} \)
with \( A\subseteq \bigcup N \) have \( x\in \bigcup N \)
then obtain \( B \) where \( B\in N \), \( x\in B \)
with \( N\subseteq \{\{x\}.\ x\in A\} \) have \( B=\{x\} \)
with \( t=\{x\} \), \( B\in N \) have \( t\in N \)
with \( N\subseteq \{\{x\}.\ x\in A\} \) have \( N=\{\{x\}.\ x\in A\} \)
with \( Finite(N) \) have \( Finite(\{\{x\}.\ x\in A\}) \)
let \( B = \{\langle x,\{x\}\rangle .\ x\in A\} \)
have \( B:A\rightarrow \{\{x\}.\ x\in A\} \) unfolding Pi_def, function_def
then have \( B:\text{bij}(A,\{\{x\}.\ x\in A\}) \) unfolding bij_def, inj_def, surj_def using apply_equality
then have \( A\approx \{\{x\}.\ x\in A\} \) using eqpoll_def
with \( Finite(\{\{x\}.\ x\in A\}) \) show \( Finite(A) \) using eqpoll_imp_Finite_iff
next
assume \( Finite(A) \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
with \( Finite(A) \) have \( Finite(\bigcup T) \) using eqpoll_imp_Finite_iff
then have \( Finite(Pow(\bigcup T)) \) using Finite_Pow
moreover
{
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( Finite(T) \) using subset_Finite
fix \( M \)
assume \( M\in Pow(T) \), \( \bigcup T\subseteq \bigcup M \)
with \( Finite(T) \) have \( Finite(M) \) using subset_Finite
with \( \bigcup T\subseteq \bigcup M \) have \( \exists N\in \text{FinPow}(M).\ \bigcup T\subseteq \bigcup N \) using FinPow_def
then have \( (\bigcup T)\text{ is compact in }T \) unfolding IsCompact_def
then show \( A \text{ is in the spectrum of } (\lambda T.\ (\bigcup T) \text{ is compact in }T) \) using Spec_def
qed
It is, at least for some people, surprising that the spectrum of some properties cannot be completely determined in \emph{ZF}.
theorem compactK_spectrum:
assumes \( \text{ the axiom of }K\text{ choice holds for subsets }(Pow(K)) \), \( \text{Card}(K) \)
shows \( (A \text{ is in the spectrum of } (\lambda T.\ ((\bigcup T)\text{ is compact of cardinal } \text{csucc}(K)\{in\}T))) \longleftrightarrow (A\preceq K) \)proof assume \( A \text{ is in the spectrum of } (\lambda T.\ ((\bigcup T)\text{ is compact of cardinal } \text{csucc}(K)\{in\}T)) \)
then have reg: \( \forall T.\ T\text{ is a topology }\wedge \bigcup T\approx A \longrightarrow ((\bigcup T)\text{ is compact of cardinal } \text{csucc}(K)\{in\}T) \) using Spec_def
from reg have \( Pow(A)\text{ is a topology }\wedge \bigcup Pow(A)\approx A \longrightarrow ((\bigcup Pow(A))\text{ is compact of cardinal } \text{csucc}(K)\{in\}Pow(A)) \)
then have \( A\text{ is compact of cardinal } \text{csucc}(K)\text{ in }Pow(A) \) using Pow_is_top
then have \( \forall M\in Pow(Pow(A)).\ A\subseteq \bigcup M \longrightarrow (\exists N\in Pow(M).\ A\subseteq \bigcup N \wedge N\prec \text{csucc}(K)) \) unfolding IsCompactOfCard_def
moreover
{
have \( \{\{x\}.\ x\in A\}\in Pow(Pow(A)) \)
moreover have \( A=\bigcup \{\{x\}.\ x\in A\} \)
ultimately have \( \exists N\in Pow(\{\{x\}.\ x\in A\}).\ A\subseteq \bigcup N \wedge N\prec \text{csucc}(K) \)
then obtain \( N \) where \( N\in Pow(\{\{x\}.\ x\in A\}) \), \( A\subseteq \bigcup N \), \( N\prec \text{csucc}(K) \)
then have \( N\subseteq \{\{x\}.\ x\in A\} \), \( N\prec \text{csucc}(K) \), \( A\subseteq \bigcup N \) using FinPow_def
fix \( t \)
assume \( t\in \{\{x\}.\ x\in A\} \)
then obtain \( x \) where \( x\in A \), \( t=\{x\} \)
with \( A\subseteq \bigcup N \) have \( x\in \bigcup N \)
then obtain \( B \) where \( B\in N \), \( x\in B \)
with \( N\subseteq \{\{x\}.\ x\in A\} \) have \( B=\{x\} \)
with \( t=\{x\} \), \( B\in N \) have \( t\in N \)
with \( N\subseteq \{\{x\}.\ x\in A\} \) have \( N=\{\{x\}.\ x\in A\} \)
let \( B = \{\langle x,\{x\}\rangle .\ x\in A\} \)
from \( N=\{\{x\}.\ x\in A\} \) have \( B:A\rightarrow N \) unfolding Pi_def, function_def
with \( N=\{\{x\}.\ x\in A\} \) have \( B:\text{inj}(A,N) \) unfolding inj_def using apply_equality
then have \( A\preceq N \) using lepoll_def
with \( N\prec \text{csucc}(K) \) have \( A\prec \text{csucc}(K) \) using lesspoll_trans1
then show \( A\preceq K \) using Card_less_csucc_eq_le, assms(2)
next
assume \( A\preceq K \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
have \( Pow(\bigcup T)\text{ is a topology } \) using Pow_is_top
{
fix \( B \)
assume AS: \( B\in Pow(\bigcup T) \)
then have \( \{\{i\}.\ i\in B\}\subseteq \{\{i\} .\ i\in \bigcup T\} \)
moreover
have \( B=\bigcup \{\{i\}.\ i\in B\} \)
ultimately have \( \exists S\in Pow(\{\{i\}.\ i\in \bigcup T\}).\ B=\bigcup S \)
then have \( B\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in \bigcup T\})\} \)
moreover {
}
ultimately have base: \( \{\{x\}.\ x\in \bigcup T\} \text{ is a base for }Pow(\bigcup T) \) unfolding IsAbaseFor_def
fix \( B \)
assume AS: \( B\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in \bigcup T\})\} \)
then have \( B\in Pow(\bigcup T) \)
let \( f = \{\langle i,\{i\}\rangle .\ i\in \bigcup T\} \)
have f: \( f:\bigcup T\rightarrow \{\{x\}.\ x\in \bigcup T\} \) using Pi_def, function_def
moreover {
}
}
fix \( w \) \( x \)
assume as: \( w\in \bigcup T \), \( x\in \bigcup T \), \( fw=fx \)
with f have \( fw=\{w\} \), \( fx=\{x\} \) using apply_equality
with as(3) have \( w=x \)
with f have \( f:\text{inj}(\bigcup T,\{\{x\}.\ x\in \bigcup T\}) \) unfolding inj_def
moreover {
fix \( xa \)
assume \( xa\in \{\{x\}.\ x\in \bigcup T\} \)
then obtain \( x \) where \( x\in \bigcup T \), \( xa=\{x\} \)
with f have \( fx=xa \) using apply_equality
with \( x\in \bigcup T \) have \( \exists x\in \bigcup T.\ fx=xa \)
then have \( \forall xa\in \{\{x\}.\ x\in \bigcup T\}.\ \exists x\in \bigcup T.\ fx=xa \)
ultimately have \( f:\text{bij}(\bigcup T,\{\{x\}.\ x\in \bigcup T\}) \) unfolding bij_def, surj_def
then have \( \bigcup T\approx \{\{x\}.\ x\in \bigcup T\} \) using eqpoll_def
then have \( \{\{x\}.\ x\in \bigcup T\}\approx \bigcup T \) using eqpoll_sym
with \( \bigcup T\approx A \) have \( \{\{x\}.\ x\in \bigcup T\}\approx A \) using eqpoll_trans
then have \( \{\{x\}.\ x\in \bigcup T\}\preceq A \) using eqpoll_imp_lepoll
with \( A\preceq K \) have \( \{\{x\}.\ x\in \bigcup T\}\preceq K \) using lepoll_trans
then have \( \{\{x\}.\ x\in \bigcup T\}\prec \text{csucc}(K) \) using assms(2), Card_less_csucc_eq_le
with base have \( Pow(\bigcup T) \text{ is of second type of cardinal }\text{csucc}(K) \) unfolding IsSecondOfCard_def
moreover
from compact_of_cardinal_Q have \( (\text{ the axiom of }K\text{ choice holds for subsets }Pow(K)) \Longrightarrow \)
\( (Pow(\bigcup T) \text{ is of second type of cardinal }\text{csucc}(K)) \Longrightarrow \)
\( (Pow(\bigcup T) \text{ is a topology }) \Longrightarrow \)
\( (\bigcup (Pow(\bigcup T))\text{ is compact of cardinal }\text{csucc}(K) \{in\}(Pow(\bigcup T))) \)
then have \( \text{ the axiom of }K\text{ choice holds for subsets }Pow(K) \Longrightarrow \)
\( (Pow(\bigcup T)) \text{ is of second type of cardinal }\text{csucc}(K) \Longrightarrow \)
\( (Pow(\bigcup T)) \text{ is a topology } \Longrightarrow \)
\( (\bigcup T)\text{ is compact of cardinal }\text{csucc}(K) \{in\}(Pow(\bigcup T)) \)
with calculation, assms(1), \( Pow(\bigcup T)\text{ is a topology } \) have \( (\bigcup T) \text{ is compact of cardinal }\text{csucc}(K)\{in\}Pow(\bigcup T) \)
moreover have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( (\bigcup T) \text{ is compact of cardinal }\text{csucc}(K)\{in\}T \) using compact_coarser
then show \( A \text{ is in the spectrum of } (\lambda T.\ ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(K) \{in\}T)) \) using Spec_def
qed
If the spectrum of \(K\)-compactness equals \(A \lesssim K\), then the \(K\)-choice principle holds.
theorem compactK_spectrum_reverse:
assumes \( \forall A.\ (A \text{ is in the spectrum of } (\lambda T.\ ((\bigcup T)\text{ is compact of cardinal } \text{csucc}(K)\{in\}T))) \longleftrightarrow (A\preceq K) \), \( \text{InfCard}(K) \)
shows \( \text{ the axiom of }K\text{ choice holds for subsets }(Pow(K)) \)proof have \( K\preceq K \) using lepoll_refl
then have \( K \text{ is in the spectrum of } (\lambda T.\ ((\bigcup T)\text{ is compact of cardinal } \text{csucc}(K)\{in\}T)) \) using assms(1)
moreover
qed
have \( Pow(K)\text{ is a topology } \) using Pow_is_top
moreover have \( \bigcup Pow(K)=K \)
then have \( \bigcup Pow(K)\approx K \) using eqpoll_refl
ultimately have \( K \text{ is compact of cardinal } \text{csucc}(K)\{in\}Pow(K) \) using Spec_def
then show \( thesis \) using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ, assms(2)
This last theorem states that if one of the forms of the axiom of choice related to this compactness property fails, then the spectrum will be different. Notice that even for Lindelöf spaces that will happend.
The spectrum gives us the posibility to define what an anti-property means. A space is anti-P if the only subspaces which have the property are the ones in the spectrum of P. This concept tries to put together spaces that are completely opposite to spaces where \( P(T) \).
definition
\( 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) \)
We abbreviate the functional form of the anti-property predicate.
abbreviation
\( ANTI(P) \equiv \lambda T.\ (T\{is anti-\}P) \)
A first, very simple, but very useful result is the following: when the properties are related and the spectra are equal, then the anti-properties are related in the oposite direction.
theorem (in topology0) eq_spect_rev_imp_anti:
assumes \( \forall T.\ T\text{ is a topology } \longrightarrow P(T) \longrightarrow Q(T) \), \( \forall A.\ (A\text{ is in the spectrum of }Q) \longrightarrow (A\text{ is in the spectrum of }P) \) and \( T\{is anti-\}Q \)
shows \( T\{is anti-\}P \)proof{
}
fix \( A \)
assume \( A\in Pow(\bigcup T) \), \( P(T\text{ restricted to }A) \)
with assms(1) have \( Q(T\text{ restricted to }A) \) using Top_1_L4
with assms(3), \( A\in Pow(\bigcup T) \) have \( A\text{ is in the spectrum of }Q \) using antiProperty_def
with assms(2) have \( A\text{ is in the spectrum of }P \)
then show \( thesis \) using antiProperty_def
qed
If a space can be \( P(T)\wedge Q(T) \) only in case the underlying set is in the spectrum of P; then \( Q(T)\longrightarrow ANTI(P,T) \) when Q is hereditary.
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)) \)proof fix \( T \)
{
assume \( T\text{ is a topology } \)
{
assume \( Q(T) \)
{
assume \( \neg (T\{is anti-\}P) \)
then obtain \( A \) where \( A\in Pow(\bigcup T) \), \( P(T\text{ restricted to }A) \), \( \neg (A\text{ is in the spectrum of }P) \) unfolding antiProperty_def
from \( Q(T) \), \( T\text{ is a topology } \), \( A\in Pow(\bigcup T) \), assms(2) have \( Q(T\text{ restricted to }A) \) unfolding IsHer_def
moreover
note \( P(T\text{ restricted to }A) \), assms(1)
moreover from \( T\text{ is a topology } \) have \( (T\text{ restricted to }A)\text{ is a topology } \) using Top_1_L4, topology0_def
moreover from \( A\in Pow(\bigcup T) \) have \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
ultimately have \( A\text{ is in the spectrum of }P \)
with \( \neg (A\text{ is in the spectrum of }P) \) have \( False \)
then have \( T\{is anti-\}P \)
then have \( Q(T)\longrightarrow (T\{is anti-\}P) \)
then show \( (T \text{ is a topology }) \longrightarrow (Q(T) \longrightarrow (T\{is anti-\}P)) \)
qed
If a topologycal space has an hereditary property, then it has its double-anti property.
theorem (in topology0) her_P_imp_anti2P:
assumes \( P\text{ is hereditary } \), \( P(T) \)
shows \( T\{is anti-\}ANTI(P) \)proof{
}
assume \( \neg (T\{is anti-\}ANTI(P)) \)
then have \( \exists A\in Pow(\bigcup T).\ ((T\text{ restricted to }A)\{is anti-\}P)\wedge \neg (A\text{ is in the spectrum of }ANTI(P)) \) unfolding antiProperty_def
then obtain \( A \) where A_def: \( A\in Pow(\bigcup T) \), \( \neg (A\text{ is in the spectrum of }ANTI(P)) \), \( (T\text{ restricted to }A)\{is anti-\}P \)
from \( A\in Pow(\bigcup T) \) have tot: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
from A_def have reg: \( \forall B\in Pow(\bigcup (T\text{ restricted to }A)).\ P((T\text{ restricted to }A)\text{ restricted to }B) \longrightarrow (B\text{ is in the spectrum of }P) \) unfolding antiProperty_def
from \( A\in Pow(\bigcup T) \) have \( \forall B\in Pow(A).\ (T\text{ restricted to }A)\text{ restricted to }B=T\text{ restricted to }B \) using subspace_of_subspace
then have \( \forall B\in Pow(A).\ P(T\text{ restricted to }B) \longrightarrow (B\text{ is in the spectrum of }P) \) using reg, tot
moreover
from \( A\in Pow(\bigcup T) \) have \( \forall B\in Pow(A).\ P(T\text{ restricted to }B) \) using assms, topSpaceAssum unfolding IsHer_def
ultimately have reg2: \( \forall B\in Pow(A).\ (B\text{ is in the spectrum of }P) \)
from \( \neg (A\text{ is in the spectrum of }ANTI(P)) \) have \( \exists T.\ T\text{ is a topology } \wedge \bigcup T\approx A \wedge \neg (T\{is anti-\}P) \) unfolding Spec_def
then obtain \( S \) where \( S\text{ is a topology } \), \( \bigcup S\approx A \), \( \neg (S\{is anti-\}P) \)
from \( \neg (S\{is anti-\}P) \) have \( \exists B\in Pow(\bigcup S).\ P(S\text{ restricted to }B) \wedge \neg (B\text{ is in the spectrum of }P) \) unfolding antiProperty_def
then obtain \( B \) where B_def: \( \neg (B\text{ is in the spectrum of }P) \), \( B\in Pow(\bigcup S) \)
then have \( B\preceq \bigcup S \) using subset_imp_lepoll
with \( \bigcup S\approx A \) have \( B\preceq A \) using lepoll_eq_trans
then obtain \( f \) where \( f\in \text{inj}(B,A) \) unfolding lepoll_def
then have \( f\in \text{bij}(B,\text{range}(f)) \) using inj_bij_range
then have \( B\approx \text{range}(f) \) unfolding eqpoll_def
with B_def(1) have \( \neg (\text{range}(f)\text{ is in the spectrum of }P) \) using eqpoll_iff_spec
moreover
from this, \( f\in \text{inj}(B,A) \) have \( \text{range}(f)\subseteq A \) unfolding inj_def, Pi_def
with reg2 have \( \text{range}(f)\text{ is in the spectrum of }P \)
ultimately have \( False \)
then show \( thesis \)
qed
The anti-properties are always hereditary
theorem anti_here:
shows \( (ANTI(P))\text{ is hereditary } \)proof{
}
}
fix \( T \)
assume \( T \text{ is a topology } \), \( ANTI(P,T) \)
{
fix \( A \)
assume \( A\in Pow(\bigcup T) \)
then have \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
moreover {
}
ultimately have \( \forall B\in Pow(\bigcup (T\text{ restricted to }A)).\ (P((T\text{ restricted to }A)\text{ restricted to }B)) \longrightarrow (B\text{ is in the spectrum of }P) \)
fix \( B \)
assume \( B\in Pow(A) \), \( P((T\text{ restricted to }A)\text{ restricted to }B) \)
with \( A\in Pow(\bigcup T) \) have \( B\in Pow(\bigcup T) \), \( P(T\text{ restricted to }B) \) using subspace_of_subspace
with \( ANTI(P,T) \) have \( B\text{ is in the spectrum of }P \) unfolding antiProperty_def
then have \( ANTI(P,(T\text{ restricted to }A)) \) unfolding antiProperty_def
then have \( \forall A\in Pow(\bigcup T).\ ANTI(P,(T\text{ restricted to }A)) \)
then show \( thesis \) using IsHer_def
qed
A space that is anti-\(P\) is also anti-anti-anti-\(P\).
corollary (in topology0) anti_imp_anti3:
assumes \( T\{is anti-\}P \)
shows \( T\{is anti-\}ANTI(ANTI(P)) \) using anti_here, her_P_imp_anti2P, assmsIn the article \cite{ReVa80}, we can find some results on anti-properties.
theorem (in topology0) anti_T0:
shows \( (T\{is anti-\}isT0) \longleftrightarrow T=\{0,\bigcup T\} \)proof assume \( T=\{0,\bigcup T\} \)
{
fix \( A \)
assume \( A\in Pow(\bigcup T) \), \( (T\text{ restricted to }A) \text{ is }T_0 \)
{
fix \( B \)
assume \( B\in T\text{ restricted to }A \)
then obtain \( S \) where \( S\in T \) and \( B=A\cap S \) unfolding RestrictedTo_def
with \( T=\{0,\bigcup T\} \) have \( S\in \{0,\bigcup T\} \)
then have \( S=0\vee S=\bigcup T \)
with \( B=A\cap S \), \( A\in Pow(\bigcup T) \) have \( B=0\vee B=A \)
moreover {
}
ultimately have \( (T\text{ restricted to }A)=\{0,A\} \)
{
have \( 0\in \{0,\bigcup T\} \), \( \bigcup T\in \{0,\bigcup T\} \)
with \( T=\{0,\bigcup T\} \) have \( 0\in T \), \( (\bigcup T)\in T \)
then have \( A\cap 0\in (T\text{ restricted to }A) \), \( A\cap (\bigcup T)\in (T\text{ restricted to }A) \) using RestrictedTo_def
moreover
from \( A\in Pow(\bigcup T) \) have \( A\cap (\bigcup T)=A \)
ultimately have \( 0\in (T\text{ restricted to }A) \), \( A\in (T\text{ restricted to }A) \)
with \( (T\text{ restricted to }A) \text{ is }T_0 \) have \( \{0,A\} \text{ is }T_0 \)
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
{
fix \( y \)
assume \( y\in A \), \( x\neq y \)
with \( \{0,A\} \text{ is }T_0 \) obtain \( U \) where \( U\in \{0,A\} \) and dis: \( (x \in U \wedge y \notin U) \vee (y \in U \wedge x \notin U) \) using isT0_def
then have \( U=A \)
with dis, \( y\in A \), \( x\in A \) have \( False \)
then have \( \forall y\in A.\ y=x \)
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
then have \( A\text{ is in the spectrum of }isT0 \) using T0_spectrum
moreover {
}
ultimately have \( A\text{ is in the spectrum of }isT0 \)
assume \( A=0 \)
then have \( A\approx 0 \)
then have \( A\preceq 1 \) using empty_lepollI, eq_lepoll_trans
then have \( A\text{ is in the spectrum of }isT0 \) using T0_spectrum
then show \( T\{is anti-\}isT0 \) using antiProperty_def
next
assume \( T\{is anti-\}isT0 \)
then have \( \forall A\in Pow(\bigcup T).\ (T\text{ restricted to }A)\text{ is }T_0 \longrightarrow (A\text{ is in the spectrum of }isT0) \) using antiProperty_def
then have reg: \( \forall A\in Pow(\bigcup T).\ (T\text{ restricted to }A)\text{ is }T_0 \longrightarrow (A\preceq 1) \) using T0_spectrum
{
assume \( \exists A\in T.\ A\neq 0\wedge A\neq \bigcup T \)
then obtain \( A \) where \( A\in T \), \( A\neq 0 \), \( A\neq \bigcup T \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in \bigcup T-A \)
with \( A\in T \) have s: \( \{x,y\}\in Pow(\bigcup T) \), \( x\neq y \)
note s
moreover {
}
fix \( b1 \) \( b2 \)
assume \( b1\in \bigcup (T\{restricted to}\{x,y\}\} \), \( b2\in \bigcup (T\{restricted to}\{x,y\}\} \), \( b1\neq b2 \)
moreover
from s have \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
ultimately have \( (b1=x\wedge b2=y)\vee (b1=y\wedge b2=x) \)
with \( x\neq y \) have \( (b1\in \{x\}\wedge b2\notin \{x\}) \vee (b2\in \{x\}\wedge b1\notin \{x\}) \)
moreover
from \( y\in \bigcup T-A \), \( x\in A \) have \( \{x\}=\{x,y\}\cap A \)
with \( A\in T \) have \( \{x\}\in (T\{restricted to}\{x,y\}\} \) unfolding RestrictedTo_def
ultimately have \( \exists U\in (T\{restricted to}\{x,y\}).\ (b1\in U\wedge b2\notin U) \vee (b2\in U\wedge b1\notin U\} \)
then have \( (T\{restricted to}\{x,y\})\{is T_0\\} \) using isT0_def
ultimately have \( \{x,y\}\preceq 1 \) using reg
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\} \)
then have \( y=x \)
with \( x\neq y \) have \( False \)
then have \( T\subseteq \{0,\bigcup T\} \)
moreover
qed
from topSpaceAssum have \( 0\in T \), \( \bigcup T\in T \) using IsATopology_def, empty_open
ultimately show \( T=\{0,\bigcup T\} \)
The spectrum of the indiscrete topology property is the class of sets of cardinality at most \(1\).
lemma indiscrete_spectrum:
shows \( (A \text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\})) \longleftrightarrow A\preceq 1 \)proof assume \( (A \text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\})) \)
then have reg: \( \forall T.\ ((T\text{ is a topology } \wedge \bigcup T\approx A) \longrightarrow T =\{0,\bigcup T\}) \) using Spec_def
moreover
{
have \( \bigcup Pow(A)=A \)
then have \( \bigcup Pow(A)\approx A \)
moreover have \( Pow(A) \text{ is a topology } \) using Pow_is_top
ultimately have P: \( Pow(A)=\{0,A\} \)
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
then have \( \{x\}\in Pow(A) \)
with P have \( \{x\}=A \)
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\approx 0 \)
then have \( A\preceq 1 \) using empty_lepollI, eq_lepoll_trans
next
assume \( A\preceq 1 \)
{
fix \( T \)
assume \( T\text{ is a topology } \), \( \bigcup T\approx A \)
{
assume \( A=0 \)
with \( \bigcup T\approx A \) have \( \bigcup T\approx 0 \)
then have \( \bigcup T=0 \) using eqpoll_0_is_0
then have \( T\subseteq \{0\} \)
with \( T\text{ is a topology } \) have \( T=\{0\} \) using empty_open
then have \( T=\{0,\bigcup T\} \)
moreover {
}
ultimately have \( T=\{0,\bigcup T\} \)
assume \( A\neq 0 \)
then obtain \( E \) where \( E\in A \)
with \( A\preceq 1 \) have \( A=\{E\} \) using lepoll_1_is_sing
then have \( A\approx 1 \) using singleton_eqpoll_1
with \( \bigcup T\approx A \) have NONempty: \( \bigcup T\approx 1 \) using eqpoll_trans
then have \( \bigcup T\preceq 1 \) using eqpoll_imp_lepoll
moreover {
}
assume \( \bigcup T=0 \)
then have \( 0\approx \bigcup T \)
with NONempty have \( 0\approx 1 \) using eqpoll_trans
then have \( 0=1 \) using eqpoll_0_is_0, eqpoll_sym
then have \( False \)
then have \( \bigcup T\neq 0 \)
then obtain \( R \) where \( R\in \bigcup T \)
ultimately have \( \bigcup T=\{R\} \) using lepoll_1_is_sing
moreover
have \( T\subseteq Pow(\bigcup T) \)
ultimately have \( T\subseteq Pow(\{R\}) \)
then have \( T\subseteq \{0,\{R\}\} \)
moreover
from this, \( T\text{ is a topology } \) have \( 0\in T \), \( \bigcup T\in T \) using IsATopology_def
moreover note \( \bigcup T=\{R\} \)
ultimately have \( T=\{0,\bigcup T\} \)
then show \( A \text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\}) \) using Spec_def
qed
A space is anti-indiscrete if and only if it is \(T_0\).
theorem (in topology0) anti_indiscrete:
shows \( (T\{is anti-\}(\lambda T.\ T=\{0,\bigcup T\})) \longleftrightarrow T\text{ is }T_0 \)proof assume \( T\text{ is }T_0 \)
{
fix \( A \)
assume \( A\in Pow(\bigcup T) \), \( T\text{ restricted to }A=\{0,\bigcup (T\text{ restricted to }A)\} \)
then have un: \( \bigcup (T\text{ restricted to }A)=A \), \( T\text{ restricted to }A=\{0,A\} \) using RestrictedTo_def
from \( T\text{ is }T_0 \), \( A\in Pow(\bigcup T) \) have \( (T\text{ restricted to }A)\text{ is }T_0 \) using T0_here
{
assume \( A=0 \)
then have \( A\approx 0 \)
then have \( A\preceq 1 \) using empty_lepollI, eq_lepoll_trans
moreover {
}
}
ultimately have \( A\preceq 1 \)
assume \( A\neq 0 \)
then obtain \( E \) where \( E\in A \)
{
fix \( y \)
assume \( y\in A \), \( y\neq E \)
with \( E\in A \), un have \( y\in \bigcup (T\text{ restricted to }A) \), \( E\in \bigcup (T\text{ restricted to }A) \)
with \( (T\text{ restricted to }A)\text{ is }T_0 \), \( y\neq E \) have \( \exists U\in (T\text{ restricted to }A).\ (E\in U\wedge y\notin U)\vee (E\notin U\wedge y\in U) \) unfolding isT0_def
then obtain \( U \) where \( U\in (T\text{ restricted to }A) \), \( (E\in U\wedge y\notin U)\vee (E\notin U\wedge y\in U) \)
with \( T\text{ restricted to }A=\{0,A\} \) have \( U=0\vee U=A \)
with \( (E\in U\wedge y\notin U)\vee (E\notin U\wedge y\in U) \), \( y\in A \), \( E\in A \) have \( False \)
then have \( \forall y\in A.\ y=E \)
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
then have \( A\text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\}) \) using indiscrete_spectrum
then show \( T\{is anti-\}(\lambda T.\ T=\{0,\bigcup T\}) \) unfolding antiProperty_def
next
assume \( T\{is anti-\}(\lambda T.\ T=\{0,\bigcup T\}) \)
then have \( \forall A\in Pow(\bigcup T).\ (T\text{ restricted to }A)=\{0,\bigcup (T\text{ restricted to }A)\} \longrightarrow (A \text{ is in the spectrum of } (\lambda T.\ T=\{0,\bigcup T\})) \) using antiProperty_def
then have \( \forall A\in Pow(\bigcup T).\ (T\text{ restricted to }A)=\{0,\bigcup (T\text{ restricted to }A)\} \longrightarrow A\preceq 1 \) using indiscrete_spectrum
moreover
{
have \( \forall A\in Pow(\bigcup T).\ \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
ultimately have reg: \( \forall A\in Pow(\bigcup T).\ (T\text{ restricted to }A)=\{0,A\} \longrightarrow A\preceq 1 \)
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
{
assume \( \forall U\in T.\ (x\in U\wedge y\in U)\vee (x\notin U\wedge y\notin U) \)
then have \( T\{restricted to}\{x,y\}\subseteq \{0,\{x,y\}\\} \) unfolding RestrictedTo_def
moreover
from \( x\in \bigcup T \), \( y\in \bigcup T \) have emp: \( 0\in T \), \( \{x,y\}\cap 0=0 \) and tot: \( \{x,y\}=\{x,y\}\cap \bigcup T \), \( \bigcup T\in T \) using topSpaceAssum, empty_open, IsATopology_def
then have \( 0\in T\{restricted to}\{x,y\\} \) unfolding RestrictedTo_def
moreover from tot have \( \{x,y\}\in T\{restricted to}\{x,y\\} \) unfolding RestrictedTo_def
ultimately have \( T\{restricted to}\{x,y\}=\{0,\{x,y\}\\} \)
with reg, \( x\in \bigcup T \), \( y\in \bigcup T \) have \( \{x,y\}\preceq 1 \)
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\} \)
then have \( y=x \)
with \( x\neq y \) have \( False \)
then have \( \exists U\in T.\ (x\notin U\vee y\notin U)\wedge (x\in U\vee y\in U) \)
then have \( \exists U\in T.\ (x\in U\wedge y\notin U)\vee (x\notin U\wedge y\in U) \)
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 \( T \text{ is }T_0 \) using isT0_def
qed
The conclusion is that being \(T_0\) is just the opposite to being indiscrete.
Next, let's compute the anti-\(T_i\) for \(i=1,\ 2,\ 3\) or \(4\). Surprisingly, they are all the same. Meaning, that the total negation of \(T_1\) is enough to negate all of these axioms.
theorem anti_T1:
shows \( (T\{is anti-\}isT1) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)proof assume \( T\{is anti-\}isT1 \)
let \( r = \{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\} \)
have \( \text{antisym}(r) \) unfolding antisym_def
moreover
}
}
}
have \( \text{trans}(r) \) unfolding trans_def
moreover {
fix \( A \) \( B \)
assume \( A\in T \), \( B\in T \)
{
assume \( \neg (A\subseteq B\vee B\subseteq A) \)
then have \( A-B\neq 0 \), \( B-A\neq 0 \)
then obtain \( x \) \( y \) where \( x\in A \), \( x\notin B \), \( y\in B \), \( y\notin A \), \( x\neq y \)
then have \( \{x,y\}\cap A=\{x\} \), \( \{x,y\}\cap B=\{y\} \)
moreover
from \( A\in T \), \( B\in T \) have \( \{x,y\}\cap A\in T\{restricted to}\{x,y\\} \), \( \{x,y\}\cap B\in T\{restricted to}\{x,y\\} \) unfolding RestrictedTo_def
ultimately have open_set: \( \{x\}\in T\{restricted to}\{x,y\\} \), \( \{y\}\in T\{restricted to}\{x,y\\} \)
from \( A\in T \), \( B\in T \), \( x\in A \), \( y\in B \) have \( x\in \bigcup T \), \( y\in \bigcup T \)
then have sub: \( \{x,y\}\in Pow(\bigcup T) \)
then have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
{
fix \( s \) \( t \)
assume \( s\in \bigcup (T\{restricted to}\{x,y\}\} \), \( t\in \bigcup (T\{restricted to}\{x,y\}\} \), \( s\neq t \)
with tot have \( s\in \{x,y\} \), \( t\in \{x,y\} \), \( s\neq t \)
then have \( (s=x\wedge t=y)\vee (s=y\wedge t=x) \)
with open_set, \( x\neq y \) have \( \exists U\in (T\{restricted to}\{x,y\}).\ s\in U\wedge t\notin \} \)
then have \( (T\{restricted to}\{x,y\})\{is T_1\\} \) unfolding isT1_def
with sub, \( T\{is anti-\}isT1 \), tot have \( \{x,y\} \text{ is in the spectrum of }isT1 \) using antiProperty_def
then have \( \{x,y\}\preceq 1 \) using T1_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\}=\{x,y\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
then have \( x=y \)
with \( x\in A \), \( y\notin A \) have \( False \)
then have \( A\subseteq B\vee B\subseteq A \)
then have \( r \text{ is total on }T \) using IsTotal_def
ultimately show \( \text{IsLinOrder}(T,r) \) using IsLinOrder_def
next
assume \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \)
then have ordTot: \( \forall S\in T.\ \forall B\in T.\ S\subseteq B\vee B\subseteq S \) unfolding IsLinOrder_def, IsTotal_def
{
fix \( A \)
assume \( A\in Pow(\bigcup T) \) and T1: \( (T\text{ restricted to }A) \text{ is }T_1 \)
then have tot: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
{
fix \( U \) \( V \)
assume \( U\in T\text{ restricted to }A \), \( V\in T\text{ restricted to }A \)
then obtain \( AU \) \( AV \) where \( AU\in T \), \( AV\in T \), \( U=A\cap AU \), \( V=A\cap AV \) unfolding RestrictedTo_def
with ordTot have \( U\subseteq V\vee V\subseteq U \)
then have ordTotSub: \( \forall S\in T\text{ restricted to }A.\ \forall B\in T\text{ restricted to }A.\ S\subseteq B\vee B\subseteq S \)
{
assume \( A=0 \)
then have \( A\approx 0 \)
moreover
have \( 0\preceq 1 \) using empty_lepollI
ultimately have \( A\preceq 1 \) using eq_lepoll_trans
then have \( A\text{ is in the spectrum of }isT1 \) using T1_spectrum
moreover {
}
}
ultimately have \( A\text{ is in the spectrum of }isT1 \)
assume \( A\neq 0 \)
then obtain \( t \) where \( t\in A \)
{
fix \( y \)
assume \( y\in A \), \( y\neq t \)
with \( t\in A \), tot, T1 obtain \( U \) where \( U\in (T\text{ restricted to }A) \), \( y\in U \), \( t\notin U \) unfolding isT1_def
from \( y\neq t \) have \( t\neq y \)
with \( y\in A \), \( t\in A \), tot, T1 obtain \( V \) where \( V\in (T\text{ restricted to }A) \), \( t\in V \), \( y\notin V \) unfolding isT1_def
with \( y\in U \), \( t\notin U \) have \( \neg (U\subseteq V\vee V\subseteq U) \)
with ordTotSub, \( U\in (T\text{ restricted to }A) \), \( V\in (T\text{ restricted to }A) \) have \( False \)
then have \( \forall y\in A.\ y=t \)
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 }isT1 \) using T1_spectrum
then show \( T\{is anti-\}isT1 \) using antiProperty_def
qed
The linearly ordered topology property is hereditary.
corollary linordtop_here:
shows \( (\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}))\text{ is hereditary } \)proof from anti_here have \( (\lambda T.\ ANTI(isT1,T))\text{ is hereditary } \)
then show \( thesis \) using anti_T1
qed
A space is anti-\(T_4\) if and only if its open sets are linearly ordered by inclusion.
theorem (in topology0) anti_T4:
shows \( (T\{is anti-\}isT4) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)proof assume \( T\{is anti-\}isT4 \)
let \( r = \{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\} \)
have \( \text{antisym}(r) \) unfolding antisym_def
moreover
}
}
}
have \( \text{trans}(r) \) unfolding trans_def
moreover {
fix \( A \) \( B \)
assume \( A\in T \), \( B\in T \)
{
assume \( \neg (A\subseteq B\vee B\subseteq A) \)
then have \( A-B\neq 0 \), \( B-A\neq 0 \)
then obtain \( x \) \( y \) where \( x\in A \), \( x\notin B \), \( y\in B \), \( y\notin A \), \( x\neq y \)
then have \( \{x,y\}\cap A=\{x\} \), \( \{x,y\}\cap B=\{y\} \)
moreover
from \( A\in T \), \( B\in T \) have \( \{x,y\}\cap A\in T\{restricted to}\{x,y\\} \), \( \{x,y\}\cap B\in T\{restricted to}\{x,y\\} \) unfolding RestrictedTo_def
ultimately have open_set: \( \{x\}\in T\{restricted to}\{x,y\\} \), \( \{y\}\in T\{restricted to}\{x,y\\} \)
from \( A\in T \), \( B\in T \), \( x\in A \), \( y\in B \) have \( x\in \bigcup T \), \( y\in \bigcup T \)
then have sub: \( \{x,y\}\in Pow(\bigcup T) \)
then have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
{
fix \( s \) \( t \)
assume \( s\in \bigcup (T\{restricted to}\{x,y\}\} \), \( t\in \bigcup (T\{restricted to}\{x,y\}\} \), \( s\neq t \)
with tot have \( s\in \{x,y\} \), \( t\in \{x,y\} \), \( s\neq t \)
then have \( (s=x\wedge t=y)\vee (s=y\wedge t=x) \)
with open_set, \( x\neq y \) have \( \exists U\in (T\{restricted to}\{x,y\}).\ s\in U\wedge t\notin \} \)
then have \( (T\{restricted to}\{x,y\})\{is T_1\\} \) unfolding isT1_def
moreover {
}
}
fix \( s \)
assume AS: \( s\text{ is closed in }(T\{restricted to}\{x,y\}\} \)
{
fix \( t \)
assume AS2: \( t\text{ is closed in }(T\{restricted to}\{x,y\}\} \), \( s\cap t=0 \)
have h: \( (T\{restricted to}\{x,y\})\text{ is a topology \} \) using Top_1_L4
from union_open have \( (T\{restricted to}\{x,y\}) \text{ is a topology } \Longrightarrow \)
\( \forall A\in T\{restricted to}\{x,y\}.\ A \in (T\{restricted to}\{x,y\}) \Longrightarrow \)
\( \bigcup (T\{restricted to}\{x,y\}) \in (T\{restricted to}\{x,y\}\\\\\} \)
with h, tot have \( 0\in (T\{restricted to}\{x,y\}\} \), \( \{x,y\}\in (T\{restricted to}\{x,y\}\} \) using empty_open
moreover
note open_set
moreover have \( T\{restricted to}\{x,y\}\subseteq Pow(\bigcup (T\{restricted to}\{x,y\})\\} \)
with tot have \( T\{restricted to}\{x,y\}\subseteq Pow(\{x,y\}\} \)
ultimately have \( T\{restricted to}\{x,y\}=\{0,\{x\},\{y\},\{x,y\}\\} \)
moreover
have \( \{0,\{x\},\{y\},\{x,y\}\}=Pow(\{x,y\}) \)
ultimately have P: \( T\{restricted to}\{x,y\}=Pow(\{x,y\}\} \)
with tot have \( \{A\in Pow(\{x,y\}).\ A\text{ is closed in }(T\{restricted to}\{x,y\})\}=\{A \in Pow(\{x, y\}) .\ A \subseteq \{x, y\} \wedge \{x, y\} - A \in Pow(\{x, y\})\\} \) using IsClosed_def
with P have S: \( \{A\in Pow(\{x,y\}).\ A\text{ is closed in }(T\{restricted to}\{x,y\})\}=T\{restricted to}\{x,y\\\} \)
from AS, AS2(1) have \( s\in Pow(\{x,y\}) \), \( t\in Pow(\{x,y\}) \) using IsClosed_def, tot
moreover
note AS2(1), AS
ultimately have \( s\in \{A\in Pow(\{x,y\}).\ A\text{ is closed in }(T\{restricted to}\{x,y\})\\} \), \( t\in \{A\in Pow(\{x,y\}).\ A\text{ is closed in }(T\{restricted to}\{x,y\})\\} \)
with S, AS2(2) have \( s\in T\{restricted to}\{x,y\\} \), \( t\in T\{restricted to}\{x,y\\} \), \( s\cap t=0 \)
then have \( \exists U\in (T\{restricted to}\{x,y\}).\ \exists V\in (T\{restricted to}\{x,y\}).\ s\subseteq U\wedge t\subseteq V\wedge U\cap V=\\} \)
then have \( \forall t.\ t\text{ is closed in }(T\{restricted to}\{x,y\})\wedge s\cap t=0 \longrightarrow (\exists U\in (T\{restricted to}\{x,y\}).\ \exists V\in (T\{restricted to}\{x,y\}).\ s\subseteq U\wedge t\subseteq V\wedge U\cap V=0\\\} \)
then have \( \forall s.\ s\text{ is closed in }(T\{restricted to}\{x,y\}) \longrightarrow (\forall t.\ t\text{ is closed in }(T\{restricted to}\{x,y\})\wedge s\cap t=0 \longrightarrow (\exists U\in (T\{restricted to}\{x,y\}).\ \exists V\in (T\{restricted to}\{x,y\}).\ s\subseteq U\wedge t\subseteq V\wedge U\cap V=0)\\\\} \)
then have \( (T\{restricted to}\{x,y\})\text{ is normal \} \) using IsNormal_def
ultimately have \( (T\{restricted to}\{x,y\})\{is T_4\\} \) using isT4_def
with sub, \( T\{is anti-\}isT4 \), tot have \( \{x,y\} \text{ is in the spectrum of }isT4 \) using antiProperty_def
then have \( \{x,y\}\preceq 1 \) using T4_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\}=\{x,y\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
then have \( x=y \)
with \( x\in A \), \( y\notin A \) have \( False \)
then have \( A\subseteq B\vee B\subseteq A \)
then have \( r \text{ is total on }T \) using IsTotal_def
ultimately show \( \text{IsLinOrder}(T,r) \) using IsLinOrder_def
next
assume \( \text{IsLinOrder}(T, \{\langle U,V\rangle \in Pow(\bigcup T) \times Pow(\bigcup T) .\ U \subseteq V\}) \)
then have \( T\{is anti-\}isT1 \) using anti_T1
moreover
qed
have \( \forall T.\ T\text{ is a topology } \longrightarrow (T\{is T_4\}) \longrightarrow (T\text{ is }T_1) \) using T4_is_T3, T3_is_T2, T2_is_T1, topology0_def
moreover have \( \forall A.\ (A \text{ is in the spectrum of } isT1) \longrightarrow (A \text{ is in the spectrum of } isT4) \) using T1_spectrum, T4_spectrum
moreover have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_1) \Longrightarrow \)
\( \forall A.\ A \text{ is in the spectrum of } isT1 \longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( ANTI(isT1, T) \Longrightarrow ANTI(isT4, T) \) using eq_spect_rev_imp_anti
ultimately show \( T\{is anti-\}isT4 \)
A space is anti-\(T_3\) if and only if its open sets are linearly ordered by inclusion.
theorem (in topology0) anti_T3:
shows \( (T\{is anti-\}isT3) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)proof assume \( T\{is anti-\}isT3 \)
moreover
have \( \forall T.\ T\text{ is a topology } \longrightarrow (T\{is T_4\}) \longrightarrow (T\text{ is }T_3) \) using T4_is_T3, topology0_def
moreover have \( \forall A.\ (A \text{ is in the spectrum of } isT3) \longrightarrow (A \text{ is in the spectrum of } isT4) \) using T3_spectrum, T4_spectrum
moreover have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_3) \Longrightarrow \)
\( \forall A.\ A \text{ is in the spectrum of } isT3 \longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( ANTI(isT3, T) \Longrightarrow ANTI(isT4, T) \) using eq_spect_rev_imp_anti
ultimately have \( T\{is anti-\}isT4 \)
then show \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) using anti_T4
next
assume \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \)
then have \( T\{is anti-\}isT1 \) using anti_T1
moreover
qed
have \( \forall T.\ T\text{ is a topology } \longrightarrow (T\text{ is }T_3) \longrightarrow (T\text{ is }T_1) \) using T3_is_T2, T2_is_T1, topology0_def
moreover have \( \forall A.\ (A \text{ is in the spectrum of } isT1) \longrightarrow (A \text{ is in the spectrum of } isT3) \) using T1_spectrum, T3_spectrum
moreover have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\text{ is }T_3 \longrightarrow T \text{ is }T_1) \Longrightarrow \)
\( \forall A.\ A \text{ is in the spectrum of } isT1 \longrightarrow \)
\( A \text{ is in the spectrum of } isT3 \Longrightarrow \)
\( ANTI(isT1, T) \Longrightarrow ANTI(isT3, T) \) using eq_spect_rev_imp_anti
ultimately show \( T\{is anti-\}isT3 \)
A space is anti-\(T_2\) if and only if its open sets are linearly ordered by inclusion.
theorem (in topology0) anti_T2:
shows \( (T\{is anti-\}isT2) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)proof assume \( T\{is anti-\}isT2 \)
moreover
have \( \forall T.\ T\text{ is a topology } \longrightarrow (T\{is T_4\}) \longrightarrow (T\text{ is }T_2) \) using T4_is_T3, T3_is_T2, topology0_def
moreover have \( \forall A.\ (A \text{ is in the spectrum of } isT2) \longrightarrow (A \text{ is in the spectrum of } isT4) \) using T2_spectrum, T4_spectrum
moreover have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\{is T_4\} \longrightarrow T \text{ is }T_2) \Longrightarrow \)
\( \forall A.\ A \text{ is in the spectrum of } isT2 \longrightarrow \)
\( A \text{ is in the spectrum of } isT4 \Longrightarrow \)
\( ANTI(isT2, T) \Longrightarrow ANTI(isT4, T) \) using eq_spect_rev_imp_anti
ultimately have \( T\{is anti-\}isT4 \)
then show \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) using anti_T4
next
assume \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \)
then have \( T\{is anti-\}isT1 \) using anti_T1
moreover
qed
have \( \forall T.\ T\text{ is a topology } \longrightarrow (T\text{ is }T_2) \longrightarrow (T\text{ is }T_1) \) using T2_is_T1
moreover have \( \forall A.\ (A \text{ is in the spectrum of } isT1) \longrightarrow (A \text{ is in the spectrum of } isT2) \) using T1_spectrum, T2_spectrum
moreover have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( (T\text{ is }T_2 \longrightarrow T \text{ is }T_1) \Longrightarrow \)
\( \forall A.\ A \text{ is in the spectrum of } isT1 \longrightarrow \)
\( A \text{ is in the spectrum of } isT2 \Longrightarrow \)
\( ANTI(isT1, T) \Longrightarrow ANTI(isT2, T) \) using eq_spect_rev_imp_anti
ultimately show \( T\{is anti-\}isT2 \)
The spectrum of the linear order property on topologies is the class of sets of cardinality at most \(1\).
lemma linord_spectrum:
shows \( (A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}))) \longleftrightarrow A\preceq 1 \)proof assume \( A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
then have reg: \( \forall T.\ T\text{ is a topology }\wedge \bigcup T\approx A \longrightarrow \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) using Spec_def
{
assume \( A=0 \)
moreover
have \( 0\preceq 1 \) using empty_lepollI
ultimately have \( A\preceq 1 \) using eq_lepoll_trans
moreover {
}
ultimately show \( A\preceq 1 \)
assume \( A\neq 0 \)
then obtain \( x \) where \( x\in A \)
moreover {
}
ultimately have \( A=\{x\} \)
fix \( y \)
assume \( y\in A \)
have \( Pow(A) \text{ is a topology } \) using Pow_is_top
moreover
note reg
ultimately have \( \text{IsLinOrder}(Pow(A),\{\langle U,V\rangle \in Pow(\bigcup Pow(A))\times Pow(\bigcup Pow(A)).\ U\subseteq V\}) \)
then have \( \text{IsLinOrder}(Pow(A),\{\langle U,V\rangle \in Pow(A)\times Pow(A).\ U\subseteq V\}) \)
with \( x\in A \), \( y\in A \) have \( \{x\}\subseteq \{y\}\vee \{y\}\subseteq \{x\} \) unfolding IsLinOrder_def, IsTotal_def
then have \( x=y \)
then have \( A\approx 1 \) using singleton_eqpoll_1
then have \( A\preceq 1 \) using eqpoll_imp_lepoll
next
assume \( A\preceq 1 \)
then have ind: \( A\text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\}) \) using indiscrete_spectrum
{
fix \( T \)
assume AS: \( T\text{ is a topology } \), \( T=\{0,\bigcup T\} \)
have \( \text{trans}(\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) unfolding trans_def
moreover
have \( \text{antisym}(\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) unfolding antisym_def
moreover have \( \{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V}\text{ is total on }\} \)proof
ultimately have \( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}) \) unfolding IsLinOrder_def
{
}
fix \( aa \) \( b \)
assume \( aa\in T \), \( b\in T \)
with AS(2) have \( aa\in \{0,\bigcup T\} \), \( b\in \{0,\bigcup T\} \)
then have \( aa=0\vee aa=\bigcup T \), \( b=0\vee b=\bigcup T \)
then have \( aa\subseteq b\vee b\subseteq aa \)
with \( aa\in T \), \( b\in T \) have \( \langle aa, b\rangle \in Collect(Pow(\bigcup T) \times Pow(\bigcup T), split((\subseteq ))) \vee \langle b, aa\rangle \in Collect(Pow(\bigcup T) \times Pow(\bigcup T), split((\subseteq ))) \)
then show \( thesis \) using IsTotal_def
qed
then have \( \forall T.\ T \text{ is a topology } \longrightarrow T = \{0, \bigcup T\} \longrightarrow \text{IsLinOrder}(T, \{\langle U,V\rangle \in Pow(\bigcup T) \times Pow(\bigcup T) .\ U \subseteq V\}) \)
moreover
qed
from P_imp_Q_spec_inv have \( \forall T.\ T \text{ is a topology } \longrightarrow \)
\( T =\)
\( cons(\emptyset , cons(\bigcup T, \emptyset )) \longrightarrow \)
\( IsLinOrder\)
\( (T, \{\langle U,V\rangle \in Pow(\bigcup T) \times \)
\( Pow(\bigcup T) .\ \)
\( U \subseteq V\}) \Longrightarrow \)
\( A \text{ is in the spectrum of } \lambda T.\ \)
\( T = \{\emptyset ,\bigcup T\} \Longrightarrow A \text{ is in the spectrum of } (\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T) \times Pow(\bigcup T).\ U \subseteq V\})) \)
moreover note ind
ultimately show \( A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
A space is anti-linearly-ordered if and only if it is \(T_1\).
theorem (in topology0) anti_linord:
shows \( (T\{is anti-\}(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}))) \longleftrightarrow T\text{ is }T_1 \)proof assume AS: \( T\{is anti-\}(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
{
assume \( \neg (T\text{ is }T_1) \)
then obtain \( x \) \( y \) where \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \), \( \forall U\in T.\ x\notin U\vee y\in U \) unfolding isT1_def
{
assume \( \{x\}\in T\{restricted to}\{x,y\\} \)
then obtain \( U \) where \( U\in T \), \( \{x\}=\{x,y\}\cap U \) unfolding RestrictedTo_def
moreover
have \( x\in \{x\} \)
ultimately have \( U\in T \), \( x\in U \)
moreover {
}
assume \( y\in U \)
then have \( y\in \{x,y\}\cap U \)
with \( \{x\}=\{x,y\}\cap U \) have \( y\in \{x\} \)
with \( x\neq y \) have \( False \)
then have \( y\notin U \)
moreover note \( \forall U\in T.\ x\notin U\vee y\in U \)
ultimately have \( False \)
then have \( \{x\}\notin T\{restricted to}\{x,y\\} \)
moreover
from \( x\in \bigcup T \), \( y\in \bigcup T \) have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
moreover have \( T\{restricted to}\{x,y\}\subseteq Pow(\bigcup (T\{restricted to}\{x,y\})\\} \)
ultimately have \( T\{restricted to}\{x,y\}\subseteq Pow(\{x,y\})-\{\{x\}\\} \)
moreover
have \( Pow(\{x,y\})=\{0,\{x,y\},\{x\},\{y\}\} \)
ultimately have \( T\{restricted to}\{x,y\}\subseteq \{0,\{x,y\},\{y\}\\} \)
moreover
have \( \text{IsLinOrder}(\{0,\{x,y\},\{y\}\},\{\langle U,V\rangle \in Pow(\{x,y\})\times Pow(\{x,y\}).\ U\subseteq V\}) \)proof
ultimately have \( \text{IsLinOrder}(T\{restricted to}\{x,y\},\{\langle U,V\rangle \in Pow(\{x,y\})\times Pow(\{x,y\}).\ U\subseteq V\}\} \) using ord_linear_subset
have \( \text{antisym}(Collect(Pow(\{x, y\}) \times Pow(\{x, y\}), split((\subseteq )))) \) using antisym_def
moreover
qed
have \( \text{trans}(Collect(Pow(\{x, y\}) \times Pow(\{x, y\}), split((\subseteq )))) \) using trans_def
moreover have \( Collect(Pow(\{x, y\}) \times Pow(\{x, y\}), split((\subseteq ))) \text{ is total on } \{0, \{x, y\}, \{y\}\} \) using IsTotal_def
ultimately show \( \text{IsLinOrder}(\{0,\{x,y\},\{y\}\},\{\langle U,V\rangle \in Pow(\{x,y\})\times Pow(\{x,y\}).\ U\subseteq V\}) \) using IsLinOrder_def
with tot have \( \text{IsLinOrder}(T\{restricted to}\{x,y\},\{\langle U,V\rangle \in Pow(\bigcup (T\{restricted to}\{x,y\}))\times Pow(\bigcup (T\{restricted to}\{x,y\})).\ U\subseteq V\}\\\} \)
then have \( \text{IsLinOrder}(T\{restricted to}\{x,y\},Collect(Pow(\bigcup (T \text{ restricted to } \{x,y\})) \times Pow(\bigcup (T \text{ restricted to } \{x,y\})), split((\subseteq )))\} \)
moreover
from \( x\in \bigcup T \), \( y\in \bigcup T \) have \( \{x,y\}\in Pow(\bigcup T) \)
moreover note AS
ultimately have \( \{x,y}\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})\} \) unfolding antiProperty_def
then have \( \{x,y\}\preceq 1 \) using linord_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\}=\{x,y\} \)
moreover
have \( y\in \{x,y\} \)
ultimately have \( y\in \{x\} \)
then have \( x=y \)
with \( x\neq y \) have \( False \)
then show \( T \text{ is }T_1 \)
next
assume T1: \( T \text{ is }T_1 \)
{
fix \( A \)
assume A_def: \( A\in Pow(\bigcup T) \), \( \text{IsLinOrder}((T\text{ restricted to }A) ,\{\langle U,V\rangle \in Pow(\bigcup (T\text{ restricted to }A))\times Pow(\bigcup (T\text{ restricted to }A)).\ U\subseteq V\}) \)
{
fix \( x \)
assume AS1: \( x\in A \)
{
fix \( y \)
assume AS: \( y\in A \), \( x\neq y \)
with AS1, \( A\in Pow(\bigcup T) \) have \( \{x,y\}\in Pow(\bigcup T) \)
from \( x\in A \), \( y\in A \) have \( \{x,y\}\in Pow(A) \)
from \( \{x,y\}\in Pow(\bigcup T) \) have T11: \( (T\{restricted to}\{x,y\})\{is T_1\\} \) using T1_here, T1
moreover
from \( \{x,y\}\in Pow(\bigcup T) \) have tot: \( \bigcup (T\{restricted to}\{x,y\})=\{x,y\\} \) unfolding RestrictedTo_def
moreover note AS(2)
ultimately obtain \( U \) where \( x\in U \), \( y\notin U \), \( U\in (T\{restricted to}\{x,y\}\} \) unfolding isT1_def
moreover
from AS(2), tot, T11 obtain \( V \) where \( y\in V \), \( x\notin V \), \( V\in (T\{restricted to}\{x,y\}\} \) unfolding isT1_def
ultimately have \( x\in U-V \), \( y\in V-U \), \( U\in (T\{restricted to}\{x,y\}\} \), \( V\in (T\{restricted to}\{x,y\}\} \)
then have \( \neg (U\subseteq V\vee V\subseteq U) \), \( U\in (T\{restricted to}\{x,y\}\} \), \( V\in (T\{restricted to}\{x,y\}\} \)
then have \( \neg (\{\langle U,V\rangle \in Pow(\bigcup (T\{restricted to}\{x,y\}))\times Pow(\bigcup (T\{restricted to}\{x,y\})).\ U\subseteq V\} \text{ is total on } (T\{restricted to}\{x,y\})\\\} \) unfolding IsTotal_def
then have \( \neg ( \text{IsLinOrder}((T\{restricted to}\{x,y\}),\{\langle U,V\rangle \in Pow(\bigcup (T\{restricted to}\{x,y\}))\times Pow(\bigcup (T\{restricted to}\{x,y\})).\ U\subseteq V\})\\\} \) unfolding IsLinOrder_def
moreover {
}
ultimately have \( False \) using tot
have \( (T\text{ restricted to }A) \text{ is a topology } \) using Top_1_L4
moreover
note A_def(2), linordtop_here
ultimately have \( \forall B\in Pow(\bigcup (T\text{ restricted to }A)).\ \text{IsLinOrder}((T\text{ restricted to }A)\text{ restricted to }B ,\{\langle U,V\rangle \in Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B))\times Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B)).\ U\subseteq V\}) \) unfolding IsHer_def
moreover
from \( A\in Pow(\bigcup T) \) have tot: \( \bigcup (T\text{ restricted to }A)=A \) unfolding RestrictedTo_def
ultimately have \( \forall B\in Pow(A).\ \text{IsLinOrder}((T\text{ restricted to }A)\text{ restricted to }B ,\{\langle U,V\rangle \in Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B))\times Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B)).\ U\subseteq V\}) \)
moreover
from \( A\in Pow(\bigcup T) \) have \( \forall B\in Pow(A).\ (T\text{ restricted to }A)\text{ restricted to }B=T\text{ restricted to }B \) using subspace_of_subspace
ultimately have \( \forall B\in Pow(A).\ \text{IsLinOrder}((T\text{ restricted to }B) ,\{\langle U,V\rangle \in Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B))\times Pow(\bigcup ((T\text{ restricted to }A)\text{ restricted to }B)).\ U\subseteq V\}) \)
moreover
from \( A\in Pow(\bigcup T) \) have \( \forall B\in Pow(A).\ \bigcup ((T\text{ restricted to }A)\text{ restricted to }B)=B \) unfolding RestrictedTo_def
ultimately have \( \forall B\in Pow(A).\ \text{IsLinOrder}((T\text{ restricted to }B) ,\{\langle U,V\rangle \in Pow(B)\times Pow(B).\ U\subseteq V\}) \)
with \( \{x,y\}\in Pow(A) \) have \( \text{IsLinOrder}((T\{restricted to}\{x,y\}) ,\{\langle U,V\rangle \in Pow(\{x,y\})\times Pow(\{x,y\}).\ U\subseteq V\}\} \)
then have \( A=\{x\} \) using AS1
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 }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \) using linord_spectrum
moreover {
}
ultimately have \( A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
assume \( A=0 \)
then have \( A\approx 0 \)
moreover
have \( 0\preceq 1 \) using empty_lepollI
ultimately have \( A\preceq 1 \) using eq_lepoll_trans
then have \( A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \) using linord_spectrum
then show \( T\{is anti-\}(\lambda T.\ \text{IsLinOrder}(T, \{\langle U,V\rangle \in Pow(\bigcup T) \times Pow(\bigcup T) .\ U \subseteq V\})) \) unfolding antiProperty_def
qed
In conclusion, \(T_1\) is also an anti-property. Let's define some anti-properties that we'll use in the future.
definition
\( T\{is anti-compact\} \equiv T\{is anti-\}(\lambda T.\ (\bigcup T)\text{ is compact in }T) \)
A space is anti-Lindelöf if the only Lindelöf subspaces lie in the spectrum of the Lindelöf property.
definition
\( T\{is anti-lindeloef\} \equiv T\{is anti-\}(\lambda T.\ ((\bigcup T)\text{ is lindeloef in }T)) \)
end
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 (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 \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge (\bigcup T)\setminus D \in T) \)
Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma (in topology0) fin_union_cl_is_cl:
assumes \( N \in \text{FinPow}(\{D\in Pow(\bigcup T).\ D \text{ is closed in } T\}) \)
shows \( (\bigcup N) \text{ is closed in } T \)Definition of CoCardinal:
\( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)
lemma empty_open:
assumes \( T \text{ is a topology } \)
shows \( \emptyset \in T \)Definition of Cofinite:
\( CoFinite X \equiv \text{CoCardinal}(X,nat) \)
lemma closed_sets_cocardinal:
assumes \( T\neq 0 \)
shows \( D \text{ is closed in } \text{CoCardinal}(X,T) \longleftrightarrow (D\in Pow(X) \wedge D\prec T) \vee D=X \) lemma union_cocardinal:
assumes \( T\neq 0 \)
shows \( \bigcup \text{CoCardinal}(X,T) = X \) lemma (in topology0) T1_cocardinal_coarser: shows \( (T \text{ is }T_1) \longleftrightarrow (CoFinite (\bigcup T))\subseteq T \)
lemma order_cocardinal_top:
assumes \( Q1\preceq Q2 \)
shows \( \text{CoCardinal}(X,Q1) \subseteq \text{CoCardinal}(X,Q2) \) theorem topology0_CoCardinal:
assumes \( \text{InfCard}(T) \)
shows \( topology0(\text{CoCardinal}(X,T)) \)Definition of FilterConverges:
\( \mathfrak{F} \text{ is a filter on }\bigcup T \Longrightarrow \mathfrak{F} \rightarrow _Fx \equiv \)
\( x\in \bigcup T \wedge (\{U\in Pow(\bigcup T).\ x\in int(U)\} \subseteq \mathfrak{F} ) \)
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 (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
Definition of IsFilter:
\( \mathfrak{F} \text{ is a filter on } X \equiv (\emptyset \notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge \mathfrak{F} \subseteq Pow(X) \wedge \)
\( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)
theorem filter_of_net_is_filter:
assumes \( N \text{ is a net on } X \)
shows \( (Filter N.\ .\ X) \text{ is a filter on } X \) and \( \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\} \text{ is a base filter } (Filter N.\ .\ X) \) theorem (in topology0) net_conver_filter_of_net_conver:
assumes \( N \text{ is a net on } \bigcup T \) and \( N \rightarrow _N x \)
shows \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \) lemma (in topology0) T2_imp_unique_limit_filter:
assumes \( T \text{ is }T_2 \), \( \mathfrak{F} \text{ is a filter on }\bigcup T \), \( \mathfrak{F} \rightarrow _F x \), \( \mathfrak{F} \rightarrow _F y \)
shows \( x=y \) lemma (in topology0) neigh_filter:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
shows \( \text{Neigh} \text{ is a filter on }\bigcup T \) and \( \text{Neigh} \rightarrow _F x \) lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
Definition of SatisfiesFilterBase:
\( C \text{ satisfies the filter base condition } \equiv (\forall A\in C.\ \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B) \wedge C\neq 0 \wedge 0\notin C \)
theorem base_unique_filter_set2:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( ((C \text{ is a base filter } \mathfrak{F} ) \wedge \bigcup \mathfrak{F} =X) \longleftrightarrow \mathfrak{F} =\{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) theorem basic_filter:
assumes \( C \text{ is a base filter } \mathfrak{F} \)
shows \( (C \text{ satisfies the filter base condition }) \longleftrightarrow (\mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} ) \) theorem (in topology0) convergence_filter_base2:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \)
shows \( \mathfrak{F} \rightarrow _F x \) theorem (in topology0) filter_conver_net_of_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( \mathfrak{F} \rightarrow _F x \)
shows \( (\text{Net}(\mathfrak{F} )) \rightarrow _N x \) theorem net_of_filter_is_net:
assumes \( \mathfrak{F} \text{ is a filter on } X \)
shows \( (\text{Net}(\mathfrak{F} )) \text{ is a net on } X \) lemma (in topology0) unique_limit_filter_imp_T2:
assumes \( \forall x\in \bigcup T.\ \forall y\in \bigcup T.\ \forall \mathfrak{F} .\ ((\mathfrak{F} \text{ is a filter on }\bigcup T) \wedge (\mathfrak{F} \rightarrow _F x) \wedge (\mathfrak{F} \rightarrow _F y)) \longrightarrow x=y \)
shows \( T \text{ is }T_2 \) lemma lim_filter_top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \) and \( x\in \bigcup \mathfrak{F} \)
shows \( \mathfrak{F} \rightarrow _F x\text{ in }(\mathfrak{F} \cup \{0\}) \) lemma topology0_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( topology0(\mathfrak{F} \cup \{0\}) \)Definition of isT4:
\( T\{is T_4\} \equiv (T\text{ is }T_1) \wedge (T\text{ is normal }) \)
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)) \)
Definition of IsRegular:
\( T \text{ is regular } \equiv \forall D.\ D \text{ is closed in } T \longrightarrow (\forall x\in \bigcup T-D.\ \exists U\in T.\ \exists V\in T.\ D\subseteq U\wedge x\in V\wedge U\cap V=0) \)
Definition of isT3:
\( T \text{ is }T_3 \equiv (T \text{ is regular }) \wedge T \text{ is }T_0 \)
lemma T1_is_T0:
assumes \( T \text{ is }T_1 \)
shows \( T \text{ is }T_0 \) lemma (in topology0) Top_3_L9:
assumes \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \) lemma (in topology0) Top_3_L13:
assumes \( B \text{ is closed in } T \), \( A\subseteq B \)
shows \( cl(A) \subseteq B \) lemma (in topology0) regular_imp_exist_clos_neig:
assumes \( T\text{ is regular } \) and \( U\in T \) and \( x\in U \)
shows \( \exists V\in T.\ x\in V \wedge cl(V)\subseteq U \) lemma (in topology0) exist_clos_neig_imp_regular:
assumes \( \forall x\in \bigcup T.\ \forall U\in T.\ x\in U \longrightarrow (\exists V\in T.\ x\in V\wedge cl(V)\subseteq U) \)
shows \( T\text{ is regular } \)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 IsCompact:
\( K \text{ is compact in } T \equiv (K \subseteq \bigcup T \wedge \)
\( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in \text{FinPow}(M).\ K \subseteq \bigcup N))) \)
theorem finite_choice:
assumes \( n\in nat \)
shows \( \text{ the axiom of } n \text{ choice holds } \)Definition of AxiomCardinalChoiceGen:
\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) theorem surj_fun_inv_2:
assumes \( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)
shows \( B\preceq A \) lemma (in topology0) fin_inter_open_open:
assumes \( N\neq 0 \), \( N \in \text{FinPow}(T) \)
shows \( \bigcap N \in T \) theorem (in topology0) T2_compact_point:
assumes \( T\text{ is }T_2 \), \( A\text{ is compact in }T \), \( x\in \bigcup T \), \( x\notin A \)
shows \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge x\in V \wedge U\cap V=0 \) lemma Compact_is_card_nat: shows \( K\text{ is compact in }T \longleftrightarrow (K\text{ is compact of cardinal } nat \{in\}T) \)
theorem compact_closed:
assumes \( K \text{ is compact of cardinal } Q\text{ in }T \) and \( R \text{ is closed in } T \)
shows \( (K\cap R) \text{ is compact of cardinal } Q\text{ in }T \) theorem (in topology0) T2_compact_compact:
assumes \( T\text{ is }T_2 \), \( A\text{ is compact in }T \), \( B\text{ is compact in }T \), \( A\cap B=0 \)
shows \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge B\subseteq V \wedge U\cap V=0 \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
theorem regular_here:
assumes \( T\text{ is regular } \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is regular } \)Definition of IsHer:
\( P \text{ is hereditary } \equiv \forall T.\ T\text{ is a topology } \wedge P(T) \longrightarrow (\forall A\in Pow(\bigcup T).\ P(T\text{ restricted to }A)) \)
theorem T1_here:
assumes \( T\text{ is }T_1 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_1 \) lemma here_and:
assumes \( P \text{ is hereditary } \), \( Q \text{ is hereditary } \)
shows \( (\lambda T.\ P(T) \wedge Q(T)) \text{ is hereditary } \) corollary here_T1: shows \( isT1 \text{ is hereditary } \)
corollary here_regular: shows \( IsRegular \text{ is hereditary } \)
lemma T3_def_alt: shows \( T \text{ is }T_3 \longleftrightarrow (T \text{ is regular }) \wedge T \text{ is }T_1 \)
lemma T2_here:
assumes \( T\text{ is }T_2 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_2 \)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))) \)
lemma T0_here:
assumes \( T\text{ is }T_0 \), \( A\in Pow(\bigcup T) \)
shows \( (T\text{ restricted to }A)\text{ is }T_0 \)Definition of Spec:
\( Spec \equiv \{I\in \mathcal{I} .\ I\triangleleft _pR\} \)
lemma equipollent_spect:
assumes \( A\approx B \), \( B \text{ is in the spectrum of } P \)
shows \( A \text{ is in the spectrum of } P \) theorem top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( (\mathfrak{F} \cup \{0\}) \text{ is a topology } \) lemma T3_is_T2:
assumes \( T \text{ is }T_3 \)
shows \( T \text{ is }T_2 \) lemma (in topology0) T4_is_T3:
assumes \( T\{is T_4\} \)
shows \( T\text{ is }T_3 \) corollary filter_T2_imp_card1:
assumes \( (\mathfrak{F} \cup \{0\}) \text{ is }T_2 \), \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \), \( x\in \bigcup \mathfrak{F} \)
shows \( \bigcup \mathfrak{F} =\{x\} \) lemma T2_is_T1:
assumes \( T \text{ is }T_2 \)
shows \( T \text{ is }T_1 \) lemma P_imp_Q_spec_inv:
assumes \( \forall T.\ T\text{ is a topology } \longrightarrow (Q(T) \longrightarrow P(T)) \), \( A \text{ is in the spectrum of } Q \)
shows \( A \text{ is in the spectrum of } P \) theorem T4_spectrum: shows \( (A \text{ is in the spectrum of } isT4) \longleftrightarrow A \preceq 1 \)
lemma Pow_is_top: shows \( Pow(X) \text{ is a topology } \)
Definition of IsCompactOfCard:
\( K\text{ is compact of cardinal } Q\{in\}T \equiv (\text{Card}(Q) \wedge K \subseteq \bigcup T \wedge \)
\( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in Pow(M).\ K \subseteq \bigcup N \wedge N\prec Q))) \)
lemma Card_less_csucc_eq_le:
assumes \( \text{Card}(m) \)
shows \( A \prec \text{csucc}(m) \longleftrightarrow A \preceq m \)Definition of IsAbaseFor:
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
Definition of IsSecondOfCard:
\( (T \text{ is of second type of cardinal }Q) \equiv (\exists B.\ (B \text{ is a base for } T) \wedge (B \prec Q)) \)
theorem compact_coarser:
assumes \( T1\subseteq T \) and \( \bigcup T1=\bigcup T \) and \( (K)\text{ is compact of cardinal }Q\{in\}T \)
shows \( (K)\text{ is compact of cardinal }Q\{in\}T1 \) theorem Q_disc_comp_csuccQ_eq_Q_choice_csuccQ:
assumes \( \text{InfCard}(Q) \)
shows \( (Q\text{ is compact of cardinal }\text{csucc}(Q)\{in\}(Pow(Q))) \longleftrightarrow (\text{ the axiom of }Q\text{ choice holds for subsets }(Pow(Q))) \) lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
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) \)
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 \) lemma inj_bij_range:
assumes \( f \in \text{inj}(A,B) \)
shows \( f \in \text{bij}(A,\text{range}(f)) \) theorem eqpoll_iff_spec:
assumes \( A\approx B \)
shows \( (B \text{ is in the spectrum of } P) \longleftrightarrow (A \text{ is in the spectrum of } P) \) theorem anti_here: shows \( (ANTI(P))\text{ is hereditary } \)
theorem (in topology0) her_P_imp_anti2P:
assumes \( P\text{ is hereditary } \), \( P(T) \)
shows \( T\{is anti-\}ANTI(P) \) theorem T0_spectrum: shows \( (A \text{ is in the spectrum of } isT0) \longleftrightarrow A \preceq 1 \)
lemma indiscrete_spectrum: shows \( (A \text{ is in the spectrum of }(\lambda T.\ T=\{0,\bigcup T\})) \longleftrightarrow A\preceq 1 \)
theorem T1_spectrum: shows \( (A \text{ is in the spectrum of } isT1) \longleftrightarrow A \preceq 1 \)
Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
theorem anti_T1: shows \( (T\{is anti-\}isT1) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
theorem (in topology0) eq_spect_rev_imp_anti:
assumes \( \forall T.\ T\text{ is a topology } \longrightarrow P(T) \longrightarrow Q(T) \), \( \forall A.\ (A\text{ is in the spectrum of }Q) \longrightarrow (A\text{ is in the spectrum of }P) \) and \( T\{is anti-\}Q \)
shows \( T\{is anti-\}P \) theorem T3_spectrum: shows \( (A \text{ is in the spectrum of } isT3) \longleftrightarrow A \preceq 1 \)
theorem (in topology0) anti_T4: shows \( (T\{is anti-\}isT4) \longleftrightarrow ( \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\})) \)
theorem T2_spectrum: shows \( (A \text{ is in the spectrum of } isT2) \longleftrightarrow A \preceq 1 \)
lemma ord_linear_subset:
assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)
shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \) lemma linord_spectrum: shows \( (A\text{ is in the spectrum of }(\lambda T.\ \text{IsLinOrder}(T,\{\langle U,V\rangle \in Pow(\bigcup T)\times Pow(\bigcup T).\ U\subseteq V\}))) \longleftrightarrow A\preceq 1 \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
