theory Topology_ZF_properties imports Topology_ZF_examples Topology_ZF_examples_1
begin
This theory deals with topological properties which make use of cardinals.
Properties of compactness
In this section we study generalizations of compactness.
It is already defined what is a compact topological space, but the is a generalization which may be useful sometimes.
definition
\( 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))) \)
The usual compact property is the one defined over the cardinal of the natural numbers.
lemma Compact_is_card_nat:
shows \( K\text{ is compact in }T \longleftrightarrow (K\text{ is compact of cardinal } nat \{in\}T) \)proof{
}
}
{
}
}
qed
assume \( K\text{ is compact in }T \)
then have sub: \( K \subseteq \bigcup T \) and reg: \( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in \text{FinPow}(M).\ K \subseteq \bigcup N)) \) using IsCompact_def
{
fix \( M \)
assume \( M\in Pow(T) \), \( K\subseteq \bigcup M \)
with reg obtain \( N \) where \( N\in \text{FinPow}(M) \), \( K\subseteq \bigcup N \)
then have \( Finite(N) \) using FinPow_def
then obtain \( n \) where A: \( n\in nat \), \( N \approx n \) using Finite_def
from A(1) have \( n\prec nat \) using n_lesspoll_nat
with A(2) have \( N\preceq nat \) using lesspoll_def, eq_lepoll_trans
moreover {
}
assume \( N \approx nat \)
then have \( nat \approx N \) using eqpoll_sym
with A(2) have \( nat \approx n \) using eqpoll_trans
then have \( n \approx nat \) using eqpoll_sym
with \( n\prec nat \) have \( False \) using lesspoll_def
then have \( \neg (N \approx nat) \)
moreover note \( K\subseteq \bigcup N \), \( N\in \text{FinPow}(M) \)
ultimately have \( N\prec nat \), \( K\subseteq \bigcup N \), \( N\in Pow(M) \) using lesspoll_def, FinPow_def
hence \( (\exists N \in Pow(M).\ K \subseteq \bigcup N \wedge N\prec nat) \)
with sub show \( K\text{ is compact of cardinal } nat \{in\}T \) using IsCompactOfCard_def, Card_nat
assume \( (K\text{ is compact of cardinal } nat \{in\}T) \)
then have sub: \( K\subseteq \bigcup T \) and reg: \( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in Pow(M).\ K \subseteq \bigcup N \wedge N\prec nat)) \) using IsCompactOfCard_def
{
fix \( M \)
assume \( M\in Pow(T) \), \( K\subseteq \bigcup M \)
with reg have \( (\exists N \in Pow(M).\ K \subseteq \bigcup N \wedge N\prec nat) \)
then obtain \( N \) where \( N\in Pow(M) \), \( K\subseteq \bigcup N \), \( N\prec nat \)
then have \( N\in \text{FinPow}(M) \), \( K\subseteq \bigcup N \) using lesspoll_nat_is_Finite, FinPow_def
hence \( \exists N\in \text{FinPow}(M).\ K\subseteq \bigcup N \)
with sub show \( K\text{ is compact in }T \) using IsCompact_def
Another property of this kind widely used is the Lindeloef property; it is the one on the successor of the natural numbers.
definition
\( K \text{ is lindeloef in } T \equiv K\text{ is compact of cardinal }\text{csucc}(nat)\{in\}T \)
It would be natural to think that every countable set with any topology is Lindeloef; but this statement is not provable in ZF. The reason is that to build a subcover, most of the time we need to \emph{choose} sets from an infinite collection which cannot be done in ZF. Additional axioms are needed, but strictly weaker than the axiom of choice.
However, if the topology has not many open sets, then the topological space is indeed compact.
theorem card_top_comp:
assumes \( \text{Card}(Q) \), \( T\prec Q \), \( K\subseteq \bigcup T \)
shows \( (K)\text{ is compact of cardinal }Q\{in\}T \)proof{
}
fix \( M \)
assume M: \( M\subseteq T \), \( K\subseteq \bigcup M \)
from M(1), assms(2) have \( M\prec Q \) using subset_imp_lepoll, lesspoll_trans1
with M(2) have \( \exists N\in Pow(M).\ K\subseteq \bigcup N \wedge N\prec Q \)
with assms(1,3) show \( thesis \) unfolding IsCompactOfCard_def
qed
The union of two compact sets, is compact; of any cardinality.
theorem union_compact:
assumes \( K\text{ is compact of cardinal }Q\{in\}T \), \( K1\text{ is compact of cardinal }Q\{in\}T \), \( \text{InfCard}(Q) \)
shows \( (K \cup K1)\text{ is compact of cardinal }Q\{in\}T \)proof from assms(1) have I: \( \text{Card}(Q) \) unfolding IsCompactOfCard_def
{
fix \( x \)
assume \( x\in K\cup K1 \)
then have \( x\in \bigcup T \) using assms(1,2) unfolding IsCompactOfCard_def
then have II: \( K\cup K1 \subseteq \bigcup T \)
{
fix \( M \)
assume \( M\subseteq T \), \( K\cup K1\subseteq \bigcup M \)
then have \( K\subseteq \bigcup M \), \( K1\subseteq \bigcup M \)
with \( M\subseteq T \) have \( \exists N\in Pow(M).\ K \subseteq \bigcup N \wedge N \prec Q \), \( \exists N\in Pow(M).\ K1 \subseteq \bigcup N \wedge N \prec Q \) using assms unfolding IsCompactOfCard_def
then obtain \( NK \) \( NK1 \) where \( NK\in Pow(M) \), \( NK1\in Pow(M) \), \( K \subseteq \bigcup NK \), \( K1 \subseteq \bigcup NK1 \), \( NK \prec Q \), \( NK1 \prec Q \)
then have \( NK\cup NK1 \prec Q \), \( K\cup K1\subseteq \bigcup (NK\cup NK1) \), \( NK\cup NK1\in Pow(M) \) using assms(3), less_less_imp_un_less
then have \( \exists N\in Pow(M).\ K\cup K1\subseteq \bigcup N \wedge N\prec Q \)
with I, II show \( thesis \) unfolding IsCompactOfCard_def
qed
If a set is compact of cardinality Q for some topology, it is compact of cardinality Q for every coarser topology.
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 \)proof{
}
fix \( M \)
assume AS: \( M\in Pow(T1) \), \( K\subseteq \bigcup M \)
then have \( M\in Pow(T) \), \( K\subseteq \bigcup M \) using assms(1)
then have \( \exists N\in Pow(M).\ K\subseteq \bigcup N\wedge N\prec Q \) using assms(3) unfolding IsCompactOfCard_def
then show \( (K)\text{ is compact of cardinal }Q\{in\}T1 \) using assms(3,2) unfolding IsCompactOfCard_def
qed
If some set is compact for some cardinal, it is compact for any greater cardinal.
theorem compact_greater_card:
assumes \( Q\preceq Q1 \) and \( (K)\text{ is compact of cardinal }Q\{in\}T \) and \( \text{Card}(Q1) \)
shows \( (K)\text{ is compact of cardinal }Q1\{in\}T \)proof{
}
fix \( M \)
assume AS: \( M\in Pow(T) \), \( K\subseteq \bigcup M \)
then have \( \exists N\in Pow(M).\ K\subseteq \bigcup N\wedge N\prec Q \) using assms(2) unfolding IsCompactOfCard_def
then have \( \exists N\in Pow(M).\ K\subseteq \bigcup N\wedge N\prec Q1 \) using assms(1), lesspoll_trans2 unfolding IsCompactOfCard_def
then show \( thesis \) using assms(2,3) unfolding IsCompactOfCard_def
qed
A closed subspace of a compact space of any cardinality, is also compact of the same cardinality.
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 \)proof{
}
fix \( M \)
assume AS: \( M\in Pow(T) \), \( K\cap R\subseteq \bigcup M \)
have \( \bigcup T-R\in T \) using assms(2), IsClosed_def
have \( K-R\subseteq (\bigcup T-R) \) using assms(1), IsCompactOfCard_def
have \( K\subseteq \bigcup (M \cup \{\bigcup T-R\}) \) and \( M \cup \{\bigcup T-R\}\in Pow(T) \)proof
{
}
fix \( x \)
assume \( x\in K \)
have \( x\in R\vee x\notin R \)
with \( x\in K \) have \( x\in K\cap R\vee x\in K-R \)
with AS(2), \( K-R\subseteq (\bigcup T-R) \) have \( x\in \bigcup M\vee x\in (\bigcup T-R) \)
then have \( x\in \bigcup (M \cup \{\bigcup T-R\}) \)
then show \( K \subseteq \bigcup (M \cup \{\bigcup T-R\}) \)
from AS(1), \( \bigcup T-R\in T \) show \( M\cup \{\bigcup T-R\}\in Pow(T) \)
qed
with assms(1) have \( \exists N\in Pow(M\cup \{\bigcup T-R\}).\ K \subseteq \bigcup N \wedge N \prec Q \) unfolding IsCompactOfCard_def
then obtain \( N \) where cub: \( N\in Pow(M\cup \{\bigcup T-R\}) \), \( K\subseteq \bigcup N \), \( N\prec Q \)
have \( N-\{\bigcup T-R\}\in Pow(M) \), \( K\cap R\subseteq \bigcup (N-\{\bigcup T-R\}) \), \( N-\{\bigcup T-R\}\prec Q \)proof
{
}
}
fix \( x \)
assume \( x\in N\setminus \{\bigcup T-R\} \)
then have \( x:M \) using cub(1)
then show \( N-\{\bigcup T-R\} \subseteq M \)
{
fix \( x \)
assume \( x\in K\cap R \)
then have \( x\notin \bigcup T-R \), \( x\in K \)
then have \( x\in \bigcup (N-\{\bigcup T-R\}) \) using cub(2)
then show \( K\cap R \subseteq \bigcup (N-\{\bigcup T-R\}) \)
have \( N-\{\bigcup T-R\}\subseteq N \)
with cub(3) show \( N-\{\bigcup T-R\}\prec Q \) using subset_imp_lepoll, lesspoll_trans1
qed
then have \( \exists N\in Pow(M).\ K\cap R\subseteq \bigcup N \wedge N\prec Q \)
then have \( \forall M\in Pow(T).\ (K \cap R \subseteq \bigcup M \longrightarrow (\exists N\in Pow(M).\ K \cap R \subseteq \bigcup N \wedge N \prec Q)) \)
then show \( thesis \) using IsCompactOfCard_def, assms(1)
qed
Properties of numerability
The properties of numerability deal with cardinals of some sets built from the topology. The properties which are normally used are the ones related to the cardinal of the natural numbers or its successor.
A topology is of first type of cardinal Q if every point has a neighborhood base of cardinality less than Q.
definition
\( (T \text{ is of first type of cardinal } Q) \equiv \forall x\in \bigcup T.\ (\exists B.\ (B \text{ is a base for } T) \wedge (\{b\in B.\ x\in b\} \prec Q)) \)
A topology is of second type of cardinal Q if the whole topology has a base of cardinality less than Q.
definition
\( (T \text{ is of second type of cardinal }Q) \equiv (\exists B.\ (B \text{ is a base for } T) \wedge (B \prec Q)) \)
A topology is separable of cardinal Q if it has a dense subset of cardinality less than Q.
definition
\( T\text{ is separable of cardinal }Q\equiv \exists U\in Pow(\bigcup T).\ \text{Closure}(U,T)=\bigcup T \wedge U\prec Q \)
A topology is first countable if it is of first type of cardinal \( \text{csucc}(nat) \), i.e., every point has a countable neighborhood base.
definition
\( (T \text{ is first countable }) \equiv T \text{ is of first type of cardinal } \text{csucc}(nat) \)
A topology is second countable if it is of second type of cardinal \( \text{csucc}(nat) \), i.e., it has a countable base.
definition
\( (T \text{ is second countable }) \equiv (T \text{ is of second type of cardinal }\text{csucc}(nat)) \)
A topology is separable if it has a countable dense subset.
definition
\( T\text{ is separable }\equiv T\text{ is separable of cardinal }\text{csucc}(nat) \)
If a set is of second type of cardinal Q, then it is of first type of that same cardinal.
theorem second_imp_first:
assumes \( T\text{ is of second type of cardinal }Q \)
shows \( T\text{ is of first type of cardinal }Q \)proof from assms have \( \exists B.\ (B \text{ is a base for } T) \wedge (B \prec Q) \) using IsSecondOfCard_def
then obtain \( B \) where base: \( (B \text{ is a base for } T) \wedge (B \prec Q) \)
{
fix \( x \)
assume \( x\in \bigcup T \)
have \( \{b\in B.\ x\in b\}\subseteq B \)
then have \( \{b\in B.\ x\in b\}\preceq B \) using subset_imp_lepoll
with base have \( \{b\in B.\ x\in b\}\prec Q \) using lesspoll_trans1
with base have \( (B \text{ is a base for } T) \wedge \{b\in B.\ x\in b\}\prec Q \)
then have \( \forall x\in \bigcup T.\ \exists B.\ (B \text{ is a base for } T) \wedge \{b\in B.\ x\in b\}\prec Q \)
then show \( thesis \) using IsFirstOfCard_def
qed
A set is dense iff it intersects all non-empty, open sets of the topology.
lemma dense_int_open:
assumes \( T\text{ is a topology } \) and \( A\subseteq \bigcup T \)
shows \( \text{Closure}(A,T)=\bigcup T \longleftrightarrow (\forall U\in T.\ U\neq 0 \longrightarrow A\cap U\neq 0) \)proof assume AS: \( \text{Closure}(A,T)=\bigcup T \)
{
fix \( U \)
assume Uopen: \( U\in T \) and \( U\neq 0 \)
then have \( U\cap \bigcup T\neq 0 \)
with AS have \( U\cap \text{Closure}(A,T) \neq 0 \)
with assms, Uopen have \( U\cap A\neq 0 \) using cl_inter_neigh, topology0_def
then show \( \forall U\in T.\ U\neq 0 \longrightarrow A\cap U\neq 0 \)
next
assume AS: \( \forall U\in T.\ U\neq 0 \longrightarrow A\cap U\neq 0 \)
{
fix \( x \)
assume A: \( x\in \bigcup T \)
then have \( \forall U\in T.\ x\in U \longrightarrow U\cap A\neq 0 \) using AS
with assms, A have \( x\in \text{Closure}(A,T) \) using inter_neigh_cl, topology0_def
then have \( \bigcup T\subseteq \text{Closure}(A,T) \)
with assms show \( \text{Closure}(A,T)=\bigcup T \) using Top_3_L11(1), topology0_def
qed
Relations between numerability properties and choice principles
It is known that some statements in topology aren't just derived from choice axioms, but also equivalent to them. Here is an example
The following are equivalent: \begin{itemize} \item Every topological space of second cardinality \( \text{csucc}(Q) \) is separable of cardinality \( \text{csucc}(Q) \). \item The axiom of Q choice. \end{itemize}
In the article \cite{HH1} there is a proof of this statement for Q\(=\mathbb{N}\), with more equivalences.
If a topology is of second type of cardinal \( \text{csucc}(Q) \), then it is separable of the same cardinal. This result makes use of the axiom of choice for the cardinal Q on subsets of \( \bigcup T \).
theorem Q_choice_imp_second_imp_separable:
assumes \( T\text{ is of second type of cardinal }\text{csucc}(Q) \) and \( \text{ the axiom of } Q \text{ choice holds for subsets } \bigcup T \) and \( T\text{ is a topology } \)
shows \( T\text{ is separable of cardinal }\text{csucc}(Q) \)proof from assms(1) have \( \exists B.\ (B \text{ is a base for } T) \wedge (B \prec \text{csucc}(Q)) \) using IsSecondOfCard_def
then obtain \( B \) where base: \( (B \text{ is a base for } T) \wedge (B \prec \text{csucc}(Q)) \)
let \( N = \lambda b\in B.\ b \)
let \( B = B-\{0\} \)
have \( B\subseteq B \)
with base have prec: \( B\prec \text{csucc}(Q) \) using subset_imp_lepoll, lesspoll_trans1
from base have baseOpen: \( \forall b\in B.\ Nb\in T \) using base_sets_open
from assms(2) have car: \( \text{Card}(Q) \) and reg: \( (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq \bigcup T)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \) using AxiomCardinalChoice_def
then have \( (B \preceq Q \wedge (\forall t\in B.\ Nt\neq 0 \wedge Nt\subseteq \bigcup T)) \longrightarrow (\exists f.\ f:\text{Pi}(B,\lambda t.\ Nt) \wedge (\forall t\in B.\ ft\in Nt)) \)
with prec have \( (\forall t\in B.\ Nt\subseteq \bigcup T) \longrightarrow (\exists f.\ f:\text{Pi}(B,\lambda t.\ Nt) \wedge (\forall t\in B.\ ft\in Nt)) \) using Card_less_csucc_eq_le, car
with baseOpen have \( \exists f.\ f:\text{Pi}(B,\lambda t.\ Nt) \wedge (\forall t\in B.\ ft\in Nt) \)
then obtain \( f \) where f: \( f:\text{Pi}(B,\lambda t.\ Nt) \) and f2: \( \forall t\in B.\ ft\in Nt \)
{
fix \( U \)
assume \( U\in T \) and \( U\neq 0 \)
then obtain \( b \) where A1: \( b\in B \) and \( b\subseteq U \) using Top_1_2_L1, base
with f2 have \( fb\in U \)
with A1 have \( \{fb.\ b\in B\}\cap U\neq 0 \)
then have r: \( \forall U\in T.\ U\neq 0 \longrightarrow \{fb.\ b\in B\}\cap U\neq 0 \)
have I: \( \{fb.\ b\in B\}\subseteq \bigcup T \) using f2, baseOpen
from this, r have II: \( \text{Closure}(\{fb.\ b\in B\},T)=\bigcup T \) using dense_int_open, assms(3)
have ffun: \( f:B\rightarrow \text{range}(f) \) using f, range_of_fun
then have R: \( \bigwedge b.\ b:B \Longrightarrow fb\in \text{range}(f) \) using apply_rangeI
from ffun have \( f\in \text{surj}(B,\text{range}(f)) \) using fun_is_surj
then have des1: \( \text{range}(f)\preceq B \) using surj_fun_inv_2, prec, Card_less_csucc_eq_le, car, Card_is_Ord
with R have \( \{fb.\ b\in B\}\subseteq \text{range}(f) \)
then have \( \{fb.\ b\in B\}\preceq \text{range}(f) \) using subset_imp_lepoll
with des1 have \( \{fb.\ b\in B\}\preceq B \) using lepoll_trans
with prec have \( \{fb.\ b\in B\}\prec \text{csucc}(Q) \) using lesspoll_trans1
with I, II show \( thesis \) using IsSeparableOfCard_def
qed
The next theorem resolves that the axiom of Q choice for subsets of \( \bigcup T \) is necessary for second type spaces to be separable of the same cardinal \( \text{csucc}(Q) \).
theorem second_imp_separable_imp_Q_choice:
assumes \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow (T\text{ is separable of cardinal }\text{csucc}(Q)) \) and \( \text{Card}(Q) \)
shows \( \text{ the axiom of } Q \text{ choice holds } \)proof{
}
}
}
}
}
fix \( N \) \( M \)
assume AS: \( M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0) \)
then obtain \( h \) where inj: \( h\in \text{inj}(M,Q) \) using lepoll_def
then have bij: \( converse(h):\text{bij}(\text{range}(h),M) \) using inj_bij_range, bij_converse_bij
let \( T = \{(N(converse(h)i))\times \{i\}.\ i\in \text{range}(h)\} \)
{
fix \( j \)
assume AS2: \( j\in \text{range}(h) \)
from bij have \( converse(h):\text{range}(h)\rightarrow M \) using bij_def, inj_def
with AS2 have \( converse(h)j\in M \)
with AS have \( N(converse(h)j)\neq 0 \)
then have \( (N(converse(h)j))\times \{j\}\neq 0 \)
then have noEmpty: \( 0\notin T \)
moreover {
}
fix \( A \) \( B \)
assume AS2: \( A\in T \), \( B\in T \), \( A\cap B\neq 0 \)
then obtain \( j \) \( t \) where A_def: \( A=N(converse(h)j)\times \{j\} \) and B_def: \( B=N(converse(h)t)\times \{t\} \) and Range: \( j\in \text{range}(h) \), \( t\in \text{range}(h) \)
from AS2(3) obtain \( x \) where \( x\in A\cap B \)
with A_def, B_def have \( j=t \)
with A_def, B_def have \( A=B \)
then have \( (\forall A\in T.\ \forall B\in T.\ A=B\vee A\cap B=0) \)
ultimately have Part: \( T \text{ is a partition of } \bigcup T \) unfolding IsAPartition_def
let \( \tau = PTopology \bigcup T T \)
from Part have top: \( \tau \text{ is a topology } \) and base: \( T \text{ is a base for }\tau \) using Ptopology_is_a_topology
let \( f = \{\langle i,(N(converse(h)i))\times \{i\}\rangle .\ i\in \text{range}(h)\} \)
from functionI have \( (\bigwedge x y z.\ \langle x,y\rangle \in f \Longrightarrow \langle x,z\rangle \in f \Longrightarrow y=z) \Longrightarrow function(f) \)
then have \( f:\text{range}(h)\rightarrow T \) using Pi_def
then have \( f\in \text{surj}(\text{range}(h),T) \) unfolding surj_def using apply_equality
moreover
have \( \text{range}(h)\subseteq Q \) using inj unfolding inj_def, range_def, domain_def, Pi_def
moreover have \( f \in \text{surj}(\text{range}(h), T) \Longrightarrow \text{range}(h) \subseteq Q \Longrightarrow Ord(Q) \Longrightarrow T \preceq \text{range}(h) \) using surj_fun_inv
ultimately have \( T\preceq Q \) using assms(2), Card_is_Ord, lepoll_trans, subset_imp_lepoll
then have \( T\prec \text{csucc}(Q) \) using Card_less_csucc_eq_le, assms(2)
with base have \( (\tau \text{ is of second type of cardinal }\text{csucc}(Q)) \) using IsSecondOfCard_def
with top have \( \tau \text{ is separable of cardinal }\text{csucc}(Q) \) using assms(1)
then obtain \( D \) where sub: \( D\in Pow(\bigcup \tau ) \) and clos: \( \text{Closure}(D,\tau )=\bigcup \tau \) and cardd: \( D\prec \text{csucc}(Q) \) using IsSeparableOfCard_def
then have \( D\preceq Q \) using Card_less_csucc_eq_le, assms(2)
then obtain \( r \) where r: \( r\in \text{inj}(D,Q) \) using lepoll_def
then have bij2: \( converse(r):\text{bij}(\text{range}(r),D) \) using inj_bij_range, bij_converse_bij
then have surj2: \( converse(r):\text{surj}(\text{range}(r),D) \) using bij_def
let \( R = \lambda i\in \text{range}(h).\ \{j\in \text{range}(r).\ converse(r)j\in ((N(converse(h)i))\times \{i\})\} \)
{
fix \( i \)
assume AS: \( i\in \text{range}(h) \)
then have T: \( (N(converse(h)i))\times \{i\}\in T \)
then have P: \( (N(converse(h)i))\times \{i\}\in \tau \) using base unfolding IsAbaseFor_def
with top, sub, clos have \( \forall U\in \tau .\ U\neq 0 \longrightarrow D\cap U\neq 0 \) using dense_int_open
with P have \( (N(converse(h)i))\times \{i\}\neq 0 \longrightarrow D\cap (N(converse(h)i))\times \{i\}\neq 0 \)
with T, noEmpty have \( D\cap (N(converse(h)i))\times \{i\}\neq 0 \)
then obtain \( x \) where \( x\in D \) and px: \( x\in (N(converse(h)i))\times \{i\} \)
with surj2 obtain \( j \) where \( j\in \text{range}(r) \) and \( converse(r)j=x \) unfolding surj_def
with px have \( j\in \{j\in \text{range}(r).\ converse(r)j\in ((N(converse(h)i))\times \{i\})\} \)
then have \( Ri\neq 0 \) using beta_if, AS
then have nonE: \( \forall i\in \text{range}(h).\ Ri\neq 0 \)
{
fix \( i \) \( j \)
assume i: \( i\in \text{range}(h) \) and j: \( j\in Ri \)
from j, i have \( converse(r)j\in ((N(converse(h)i))\times \{i\}) \) using beta_if
then have pp: \( \forall i\in \text{range}(h).\ \forall j\in Ri.\ converse(r)j\in ((N(converse(h)i))\times \{i\}) \)
let \( E = \{\langle m,\text{fst}(converse(r)(\mu j.\ j\in R(hm)))\rangle .\ m\in M\} \)
have ff: \( function(E) \) unfolding function_def
moreover {
}
}
ultimately have thesis1: \( \forall m\in M.\ Em\in (N(m)) \) using function_apply_equality
{
fix \( m \)
assume M: \( m\in M \)
with inj have hm: \( hm\in \text{range}(h) \) using apply_rangeI, inj_def
{
fix \( j \)
assume \( j\in R(hm) \)
with hm have \( j\in \text{range}(r) \) using beta_if
from r have \( r:\text{surj}(D,\text{range}(r)) \) using fun_is_surj, inj_def
with \( j\in \text{range}(r) \) obtain \( d \) where \( d\in D \) and \( rd=j \) using surj_def
then have \( j\in Q \) using r, inj_def
then have subcar: \( R(hm)\subseteq Q \)
from nonE, hm obtain \( ee \) where P: \( ee\in R(hm) \)
with subcar have \( ee\in Q \)
then have ord: \( Ord(ee) \) using assms(2), Card_is_Ord, Ord_in_Ord
have \( ee\in R(hm) \Longrightarrow Ord(ee) \Longrightarrow (\mu j.\ j\in R(hm))\in R(hm) \) using LeastI
with P, ord have \( (\mu j.\ j\in R(hm))\in R(hm) \)
with pp, hm have \( converse(r)(\mu j.\ j\in R(hm))\in ((N(converse(h)(hm)))\times \{(hm)\}) \)
then have \( converse(r)(\mu j.\ j\in R(hm))\in ((N(m))\times \{(hm)\}) \) using left_inverse, inj, M
then have \( \text{fst}(converse(r)(\mu j.\ j\in R(hm)))\in (N(m)) \)
fix \( e \)
assume \( e\in E \)
then obtain \( m \) where \( m\in M \) and \( e=\langle m,Em\rangle \) using function_apply_equality, ff
with thesis1 have \( e\in Sigma(M,\lambda t.\ Nt) \)
then have \( E\in Pow(Sigma(M,\lambda t.\ Nt)) \)
with ff have \( E\in \text{Pi}(M,\lambda m.\ Nm) \) using Pi_iff
then have \( (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt)) \) using thesis1
then show \( thesis \) using AxiomCardinalChoiceGen_def, assms(2)
qed
Here is the equivalence from the two previous results.
theorem Q_choice_eq_secon_imp_sepa:
assumes \( \text{Card}(Q) \)
shows \( (\forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow (T\text{ is separable of cardinal }\text{csucc}(Q)))\) \( \longleftrightarrow (\text{ the axiom of } Q \text{ choice holds }) \) using Q_choice_imp_second_imp_separable, choice_subset_imp_choice using second_imp_separable_imp_Q_choice, assmsGiven a base injective with a set, then we can find a base whose elements are indexed by that set.
lemma base_to_indexed_base:
assumes \( B \preceq Q \), \( B \text{ is a base for }T \)
shows \( \exists N.\ \{Ni.\ i\in Q}\text{ is a base for }\} \)proof from assms obtain \( f \) where f_def: \( f\in \text{inj}(B,Q) \) unfolding lepoll_def
let \( ff = \{\langle b,fb\rangle .\ b\in B\} \)
have \( domain(ff)=B \)
moreover
have \( relation(ff) \) unfolding relation_def
moreover have \( function(ff) \) unfolding function_def
moreover have \( relation(ff) \Longrightarrow function(ff) \Longrightarrow ff:domain(ff)\rightarrow \text{range}(ff) \) using function_imp_Pi
ultimately have fun: \( ff:B\rightarrow \text{range}(ff) \)
have injj: \( ff\in \text{inj}(B,\text{range}(ff)) \)proof
{
}
fix \( w \) \( x \)
assume AS: \( w\in B \), \( x\in B \), \( \{\langle b, f b\rangle .\ b \in B\} w = \{\langle b, f b\rangle .\ b \in B\} x \)
then have \( fw=fx \) using apply_equality, fun
then have \( w=x \) using f_def, inj_def, AS(1,2)
then have \( \forall w\in B.\ \forall x\in B.\ \{\langle b, f b\rangle .\ b \in B\} w = \{\langle b, f b\rangle .\ b \in B\} x \longrightarrow w = x \)
then show \( ff\in \text{inj}(B,\text{range}(ff)) \) unfolding inj_def using fun
qed
then have bij: \( ff\in \text{bij}(B,\text{range}(ff)) \) using inj_bij_range
from fun have \( \text{range}(ff)=\{fb.\ b\in B\} \)
with f_def have ran: \( \text{range}(ff)\subseteq Q \) using inj_def
let \( N = \{\langle i,(\text{if }i\in \text{range}(ff)\text{ then }converse(ff)i\text{ else }0)\rangle .\ i\in Q\} \)
have FN: \( function(N) \) unfolding function_def
have \( B \subseteq \{Ni.\ i\in Q\} \)proof
fix \( t \)
assume a: \( t\in B \)
from bij have rr: \( ff:B\rightarrow \text{range}(ff) \) unfolding bij_def, inj_def
have ig: \( fft=ft \) using a, apply_equality, rr
have r: \( fft\in \text{range}(ff) \) using apply_type, rr, a
from ig have t: \( fft\in Q \) using apply_type, a, f_def unfolding inj_def
with r have \( N(fft)=converse(ff)(fft) \) using function_apply_equality, FN
then have \( N(fft)=t \) using left_inverse, injj, a
then have \( t=N(fft) \)
then have \( \exists i\in Q.\ t=Ni \) using t(1)
then show \( t\in \{Ni.\ i\in Q\} \)
qed
moreover
have \( \forall r\in \{Ni.\ i\in Q\}-B.\ r=0 \)proof
}
ultimately have \( \{Ni.\ i\in Q\}=B\vee \{Ni.\ i\in Q\}=B \cup \{0\} \)
fix \( r \)
assume \( r\in \{Ni.\ i\in Q\}-B \)
then obtain \( j \) where R: \( j\in Q \), \( r=Nj \), \( r\notin B \)
{
assume AS: \( j\in \text{range}(ff) \)
with R(1) have \( Nj=converse(ff)j \) using function_apply_equality, FN
moreover
have \( converse(ff):\text{range}(ff)\rightarrow B \) using inj_is_fun, bij_is_inj, bij_converse_bij, bij
ultimately have \( Nj\in B \) using apply_funtype, AS
then have \( False \) using R(3,2)
then have \( j\notin \text{range}(ff) \)
then show \( r=0 \) using function_apply_equality, FN, R(1,2)
qed
moreover
qed
have \( (B \cup \{0\})-\{0\}=B-\{0\} \)
then have \( (B \cup \{0\})-\{0\} \text{ is a base for }T \) using base_no_0, assms(2)
then have \( B \cup \{0\} \text{ is a base for }T \) using base_no_0
ultimately have \( \{Ni.\ i\in Q}\text{ is a base for }\} \) using assms(2)
then show \( thesis \)
Relation between numerability and compactness
If the axiom of Q choice holds, then any topology of second type of cardinal \( \text{csucc}(Q) \) is compact of cardinal \( \text{csucc}(Q) \)
Under the axiom of Q choice for subsets of \( Pow(Q) \), every topology of second type of cardinal \( \text{csucc}(Q) \) is compact of that same cardinal.
theorem compact_of_cardinal_Q:
assumes \( \text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q)) \), \( T\text{ is of second type of cardinal }\text{csucc}(Q) \), \( T\text{ is a topology } \)
shows \( ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \)proof from assms(1) have CC: \( \text{Card}(Q) \) and reg: \( \bigwedge M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0\wedge Nt\subseteq Pow(Q))) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt)) \) using AxiomCardinalChoice_def
from assms(2) obtain \( R \) where \( R\preceq Q \), \( R\text{ is a base for }T \) unfolding IsSecondOfCard_def using Card_less_csucc_eq_le, CC
with base_to_indexed_base obtain \( N \) where base: \( \{Ni.\ i\in Q}\text{ is a base for }\} \)
{
fix \( M \)
assume A: \( \bigcup T\subseteq \bigcup M \), \( M\in Pow(T) \)
let \( \ \lt alpha> = \lambda U\in M.\ \{i\in Q.\ N(i)\subseteq U\} \)
have inj: \( \ \lt alpha>\in \text{inj}(M,Pow(Q)) \)proof
{
}
}
}
qed
have \( (\bigwedge x.\ x \in M \Longrightarrow \{i \in Q .\ N i \subseteq x\} \in Pow(Q)) \Longrightarrow \ \lt alpha> \in M \rightarrow Pow(Q) \) using lam_type
then have I: \( \ \lt alpha> \in M \rightarrow Pow(Q) \)
{
fix \( w \) \( x \)
assume AS: \( w\in M \), \( x\in M \), \( \{i \in Q .\ N(i) \subseteq w\} = \{i \in Q .\ N(i) \subseteq x\} \)
from AS(1,2), A(2) have \( w\in T \), \( x\in T \)
then have \( w= \text{Interior}(w,T) \), \( x= \text{Interior}(x,T) \) using assms(3), Top_2_L3, topology0_def
then have UN: \( w=(\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\}) \), \( x=(\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\}) \) using interior_set_base_topology, assms(3), base
{
fix \( b \)
assume \( b\in w \)
then have \( b\in \bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\} \) using UN(1)
then obtain \( S \) where S: \( S\in \{N(i).\ i\in Q\} \), \( b\in S \), \( S\subseteq w \)
then obtain \( j \) where j: \( j\in Q \), \( S=N(j) \)
then have \( j\in \{i \in Q .\ N(i) \subseteq w\} \) using S(3)
then have \( N(j)\subseteq x \), \( b\in N(j) \), \( j\in Q \) using S(2), AS(3), j
then have \( b\in (\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\}) \)
then have \( b\in x \) using UN(2)
moreover {
}
ultimately have \( w=x \)
fix \( b \)
assume \( b\in x \)
then have \( b\in \bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\} \) using UN(2)
then obtain \( S \) where S: \( S\in \{N(i).\ i\in Q\} \), \( b\in S \), \( S\subseteq x \)
then obtain \( j \) where j: \( j\in Q \), \( S=N(j) \)
then have \( j\in \{i \in Q .\ N(i) \subseteq x\} \) using S(3)
then have \( j\in \{i \in Q .\ N(i) \subseteq w\} \) using AS(3)
then have \( N(j)\subseteq w \), \( b\in N(j) \), \( j\in Q \) using S(2), j(2)
then have \( b\in (\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\}) \)
then have \( b\in w \) using UN(2)
then have II: \( \forall w\in M.\ \forall x\in M.\ (\lambda U\in M.\ \{i \in Q .\ N i \subseteq U\}) w = (\lambda U\in M.\ \{i \in Q .\ N i \subseteq U\}) x \longrightarrow w = x \)
from I, II show \( thesis \) unfolding inj_def
let \( X = \lambda i\in Q.\ \{\ \lt alpha>U.\ U\in \{V\in M.\ N(i)\subseteq V\}\} \)
let \( M = \{i\in Q.\ Xi\neq 0\} \)
have subMQ: \( M\subseteq Q \)
then have ddd: \( M \preceq Q \) using subset_imp_lepoll
then have \( M \preceq Q \), \( \forall i\in M.\ Xi\neq 0 \), \( \forall i\in M.\ Xi\subseteq Pow(Q) \)
then have \( M \preceq Q \), \( \forall i\in M.\ Xi\neq 0 \), \( \forall i\in M.\ Xi \preceq Pow(Q) \) using subset_imp_lepoll
moreover
{
from reg have \( (M \preceq Q \wedge (\forall t\in M.\ Xt\neq 0\wedge Xt\subseteq Pow(Q))) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Xt) \wedge (\forall t\in M.\ ft\in Xt)) \)
ultimately have \( (\exists f.\ f:\text{Pi}(M,\lambda t.\ Xt) \wedge (\forall t\in M.\ ft\in Xt)) \)
then obtain \( f \) where f: \( f:\text{Pi}(M,\lambda t.\ Xt) \), \( (\bigwedge t.\ t\in M \Longrightarrow ft\in Xt) \)
fix \( m \)
assume S: \( m\in M \)
from f(2), S obtain \( YY \) where YY: \( (YY\in M) \), \( (fm=\ \lt alpha>YY) \)
then have Y: \( (YY\in M)\wedge (fm=\ \lt alpha>YY) \)
{
fix \( U \)
assume \( U\in M\wedge (fm=\ \lt alpha>U) \)
then have \( U=YY \) using inj, inj_def, YY
then have r: \( \bigwedge x.\ x\in M\wedge (fm=\ \lt alpha>x) \Longrightarrow x=YY \)
have \( (YY\in M)\wedge (fm=\ \lt alpha>YY) \Longrightarrow (\bigwedge x.\ x\in M\wedge (fm=\ \lt alpha>x) \Longrightarrow x=YY) \Longrightarrow \exists !x.\ x \in M \wedge f m = \ \lt alpha> x \) by (rule ex1I )
then have \( \exists !YY.\ YY\in M \wedge fm=\ \lt alpha>YY \) using Y, r
then have ex1YY: \( \forall m\in M.\ \exists !YY.\ YY\in M \wedge fm=\ \lt alpha>YY \)
let \( YYm = \{\langle m,(\text{The } YY.\ YY\in M \wedge fm=\ \lt alpha>YY)\rangle .\ m\in M\} \)
have aux: \( \bigwedge m.\ m\in M \Longrightarrow YYmm=(\text{The } YY.\ YY\in M \wedge fm=\ \lt alpha>YY) \) unfolding apply_def
have ree: \( \forall m\in M.\ (YYmm)\in M \wedge fm=\ \lt alpha>(YYmm) \)proof
fix \( m \)
assume C: \( m\in M \)
then have \( \exists !YY.\ YY\in M \wedge fm=\ \lt alpha>YY \) using ex1YY
then have \( (\text{The } YY.\ YY\in M \wedge fm=\ \lt alpha>YY)\in M\wedge fm=\ \lt alpha>(\text{The } YY.\ YY\in M \wedge fm=\ \lt alpha>YY) \) by (rule theI )
moreover
qed
from aux, C have \( (\text{The } YY.\ YY\in M \wedge fm=\ \lt alpha>YY) = YYmm \)
ultimately show \( (YYmm)\in M \wedge fm=\ \lt alpha>(YYmm) \)
have tt: \( \bigwedge m.\ m\in M \Longrightarrow N(m)\subseteq YYmm \)proof
fix \( m \)
assume D: \( m\in M \)
then have QQ: \( m\in Q \)
from D have t: \( (YYmm)\in M \wedge fm=\ \lt alpha>(YYmm) \) using ree
then have \( fm=\ \lt alpha>(YYmm) \)
moreover
qed
from f(2), D have \( fm\in Xm \)
ultimately have \( (\ \lt alpha>(YYmm))\in Xm \)
then have \( (\ \lt alpha>(YYmm))\in \{\ \lt alpha>U.\ U\in \{V\in M.\ N(m)\subseteq V\}\} \) using QQ
then obtain \( U \) where \( U\in \{V\in M.\ N(m)\subseteq V\} \), \( \ \lt alpha>(YYmm)=\ \lt alpha>U \)
then have r: \( U\in M \), \( N(m)\subseteq U \), \( \ \lt alpha>(YYmm)=\ \lt alpha>U \), \( (YYmm)\in M \) using t
then have \( YYmm=U \) using inj_apply_equality, inj
then show \( N(m)\subseteq YYmm \) using r
then have I: \( (\bigcup m\in M.\ N(m))\subseteq (\bigcup m\in M.\ YYmm) \)proof
{
{
}
fix \( s \)
assume \( s\in (\bigcup m\in M.\ N(m)) \)
then obtain \( t \) where r: \( t\in M \), \( s\in N(t) \)
then have \( s\in YYmt \) using tt, r(1)
then have \( s\in (\bigcup m\in M.\ YYmm) \) using r(1)
then show \( thesis \)
qed
fix \( x \)
assume AT: \( x\in \bigcup T \)
with A obtain \( U \) where BB: \( U\in M \), \( U\in T \), \( x\in U \)
have \( U \in T \Longrightarrow x \in U \Longrightarrow \exists V\in \{Nj.\ j\in Q\}.\ V \subseteq U \wedge x \in V \) using point_open_base_neigh, base
with BB(2,3) obtain \( j \) where BC: \( j\in Q \), \( N(j)\subseteq U \), \( x\in N(j) \)
then have \( Xj\neq 0 \) using BB(1)
then have \( j\in M \) using BC(1)
then have \( x\in (\bigcup m\in M.\ N(m)) \) using BC(3)
then have II: \( \bigcup T\subseteq (\bigcup m\in M.\ N(m)) \)
have covers: \( \bigcup T\subseteq (\bigcup m\in M.\ YYmm) \)proof
{
}
fix \( x \)
assume \( x\in \bigcup T \)
with II have \( x\in (\bigcup m\in M.\ Nm) \)
with I have \( x\in (\bigcup m\in M.\ YYmm) \)
then show \( thesis \)
qed
have \( relation(YYm) \) unfolding relation_def
moreover
have f: \( function(YYm) \) unfolding function_def
moreover have d: \( domain(YYm)=M \)
moreover have r: \( \text{range}(YYm)=YYmM \)
moreover have \( relation(YYm) \Longrightarrow function(YYm) \Longrightarrow YYm:domain(YYm)\rightarrow \text{range}(YYm) \) using function_imp_Pi
ultimately have fun: \( YYm:M\rightarrow YYmM \)
have \( YYm:M\rightarrow YYmM \Longrightarrow YYm\in \text{surj}(M,\text{range}(YYm)) \) using fun_is_surj
with fun have \( YYm\in \text{surj}(M,YYmM) \) using r
with surj_fun_inv, subMQ, Card_is_Ord, CC have \( YYmM \preceq M \)
with ddd have Rw: \( YYmM \preceq Q \) using lepoll_trans
{
fix \( m \)
assume \( m\in M \)
then have \( \langle m,YYmm\rangle \in YYm \) using function_apply_Pair, f, d
then have \( YYmm\in YYmM \)
then have l1: \( \{YYmm.\ m\in M\}\subseteq YYmM \)
{
fix \( t \)
assume \( t\in YYmM \)
then have \( \exists x\in M.\ \langle x,t\rangle \in YYm \) unfolding image_def
then obtain \( r \) where S: \( r\in M \), \( \langle r,t\rangle \in YYm \)
have \( YYmr=t \) using apply_equality, S(2), fun
with S(1) have \( t\in \{YYmm.\ m\in M\} \)
with l1 have \( \{YYmm.\ m\in M\}=YYmM \)
with Rw have \( \{YYmm.\ m\in M\} \preceq Q \)
with covers have \( \{YYmm.\ m\in M\}\in Pow(M)\wedge \bigcup T\subseteq \bigcup \{YYmm.\ m\in M\}\wedge \{YYmm.\ m\in M\} \prec \text{csucc}(Q) \) using ree, Card_less_csucc_eq_le, CC
then have \( \exists N\in Pow(M).\ \bigcup T\subseteq \bigcup N\wedge N\prec \text{csucc}(Q) \)
then have \( \forall M\in Pow(T).\ \bigcup T \subseteq \bigcup M \longrightarrow (\exists N\in Pow(M).\ \bigcup T \subseteq \bigcup N \wedge N \prec \text{csucc}(Q)) \)
then show \( thesis \) using IsCompactOfCard_def, Card_csucc, CC, Card_is_Ord
qed
In the following proof, we have chosen an infinite cardinal
to be able to apply the equation @{prop "Q\
theorem second_imp_compact_imp_Q_choice_PowQ:
assumes \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \) and \( \text{InfCard}(Q) \)
shows \( \text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q)) \)proof{
}
}
}
}
}
}
}
fix \( N \) \( M \)
assume AS: \( M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq Pow(Q)) \)
then obtain \( h \) where \( h\in \text{inj}(M,Q) \) using lepoll_def
have discTop: \( Pow(Q\times M) \text{ is a topology } \) using Pow_is_top
{
fix \( A \)
assume AS: \( A\in Pow(Q\times M) \)
have \( A=\bigcup \{\{i\}.\ i\in A\} \)
with AS have \( \exists T\in Pow(\{\{i\}.\ i\in Q\times M\}).\ A=\bigcup T \)
then have \( A\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in Q\times M\})\} \)
moreover {
}
ultimately have base: \( \{\{x\}.\ x\in Q\times M\} \text{ is a base for } Pow(Q\times M) \) unfolding IsAbaseFor_def
fix \( A \)
assume AS: \( A\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in Q\times M\})\} \)
then have \( A\in Pow(Q\times M) \)
let \( f = \{\langle i,\{i\}\rangle .\ i\in Q\times M\} \)
have \( Q \preceq Q \Longrightarrow M \preceq Q \Longrightarrow Q \times M \preceq Q \times Q \) using prod_lepoll_mono
then have \( M \preceq Q \Longrightarrow Q \times M \preceq Q \times Q \) using lepoll_refl
with AS have R: \( Q \times M \preceq Q \times Q \)
have fff: \( f\in Q\times M\rightarrow \{\{i\}.\ i\in Q\times M\} \) using Pi_def, function_def
then have \( f\in \text{inj}(Q\times M,\{\{i\}.\ i\in Q\times M\}) \) unfolding inj_def using apply_equality
then have \( f\in \text{bij}(Q\times M,\{\{i\}.\ i\in Q\times M\}) \) unfolding bij_def, surj_def using fff, apply_equality, fff
then have \( Q\times M\approx \{\{i\}.\ i\in Q\times M\} \) using eqpoll_def
then have \( \{\{i\}.\ i\in Q\times M\}\approx Q\times M \) using eqpoll_sym
then have \( \{\{i\}.\ i\in Q\times M\}\preceq Q\times M \) using eqpoll_imp_lepoll
then have \( \{\{i\}.\ i\in Q\times M\}\preceq Q\times Q \) using R, lepoll_trans
then have \( \{\{i\}.\ i\in Q\times M\}\preceq Q \) using InfCard_square_eqpoll, assms(2), lepoll_eq_trans
then have \( \{\{i\}.\ i\in Q\times M\}\prec \text{csucc}(Q) \) using Card_less_csucc_eq_le, assms(2), InfCard_is_Card
then have \( Pow(Q\times M) \text{ is of second type of cardinal } \text{csucc}(Q) \) using IsSecondOfCard_def, base
then have comp: \( (Q\times M) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M) \) using discTop, assms(1)
{
fix \( W \)
assume \( W\in Pow(Q\times M) \)
then have T: \( W\text{ is closed in } Pow(Q\times M) \), \( (Q\times M)\cap W=W \) using IsClosed_def
have \( ((Q\times M) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \Longrightarrow (W \text{ is closed in } Pow(Q\times M)) \)
\( \Longrightarrow (((Q\times M)\cap W) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \) using compact_closed
with comp, T(1) have \( (((Q\times M)\cap W) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \)
with T(2) have \( W\text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M) \)
then have subCompact: \( \forall W\in Pow(Q\times M).\ (W \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \)
let \( cub = \bigcup \{\{(U)\times \{t\}.\ U\in Nt\}.\ t\in M\} \)
from AS have \( (\bigcup cub)\in Pow((Q)\times M) \)
with subCompact have Ncomp: \( ((\bigcup cub) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \)
have cond: \( (cub)\in Pow(Pow(Q\times M))\wedge \bigcup cub\subseteq \bigcup cub \) using AS
have \( \exists S\in Pow(cub).\ (\bigcup cub) \subseteq \bigcup S \wedge S \prec \text{csucc}(Q) \)proof
{
}
have \( ((\bigcup cub) \text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q\times M)) \) using Ncomp
then have \( \forall M\in Pow(Pow(Q\times M)).\ \bigcup cub \subseteq \bigcup M \longrightarrow (\exists Na\in Pow(M).\ \bigcup cub \subseteq \bigcup Na \wedge Na \prec \text{csucc}(Q)) \) unfolding IsCompactOfCard_def
with cond have \( \exists S\in Pow(cub).\ \bigcup cub \subseteq \bigcup S \wedge S \prec \text{csucc}(Q) \)
then show \( thesis \)
qed
then have ttt: \( \exists S\in Pow(cub).\ (\bigcup cub) \subseteq \bigcup S \wedge S \preceq Q \) using Card_less_csucc_eq_le, assms(2), InfCard_is_Card
then obtain \( S \) where S_def: \( S\in Pow(cub) \), \( (\bigcup cub) \subseteq \bigcup S \), \( S \preceq Q \)
{
fix \( t \)
assume AA: \( t\in M \), \( Nt\neq \{0\} \)
from AA(1), AS have \( Nt\neq 0 \)
with AA(2) obtain \( U \) where G: \( U\in Nt \) and notEm: \( U\neq 0 \)
then have \( U\times \{t\}\in cub \) using AA
then have \( U\times \{t\}\subseteq \bigcup cub \)
with G, notEm, AA have \( \exists s.\ \langle s,t\rangle \in \bigcup cub \)
then have \( \forall t\in M.\ (Nt\neq \{0\})\longrightarrow (\exists s.\ \langle s,t\rangle \in \bigcup cub) \)
then have A: \( \forall t\in M.\ (Nt\neq \{0\})\longrightarrow (\exists s.\ \langle s,t\rangle \in \bigcup S) \) using S_def(2)
from S_def(1) have B: \( \forall f\in S.\ \exists t\in M.\ \exists U\in Nt.\ f=U\times \{t\} \)
from A, B have \( \forall t\in M.\ (Nt\neq \{0\})\longrightarrow (\exists U\in Nt.\ U\times \{t\}\in S) \)
then have noEmp: \( \forall t\in M.\ (Nt\neq \{0\})\longrightarrow (S\cap (\{U\times \{t\}.\ U\in Nt\})\neq 0) \)
from S_def(3) obtain \( r \) where r: \( r:\text{inj}(S,Q) \) using lepoll_def
then have bij2: \( converse(r):\text{bij}(\text{range}(r),S) \) using inj_bij_range, bij_converse_bij
then have surj2: \( converse(r):\text{surj}(\text{range}(r),S) \) using bij_def
let \( R = \lambda t\in M.\ \{j\in \text{range}(r).\ converse(r)j\in (\{U\times \{t\}.\ U\in Nt\})\} \)
{
fix \( t \)
assume AA: \( t\in M \), \( Nt\neq \{0\} \)
then have \( (S\cap (\{U\times \{t\}.\ U\in Nt\})\neq 0) \) using noEmp
then obtain \( s \) where ss: \( s\in S \), \( s\in \{U\times \{t\}.\ U\in Nt\} \)
then obtain \( j \) where \( converse(r)j=s \), \( j\in \text{range}(r) \) using surj2 unfolding surj_def
then have \( j\in \{j\in \text{range}(r).\ converse(r)j\in (\{U\times \{t\}.\ U\in Nt\})\} \) using ss
then have \( Rt\neq 0 \) using beta_if, AA
then have nonE: \( \forall t\in M.\ Nt\neq \{0\}\longrightarrow Rt\neq 0 \)
{
fix \( t \) \( j \)
assume \( t\in M \), \( j\in Rt \)
then have \( converse(r)j\in \{U\times \{t\}.\ U\in Nt\} \) using beta_if
then have pp: \( \forall t\in M.\ \forall j\in Rt.\ converse(r)j\in \{U\times \{t\}.\ U\in Nt\} \)
have reg: \( \forall t U V.\ U\times \{t\}=V\times \{t\}\longrightarrow U=V \)proof
{
}
}
fix \( t \) \( U \) \( V \)
assume AA: \( U\times \{t\}=V\times \{t\} \)
{
fix \( v \)
assume \( v\in V \)
then have \( \langle v,t\rangle \in V \times \{t\} \)
then have \( \langle v,t\rangle \in U \times \{t\} \) using AA
then have \( v\in U \)
then have \( V\subseteq U \)
moreover {
}
fix \( u \)
assume \( u\in U \)
then have \( \langle u,t\rangle \in U \times \{t\} \)
then have \( \langle u,t\rangle \in V \times \{t\} \) using AA
then have \( u\in V \)
then have \( U\subseteq V \)
ultimately have \( U=V \)
then show \( thesis \)
qed
let \( E = \{\langle t,\text{if }Nt=\{0\}\text{ then }0\text{ else }(\text{The } U.\ converse(r)(\mu j.\ j\in Rt)=U\times \{t\})\rangle .\ t\in M\} \)
have ff: \( function(E) \) unfolding function_def
moreover {
}
}
}
ultimately have thesis1: \( \forall t\in M.\ Et\in Nt \) using function_apply_equality
{
fix \( t \)
assume pm: \( t\in M \)
{
assume nonEE: \( Nt\neq \{0\} \)
{
fix \( j \)
assume \( j\in Rt \)
with pm(1) have \( j\in \text{range}(r) \) using beta_if
from r have \( r:\text{surj}(S,\text{range}(r)) \) using fun_is_surj, inj_def
with \( j\in \text{range}(r) \) obtain \( d \) where \( d\in S \) and \( rd=j \) using surj_def
then have \( j\in Q \) using r, inj_def
then have sub: \( Rt\subseteq Q \)
from nonE, pm, nonEE obtain \( ee \) where P: \( ee\in Rt \)
with sub have \( ee\in Q \)
then have \( Ord(ee) \) using assms(2), Card_is_Ord, Ord_in_Ord, InfCard_is_Card
with P have \( (\mu j.\ j\in Rt)\in Rt \) by (rule LeastI )
with pp, pm have \( converse(r)(\mu j.\ j\in Rt)\in \{U\times \{t\}.\ U\in Nt\} \)
then obtain \( W \) where \( converse(r)(\mu j.\ j\in Rt)=W\times \{t\} \) and s: \( W\in Nt \)
then have \( (\text{The } U.\ converse(r)(\mu j.\ j\in Rt)=U\times \{t\})=W \) using reg
with s have \( (\text{The } U.\ converse(r)(\mu j.\ j\in Rt)=U\times \{t\})\in Nt \)
then have \( (\text{if }Nt=\{0\}\text{ then }0\text{ else }(\text{The } U.\ converse(r)(\mu j.\ j\in Rt)=U\times \{t\}))\in Nt \)
fix \( e \)
assume \( e\in E \)
then obtain \( m \) where \( m\in M \) and \( e=\langle m,Em\rangle \) using function_apply_equality, ff
with thesis1 have \( e\in Sigma(M,\lambda t.\ Nt) \)
then have \( E\in Pow(Sigma(M,\lambda t.\ Nt)) \)
with ff have \( E\in \text{Pi}(M,\lambda m.\ Nm) \) using Pi_iff
then have \( (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt)) \) using thesis1
then show \( thesis \) using AxiomCardinalChoice_def, assms(2), InfCard_is_Card
qed
The two previous results, state the following equivalence:
theorem Q_choice_Pow_eq_secon_imp_comp:
assumes \( \text{InfCard}(Q) \)
shows \( (\forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T))\) \( \longleftrightarrow (\text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q))) \) using second_imp_compact_imp_Q_choice_PowQ, compact_of_cardinal_Q, assmsIn the next result we will prove that if the space \((\kappa,Pow(\kappa))\), for \(\kappa\) an infinite cardinal, is compact of its successor cardinal; then all topologycal spaces which are of second type of the successor cardinal of \(\kappa\) are also compact of that cardinal.
theorem Q_csuccQ_comp_eq_Q_choice_Pow:
assumes \( \text{InfCard}(Q) \), \( (Q)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q) \)
shows \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \)proof fix \( T \)
{
assume top: \( T \text{ is a topology } \) and sec: \( T\text{ is of second type of cardinal }\text{csucc}(Q) \)
from assms have \( \text{Card}(\text{csucc}(Q)) \), \( \text{Card}(Q) \) using InfCard_is_Card, Card_is_Ord, Card_csucc
moreover
}
}
have \( \bigcup T\subseteq \bigcup T \)
moreover {
fix \( M \)
assume MT: \( M\in Pow(T) \) and cover: \( \bigcup T\subseteq \bigcup M \)
from sec obtain \( B \) where \( B \text{ is a base for } T \), \( B\prec \text{csucc}(Q) \) using IsSecondOfCard_def
with \( \text{Card}(Q) \) obtain \( N \) where base: \( \{Ni.\ i\in Q}\text{ is a base for }\} \) using Card_less_csucc_eq_le, base_to_indexed_base
let \( S = \{\langle u,\{i\in Q.\ Ni\subseteq u\}\rangle .\ u\in M\} \)
have \( function(S) \) unfolding function_def
then have I: \( S:M\rightarrow Pow(Q) \) using Pi_iff
have \( S\in \text{inj}(M,Pow(Q)) \)proof
{
}
}
fix \( w \) \( x \)
assume AS: \( w\in M \), \( x\in M \), \( \{\langle u, \{i \in Q .\ N i \subseteq u\}\rangle .\ u \in M\} w = \{\langle u, \{i \in Q .\ N i \subseteq u\}\rangle .\ u \in M\} x \)
with \( S:M\rightarrow Pow(Q) \) have ASS: \( \{i \in Q .\ N i \subseteq w\}=\{i \in Q .\ N i \subseteq x\} \) using apply_equality
from AS(1,2), MT have \( w\in T \), \( x\in T \)
then have \( w= \text{Interior}(w,T) \), \( x= \text{Interior}(x,T) \) using top, Top_2_L3, topology0_def
then have UN: \( w=(\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\}) \), \( x=(\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\}) \) using interior_set_base_topology, top, base
{
fix \( b \)
assume \( b\in w \)
then have \( b\in \bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\} \) using UN(1)
then obtain \( S \) where S: \( S\in \{N(i).\ i\in Q\} \), \( b\in S \), \( S\subseteq w \)
then obtain \( j \) where j: \( j\in Q \), \( S=N(j) \)
then have \( j\in \{i \in Q .\ N(i) \subseteq w\} \) using S(3)
then have \( N(j)\subseteq x \), \( b\in N(j) \), \( j\in Q \) using S(2), ASS, j
then have \( b\in (\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\}) \)
then have \( b\in x \) using UN(2)
moreover {
}
ultimately have \( w=x \)
fix \( b \)
assume \( b\in x \)
then have \( b\in \bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq x\} \) using UN(2)
then obtain \( S \) where S: \( S\in \{N(i).\ i\in Q\} \), \( b\in S \), \( S\subseteq x \)
then obtain \( j \) where j: \( j\in Q \), \( S=N(j) \)
then have \( j\in \{i \in Q .\ N(i) \subseteq x\} \) using S(3)
then have \( j\in \{i \in Q .\ N(i) \subseteq w\} \) using ASS
then have \( N(j)\subseteq w \), \( b\in N(j) \), \( j\in Q \) using S(2), j(2)
then have \( b\in (\bigcup \{B\in \{N(i).\ i\in Q\}.\ B\subseteq w\}) \)
then have \( b\in w \) using UN(2)
then have II: \( \forall w\in M.\ \forall x\in M.\ \{\langle u, \{i \in Q .\ N i \subseteq u\}\rangle .\ u \in M\} w = \{\langle u, \{i \in Q .\ N i \subseteq u\}\rangle .\ u \in M\} x \longrightarrow w = x \)
from I, II show \( thesis \) unfolding inj_def
qed
then have \( S\in \text{bij}(M,\text{range}(S)) \) using fun_is_surj unfolding bij_def, inj_def, surj_def
have M: \( (\bigcup (\text{range}(S))) \text{ is closed in } Pow(Q) \), \( Q\cap (\bigcup \text{range}(S))=(\bigcup \text{range}(S)) \) using IsClosed_def
have \( \text{range}(S)\subseteq Pow(Q) \)
then have \( \text{range}(S)\in Pow(Pow(Q)) \)
moreover
{
from compact_closed have \( Q\text{ is compact of cardinal }\text{csucc}(Q) \{in\}Pow(Q) \)
\( \Longrightarrow (\bigcup (\text{range}(S))) \text{ is closed in } Pow(Q) \)
\( \Longrightarrow (Q\cap (\bigcup (\text{range}(S))))\text{ is compact of cardinal }\text{csucc}(Q) \{in\}Pow(Q) \)
with M, assms(2) have \( (\bigcup \text{range}(S))\text{ is compact of cardinal }\text{csucc}(Q) \{in\}Pow(Q) \)
moreover have \( \bigcup (\text{range}(S))\subseteq \bigcup (\text{range}(S)) \)
ultimately have \( \exists S\in Pow(\text{range}(S)).\ (\bigcup (\text{range}(S)))\subseteq \bigcup S \wedge S\prec \text{csucc}(Q) \) using IsCompactOfCard_def
then obtain \( SS \) where SS_def: \( SS\subseteq \text{range}(S) \), \( (\bigcup (\text{range}(S)))\subseteq \bigcup SS \), \( SS\prec \text{csucc}(Q) \)
with \( S\in \text{bij}(M,\text{range}(S)) \) have con: \( converse(S)\in \text{bij}(\text{range}(S),M) \) using bij_converse_bij
then have r1: \( \text{restrict}(converse(S),SS)\in \text{bij}(SS,converse(S)SS) \) using restrict_bij, bij_def, SS_def(1)
then have rr: \( converse(\text{restrict}(converse(S),SS))\in \text{bij}(converse(S)SS,SS) \) using bij_converse_bij
fix \( x \)
assume \( x\in \bigcup T \)
with cover have \( x\in \bigcup M \)
then obtain \( R \) where \( R\in M \), \( x\in R \)
with MT have \( R\in T \), \( x\in R \)
then have \( \exists V\in \{Ni.\ i\in Q\}.\ V\subseteq R \wedge x\in V \) using point_open_base_neigh, base
then obtain \( j \) where \( j\in Q \), \( Nj\subseteq R \) and x_p: \( x\in Nj \)
with \( R\in M \), \( S:M\rightarrow Pow(Q) \), \( S\in \text{bij}(M,\text{range}(S)) \) have \( SR\in \text{range}(S) \wedge j\in SR \) using apply_equality, bij_def, inj_def
then have \( \exists A.\ A\in \text{range}(S) \wedge j\in A \) by (rule exI )
then have \( \exists A\in \text{range}(S).\ j\in A \) unfolding Bex_def
then have \( j\in (\bigcup (\text{range}(S))) \)
then have \( j\in \bigcup SS \) using SS_def(2)
then obtain \( SR \) where \( SR\in SS \), \( j\in SR \)
moreover
have \( converse(\text{restrict}(converse(S),SS))\in \text{surj}(converse(S)SS,SS) \) using rr, bij_def
ultimately obtain \( RR \) where \( converse(\text{restrict}(converse(S),SS))RR=SR \) and p: \( RR\in converse(S)SS \) unfolding surj_def
then have \( converse(converse(\text{restrict}(converse(S),SS)))(converse(\text{restrict}(converse(S),SS))RR)=converse(converse(\text{restrict}(converse(S),SS)))SR \)
moreover
have \( converse(\text{restrict}(converse(S),SS))\in \text{inj}(converse(S)SS,SS) \) using rr unfolding bij_def
moreover have \( converse(\text{restrict}(converse(S),SS)) \in \text{inj}(converse(S)SS, SS) \Longrightarrow RR \in converse(S) SS \Longrightarrow \)
\( converse(converse(\text{restrict}(converse(S),SS))) (converse(\text{restrict}(converse(S),SS)) RR) = RR \) using left_inverse
ultimately have \( RR=converse(converse(\text{restrict}(converse(S),SS)))SR \) using p
moreover
from this, r1 have \( \text{restrict}(converse(S),SS)\in SS\rightarrow converse(S)SS \) unfolding bij_def, inj_def
then have \( relation(\text{restrict}(converse(S),SS)) \) using Pi_def, relation_def
then have \( converse(converse(\text{restrict}(converse(S),SS)))=\text{restrict}(converse(S),SS) \) using relation_converse_converse
ultimately have \( RR=\text{restrict}(converse(S),SS)SR \)
with \( SR\in SS \) have eq: \( RR=converse(S)SR \) unfolding restrict
then have \( converse(converse(S))RR=converse(converse(S))(converse(S)SR) \)
moreover
from this, \( SR\in SS \) have \( SR\in \text{range}(S) \) using SS_def(1)
then have \( converse(S) \in \text{inj}(\text{range}(S),M) \Longrightarrow converse(converse(S)) (converse(S) SR) = SR \)
with con have \( converse(converse(S))(converse(S)SR)=SR \) unfolding bij_def
ultimately have \( converse(converse(S))RR=SR \)
then have \( SRR=SR \) using relation_converse_converse unfolding relation_def
moreover
have \( converse(S):\text{range}(S)\rightarrow M \) using con, bij_def, inj_def
with \( SR\in \text{range}(S) \) have \( converse(S)SR\in M \) using apply_funtype
with eq have \( RR\in M \)
ultimately have \( SR=\{i\in Q.\ Ni\subseteq RR\} \) using I, apply_equality
with \( j\in SR \) have \( Nj\subseteq RR \)
with x_p have \( x\in RR \)
with p have \( x\in \bigcup (converse(S)SS) \)
then have \( \bigcup T\subseteq \bigcup (converse(S)SS) \)
moreover {
}
from con have \( converse(S)SS=\{converse(S)R.\ R\in SS\} \) using image_function, SS_def(1) unfolding range_def, bij_def, inj_def, Pi_def
have \( \{converse(S)R.\ R\in SS\}\subseteq \{converse(S)R.\ R\in \text{range}(S)\} \) using SS_def(1)
moreover
have \( converse(S):\text{range}(S)\rightarrow M \) using con unfolding bij_def, inj_def
then have \( \{converse(S)R.\ R\in \text{range}(S)\}\subseteq M \) using apply_funtype
ultimately have \( (converse(S)SS)\subseteq M \)
then have \( converse(S)SS\in Pow(M) \)
moreover from this, rr have \( converse(S)SS\approx SS \) using eqpoll_def
then have \( converse(S)SS\prec \text{csucc}(Q) \) using SS_def(3), eq_lesspoll_trans
ultimately have \( \exists N\in Pow(M).\ \bigcup T\subseteq \bigcup N \wedge N\prec \text{csucc}(Q) \)
then have \( \forall M\in Pow(T).\ \bigcup T\subseteq \bigcup M \longrightarrow (\exists N\in Pow(M).\ \bigcup T\subseteq \bigcup N \wedge N\prec \text{csucc}(Q)) \)
ultimately have \( (\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T \) unfolding IsCompactOfCard_def
then show \( (T \text{ is a topology }) \wedge (T \text{ is of second type of cardinal }\text{csucc}(Q)) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q) \{in\}T) \)
qed
The discrete topology on an infinite cardinal Q is of second type of cardinal \( \text{csucc}(Q) \), as witnessed by the base of singletons.
theorem Q_disc_is_second_card_csuccQ:
assumes \( \text{InfCard}(Q) \)
shows \( Pow(Q)\text{ is of second type of cardinal }\text{csucc}(Q) \)proof{
}
fix \( A \)
assume AS: \( A\in Pow(Q) \)
have \( A=\bigcup \{\{i\}.\ i\in A\} \)
with AS have \( \exists T\in Pow(\{\{i\}.\ i\in Q\}).\ A=\bigcup T \)
then have \( A\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in Q\})\} \)
moreover {
}
ultimately have base: \( \{\{x\}.\ x\in Q\} \text{ is a base for } Pow(Q) \) unfolding IsAbaseFor_def
fix \( A \)
assume AS: \( A\in \{\bigcup U.\ U\in Pow(\{\{i\}.\ i\in Q\})\} \)
then have \( A\in Pow(Q) \)
let \( f = \{\langle i,\{i\}\rangle .\ i\in Q\} \)
have \( f\in Q\rightarrow \{\{x\}.\ x\in Q\} \) unfolding Pi_def, function_def
then have \( f\in \text{inj}(Q,\{\{x\}.\ x\in Q\}) \) unfolding inj_def using apply_equality
moreover
qed
from \( f\in Q\rightarrow \{\{x\}.\ x\in Q\} \) have \( f\in \text{surj}(Q,\{\{x\}.\ x\in Q\}) \) unfolding surj_def using apply_equality
ultimately have \( f\in \text{bij}(Q,\{\{x\}.\ x\in Q\}) \) unfolding bij_def
then have \( Q\approx \{\{x\}.\ x\in Q\} \) using eqpoll_def
then have \( \{\{x\}.\ x\in Q\}\approx Q \) using eqpoll_sym
then have \( \{\{x\}.\ x\in Q\}\preceq Q \) using eqpoll_imp_lepoll
then have \( \{\{x\}.\ x\in Q\}\prec \text{csucc}(Q) \) using Card_less_csucc_eq_le, assms, InfCard_is_Card
with base show \( thesis \) using IsSecondOfCard_def
This previous results give us another equivalence of the axiom of Q choice that is apparently weaker (easier to check) to the previous one.
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))) \)proof assume \( Q\text{ is compact of cardinal }\text{csucc}(Q) \{in\}Pow(Q) \)
with assms show \( \text{ the axiom of }Q\text{ choice holds for subsets }(Pow(Q)) \) using Q_choice_Pow_eq_secon_imp_comp, Q_csuccQ_comp_eq_Q_choice_Pow
next
assume \( \text{ the axiom of }Q\text{ choice holds for subsets }(Pow(Q)) \)
with assms show \( Q\text{ is compact of cardinal }\text{csucc}(Q)\{in\}(Pow(Q)) \) using Q_disc_is_second_card_csuccQ, Q_choice_Pow_eq_secon_imp_comp, Pow_is_top
qed
end
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))) \)
Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
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 less_less_imp_un_less:
assumes \( A\prec Q \) and \( B\prec Q \) and \( \text{InfCard}(Q) \)
shows \( A \cup B\prec Q \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge (\bigcup T)\setminus D \in T) \)
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)) \)
Definition of IsFirstOfCard:
\( (T \text{ is of first type of cardinal } Q) \equiv \forall x\in \bigcup T.\ (\exists B.\ (B \text{ is a base for } T) \wedge (\{b\in B.\ x\in b\} \prec Q)) \)
lemma (in topology0) cl_inter_neigh:
assumes \( A \subseteq \bigcup T \) and \( U\in T \) and \( x \in cl(A) \cap U \)
shows \( A\cap U \neq 0 \) lemma (in topology0) inter_neigh_cl:
assumes \( A \subseteq \bigcup T \) and \( x\in \bigcup T \) and \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)
shows \( x \in cl(A) \) lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T \setminus A) = \bigcup T \setminus int(A) \) lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \)Definition of AxiomCardinalChoice:
\( \text{ the axiom of } Q \text{ choice holds for subsets }K \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq K)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
lemma Card_less_csucc_eq_le:
assumes \( \text{Card}(m) \)
shows \( A \prec \text{csucc}(m) \longleftrightarrow A \preceq m \) lemma Top_1_2_L1:
assumes \( B \text{ is a base for } T \) and \( U\in T \)
shows \( \exists A\in Pow(B).\ U = \bigcup A \) lemma dense_int_open:
assumes \( T\text{ is a topology } \) and \( A\subseteq \bigcup T \)
shows \( \text{Closure}(A,T)=\bigcup T \longleftrightarrow (\forall U\in T.\ U\neq 0 \longrightarrow A\cap U\neq 0) \) theorem surj_fun_inv_2:
assumes \( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)
shows \( B\preceq A \)Definition of IsSeparableOfCard:
\( T\text{ is separable of cardinal }Q\equiv \exists U\in Pow(\bigcup T).\ \text{Closure}(U,T)=\bigcup T \wedge U\prec Q \)
lemma inj_bij_range:
assumes \( f \in \text{inj}(A,B) \)
shows \( f \in \text{bij}(A,\text{range}(f)) \)Definition of IsAPartition:
\( (U \text{ is a partition of } X) \equiv (\bigcup U=X \wedge (\forall A\in U.\ \forall B\in U.\ A=B\vee A\cap B=0)\wedge 0\notin U) \)
theorem Ptopology_is_a_topology:
assumes \( U \text{ is a partition of } X \)
shows \( (PTopology X U) \text{ is a topology } \) and \( U \text{ is a base for } (PTopology X U) \) lemma surj_fun_inv:
assumes \( f \in \text{surj}(A,B) \), \( A\subseteq Q \), \( Ord(Q) \)
shows \( B\preceq A \)Definition of IsAbaseFor:
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
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))) \)
theorem Q_choice_imp_second_imp_separable:
assumes \( T\text{ is of second type of cardinal }\text{csucc}(Q) \) and \( \text{ the axiom of } Q \text{ choice holds for subsets } \bigcup T \) and \( T\text{ is a topology } \)
shows \( T\text{ is separable of cardinal }\text{csucc}(Q) \) lemma choice_subset_imp_choice: shows \( \text{ the axiom of } Q \text{ choice holds } \longleftrightarrow (\forall K.\ \text{ the axiom of } Q \text{ choice holds for subsets }K) \)
theorem second_imp_separable_imp_Q_choice:
assumes \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow (T\text{ is separable of cardinal }\text{csucc}(Q)) \) and \( \text{Card}(Q) \)
shows \( \text{ the axiom of } Q \text{ choice holds } \) lemma base_no_0: shows \( B\text{ is a base for }T \longleftrightarrow (B-\{0\})\text{ is a base for }T \)
lemma (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
lemma interior_set_base_topology:
assumes \( U \text{ is a base for } T \), \( T\text{ is a topology } \)
shows \( \text{Interior}(A,T) = \bigcup \{T\in U.\ T\subseteq A\} \) lemma point_open_base_neigh:
assumes \( B \text{ is a base for } T \) and \( U\in T \) and \( x\in U \)
shows \( \exists V\in B.\ V\subseteq U \wedge x\in V \) lemma Pow_is_top: shows \( Pow(X) \text{ is a topology } \)
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 second_imp_compact_imp_Q_choice_PowQ:
assumes \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \) and \( \text{InfCard}(Q) \)
shows \( \text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q)) \) theorem compact_of_cardinal_Q:
assumes \( \text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q)) \), \( T\text{ is of second type of cardinal }\text{csucc}(Q) \), \( T\text{ is a topology } \)
shows \( ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \) lemma base_to_indexed_base:
assumes \( B \preceq Q \), \( B \text{ is a base for }T \)
shows \( \exists N.\ \{Ni.\ i\in Q}\text{ is a base for }\} \) theorem Q_choice_Pow_eq_secon_imp_comp:
assumes \( \text{InfCard}(Q) \)
shows \( (\forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T))\) \( \longleftrightarrow (\text{ the axiom of } Q \text{ choice holds for subsets } (Pow(Q))) \) theorem Q_csuccQ_comp_eq_Q_choice_Pow:
assumes \( \text{InfCard}(Q) \), \( (Q)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}Pow(Q) \)
shows \( \forall T.\ (T\text{ is a topology } \wedge (T\text{ is of second type of cardinal }\text{csucc}(Q))) \longrightarrow ((\bigcup T)\text{ is compact of cardinal }\text{csucc}(Q)\{in\}T) \) theorem Q_disc_is_second_card_csuccQ:
assumes \( \text{InfCard}(Q) \)
shows \( Pow(Q)\text{ is of second type of cardinal }\text{csucc}(Q) \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
