section ‹Properties in Topology›
theory Topology_ZF_properties imports Topology_ZF_examples Topology_ZF_examples_1
begin
text‹
This theory deals with topological properties which make use of cardinals.
›
subsection‹Properties of compactness›
text‹It is already defined what is a compact topological space, but the is a
generalization which may be useful sometimes.›
definition
IsCompactOfCard ("_{is compact of cardinal}_ {in}_" 90)
where "K{is compact of cardinal} Q{in}T ≡ (Card(Q) ∧ K ⊆ ⋃T ∧
(∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺Q)))"
text‹The usual compact property is the one defined over the cardinal
of the natural numbers.›
lemma Compact_is_card_nat:
shows "K{is compact in}T ⟷ (K{is compact of cardinal} nat {in}T)"
proof
{
assume "K{is compact in}T"
then have sub:"K ⊆ ⋃T" and reg:"(∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ FinPow(M). K ⊆ ⋃N))"
using IsCompact_def by auto
{
fix M
assume "M∈Pow(T)""K⊆⋃M"
with reg obtain N where "N∈FinPow(M)" "K⊆⋃N" by blast
then have "Finite(N)" using FinPow_def by auto
then obtain n where A:"n∈nat""N ≈n" using Finite_def by auto
from A(1) have "n≺nat" using n_lesspoll_nat by auto
with A(2) have "N≲nat" using lesspoll_def eq_lepoll_trans by auto
moreover
{
assume "N ≈nat"
then have "nat ≈ N" using eqpoll_sym by auto
with A(2) have "nat ≈n" using eqpoll_trans by blast
then have "n ≈nat" using eqpoll_sym by auto
with ‹n≺nat› have "False" using lesspoll_def by auto
}
then have "~(N ≈nat)" by auto
with calculation ‹K⊆⋃N›‹N∈FinPow(M)› have "N≺nat""K⊆⋃N""N∈Pow(M)" using lesspoll_def
FinPow_def by auto
hence "(∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat)" by auto
}
with sub show "K{is compact of cardinal} nat {in}T" using IsCompactOfCard_def Card_nat by auto
}
{
assume "(K{is compact of cardinal} nat {in}T)"
then have sub:"K⊆⋃T" and reg:"(∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat))"
using IsCompactOfCard_def by auto
{
fix M
assume "M∈Pow(T)""K⊆⋃M"
with reg have "(∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat)" by auto
then obtain N where "N∈Pow(M)""K⊆⋃N""N≺nat" by blast
then have "N∈FinPow(M)""K⊆⋃N" using lesspoll_nat_is_Finite FinPow_def by auto
hence "∃N∈FinPow(M). K⊆⋃N" by auto
}
with sub show "K{is compact in}T" using IsCompact_def by auto
}
qed
text‹Another property of this kind widely used is the Lindeloef property;
it is the one on the successor of the natural numbers.›
definition
IsLindeloef ("_{is lindeloef in}_" 90) where
"K {is lindeloef in} T≡K{is compact of cardinal}csucc(nat){in}T"
text‹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.›
text‹However, if the topology has not many open sets, then the topological
space is indeed compact.›
theorem card_top_comp:
assumes "Card(Q)" "T≺Q" "K⊆⋃T"
shows "(K){is compact of cardinal}Q{in}T"
proof-
{
fix M assume M:"M⊆T" "K⊆⋃M"
from M(1) assms(2) have "M≺Q" using subset_imp_lepoll lesspoll_trans1 by blast
with M(2) have "∃N∈Pow(M). K⊆⋃N ∧ N≺Q" by auto
}
with assms(1,3) show ?thesis unfolding IsCompactOfCard_def by auto
qed
text‹The union of two compact sets, is compact; of any cardinality.›
theorem union_compact:
assumes "K{is compact of cardinal}Q{in}T" "K1{is compact of cardinal}Q{in}T" "InfCard(Q)"
shows "(K ∪ K1){is compact of cardinal}Q{in}T" unfolding IsCompactOfCard_def
proof(safe)
from assms(1) show "Card(Q)" unfolding IsCompactOfCard_def by auto
fix x assume "x∈K" then show "x∈⋃T" using assms(1) unfolding IsCompactOfCard_def by blast
next
fix x assume "x∈K1" then show "x∈⋃T" using assms(2) unfolding IsCompactOfCard_def by blast
next
fix M assume "M⊆T" "K∪K1⊆⋃M"
then have "K⊆⋃M""K1⊆⋃M" by auto
with ‹M⊆T› have "∃N∈Pow(M). K ⊆ ⋃N ∧ N ≺ Q""∃N∈Pow(M). K1 ⊆ ⋃N ∧ N ≺ Q" using assms unfolding IsCompactOfCard_def
by auto
then obtain NK NK1 where "NK∈Pow(M)""NK1∈Pow(M)""K ⊆ ⋃NK""K1 ⊆ ⋃NK1""NK ≺ Q""NK1 ≺ Q" by auto
then have "NK∪NK1 ≺ Q""K∪K1⊆⋃(NK∪NK1)""NK∪NK1∈Pow(M)" using assms(3) less_less_imp_un_less by auto
then show "∃N∈Pow(M). K∪K1⊆⋃N ∧ N≺Q" by auto
qed
text‹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⊆T" and "⋃T1=⋃T" and "(K){is compact of cardinal}Q{in}T"
shows "(K){is compact of cardinal}Q{in}T1"
proof-
{
fix M
assume AS:"M∈Pow(T1)""K⊆⋃M"
then have "M∈Pow(T)""K⊆⋃M" using assms(1) by auto
then have "∃N∈Pow(M).K⊆⋃N∧N≺Q" using assms(3) unfolding IsCompactOfCard_def by auto
}
then show "(K){is compact of cardinal}Q{in}T1" using assms(3,2) unfolding IsCompactOfCard_def by auto
qed
text‹If some set is compact for some cardinal, it is compact for any greater cardinal.›
theorem compact_greater_card:
assumes "Q≲Q1" and "(K){is compact of cardinal}Q{in}T" and "Card(Q1)"
shows "(K){is compact of cardinal}Q1{in}T"
proof-
{
fix M
assume AS: "M∈Pow(T)""K⊆⋃M"
then have "∃N∈Pow(M).K⊆⋃N∧N≺Q" using assms(2) unfolding IsCompactOfCard_def by auto
then have "∃N∈Pow(M).K⊆⋃N∧N≺Q1" using assms(1) lesspoll_trans2
unfolding IsCompactOfCard_def by auto
}
then show ?thesis using assms(2,3) unfolding IsCompactOfCard_def by auto
qed
text‹A closed subspace of a compact space of any cardinality, is also
compact of the same cardinality.›
theorem compact_closed:
assumes "K {is compact of cardinal} Q {in} T"
and "R {is closed in} T"
shows "(K∩R) {is compact of cardinal} Q {in} T"
proof-
{
fix M
assume AS:"M∈Pow(T)""K∩R⊆⋃M"
have "⋃T-R∈T" using assms(2) IsClosed_def by auto
have "K-R⊆(⋃T-R)" using assms(1) IsCompactOfCard_def by auto
with ‹⋃T-R∈T› have "K⊆⋃(M ∪{⋃T-R})" and "M ∪{⋃T-R}∈Pow(T)"
proof (safe)
{
fix x
assume "x∈M"
with AS(1) show "x∈T" by auto
}
{
fix x
assume "x∈K"
have "x∈R∨x∉R" by auto
with ‹x∈K› have "x∈K∩R∨x∈K-R" by auto
with AS(2) ‹K-R⊆(⋃T-R)› have "x∈⋃M∨x∈(⋃T-R)" by auto
then show "x∈⋃(M ∪{⋃T-R})" by auto
}
qed
with assms(1) have "∃N∈Pow(M∪{⋃T-R}). K ⊆ ⋃N ∧ N ≺ Q" unfolding IsCompactOfCard_def by auto
then obtain N where cub:"N∈Pow(M∪{⋃T-R})" "K⊆⋃N" "N≺Q" by auto
have "N-{⋃T-R}∈Pow(M)""K∩R⊆⋃(N-{⋃T-R})" "N-{⋃T-R}≺Q"
proof (safe)
{
fix x
assume "x∈N""x∉M"
then show "x=⋃T-R" using cub(1) by auto
}
{
fix x
assume "x∈K""x∈R"
then have "x∉⋃T-R""x∈K" by auto
then show "x∈⋃(N-{⋃T-R})" using cub(2) by blast
}
have "N-{⋃T-R}⊆N" by auto
with cub(3) show "N-{⋃T-R}≺Q" using subset_imp_lepoll lesspoll_trans1 by blast
qed
then have "∃N∈Pow(M). K∩R⊆⋃N ∧ N≺Q" by auto
}
then have "∀M∈Pow(T). (K ∩ R ⊆ ⋃M ⟶ (∃N∈Pow(M). K ∩ R ⊆ ⋃N ∧ N ≺ Q))" by auto
then show ?thesis using IsCompactOfCard_def assms(1) by auto
qed
subsection‹Properties of numerability›
text‹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.›
definition
IsFirstOfCard ("_ {is of first type of cardinal}_" 90) where
"(T {is of first type of cardinal} Q) ≡ ∀x∈⋃T. (∃B. (B {is a base for} T) ∧ ({b∈B. x∈b} ≺ Q))"
definition
IsSecondOfCard ("_ {is of second type of cardinal}_" 90) where
"(T {is of second type of cardinal}Q) ≡ (∃B. (B {is a base for} T) ∧ (B ≺ Q))"
definition
IsSeparableOfCard ("_{is separable of cardinal}_" 90) where
"T{is separable of cardinal}Q≡ ∃U∈Pow(⋃T). Closure(U,T)=⋃T ∧ U≺Q"
definition
IsFirstCountable ("_ {is first countable}" 90) where
"(T {is first countable}) ≡ T {is of first type of cardinal} csucc(nat)"
definition
IsSecondCountable ("_ {is second countable}" 90) where
"(T {is second countable}) ≡ (T {is of second type of cardinal}csucc(nat))"
definition
IsSeparable ("_{is separable}" 90) where
"T{is separable}≡ T{is separable of cardinal}csucc(nat)"
text‹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{is of second type of cardinal}Q"
shows "T{is of first type of cardinal}Q"
proof-
from assms have "∃B. (B {is a base for} T) ∧ (B ≺ Q)" using IsSecondOfCard_def by auto
then obtain B where base:"(B {is a base for} T) ∧ (B ≺ Q)" by auto
{
fix x
assume "x∈⋃T"
have "{b∈B. x∈b}⊆B" by auto
then have "{b∈B. x∈b}≲B" using subset_imp_lepoll by auto
with base have "{b∈B. x∈b}≺Q" using lesspoll_trans1 by auto
with base have "(B {is a base for} T) ∧ {b∈B. x∈b}≺Q" by auto
}
then have "∀x∈⋃T. ∃B. (B {is a base for} T) ∧ {b∈B. x∈b}≺Q" by auto
then show ?thesis using IsFirstOfCard_def by auto
qed
text‹A set is dense iff it intersects all non-empty, open sets of the topology.›
lemma dense_int_open:
assumes "T{is a topology}" and "A⊆⋃T"
shows "Closure(A,T)=⋃T ⟷ (∀U∈T. U≠0 ⟶ A∩U≠0)"
proof
assume AS:"Closure(A,T)=⋃T"
{
fix U
assume Uopen:"U∈T" and "U≠0"
then have "U∩⋃T≠0" by auto
with AS have "U∩Closure(A,T) ≠0" by auto
with assms Uopen have "U∩A≠0" using topology0.cl_inter_neigh topology0_def by blast
}
then show "∀U∈T. U≠0 ⟶ A∩U≠0" by auto
next
assume AS:"∀U∈T. U≠0 ⟶ A∩U≠0"
{
fix x
assume A:"x∈⋃T"
then have "∀U∈T. x∈U ⟶ U∩A≠0" using AS by auto
with assms A have "x∈Closure(A,T)" using topology0.inter_neigh_cl topology0_def by auto
}
then have "⋃T⊆Closure(A,T)" by auto
with assms show "Closure(A,T)=⋃T" using topology0.Top_3_L11(1) topology0_def by blast
qed
subsection‹Relations between numerability properties and choice principles›
text‹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 ‹csucc(Q)› is
separable of cardinality ‹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.›
text‹If a topology is of second type of cardinal ‹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 ‹⋃T›.›
theorem Q_choice_imp_second_imp_separable:
assumes "T{is of second type of cardinal}csucc(Q)"
and "{the axiom of} Q {choice holds for subsets} ⋃T"
and "T{is a topology}"
shows "T{is separable of cardinal}csucc(Q)"
proof-
from assms(1) have "∃B. (B {is a base for} T) ∧ (B ≺ csucc(Q))" using IsSecondOfCard_def by auto
then obtain B where base:"(B {is a base for} T) ∧ (B ≺ csucc(Q))" by auto
let ?N="λb∈B. b"
let ?B="B-{0}"
have "B-{0}⊆B" by auto
with base have prec:"B-{0}≺csucc(Q)" using subset_imp_lepoll lesspoll_trans1 by blast
from base have baseOpen:"∀b∈B. ?N`b∈T" using base_sets_open by auto
from assms(2) have car:"Card(Q)" and reg:"(∀ M N. (M ≲Q ∧ (∀t∈M. N`t≠0 ∧ N`t⊆⋃T)) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t)))"
using AxiomCardinalChoice_def by auto
then have "(?B ≲Q ∧ (∀t∈?B. ?N`t≠0 ∧ ?N`t⊆⋃T)) ⟶ (∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t))" by blast
with prec have "(∀t∈?B. ?N`t⊆⋃T) ⟶ (∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t))" using Card_less_csucc_eq_le car by auto
with baseOpen have "∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t)" by blast
then obtain f where f:"f:Pi(?B,λt. ?N`t)" and f2:"∀t∈?B. f`t∈?N`t" by auto
{
fix U
assume "U∈T" and "U≠0"
then obtain b where A1:"b∈B-{0}" and "b⊆U" using Top_1_2_L1 base by blast
with f2 have "f`b∈U" by auto
with A1 have "{f`b. b∈?B}∩U≠0" by auto
}
then have r:"∀U∈T. U≠0 ⟶ {f`b. b∈?B}∩U≠0" by auto
have "{f`b. b∈?B}⊆⋃T" using f2 baseOpen by auto
moreover
with r have "Closure({f`b. b∈?B},T)=⋃T" using dense_int_open assms(3) by auto
moreover
have ffun:"f:?B→range(f)" using f range_of_fun by auto
then have "f∈surj(?B,range(f))" using fun_is_surj by auto
then have des1:"range(f)≲?B" using surj_fun_inv_2[of "f""?B""range(f)""Q"] prec Card_less_csucc_eq_le car
Card_is_Ord by auto
then have "{f`b. b∈?B}⊆range(f)" using apply_rangeI[OF ffun] by auto
then have "{f`b. b∈?B}≲range(f)" using subset_imp_lepoll by auto
with des1 have "{f`b. b∈?B}≲?B" using lepoll_trans by blast
with prec have "{f`b. b∈?B}≺csucc(Q)" using lesspoll_trans1 by auto
ultimately show ?thesis using IsSeparableOfCard_def by auto
qed
text‹The next theorem resolves that the axiom of ‹Q› choice for subsets
of ‹⋃T› is necessary for second type spaces to be separable of the same cardinal
‹csucc(Q)›.›
theorem second_imp_separable_imp_Q_choice:
assumes "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ (T{is separable of cardinal}csucc(Q))"
and "Card(Q)"
shows "{the axiom of} Q {choice holds}"
proof-
{
fix N M
assume AS:"M ≲Q ∧ (∀t∈M. N`t≠0)"
then obtain h where inj:"h∈inj(M,Q)" using lepoll_def by auto
then have bij:"converse(h):bij(range(h),M)" using inj_bij_range bij_converse_bij by auto
let ?T="{(N`(converse(h)`i))×{i}. i∈range(h)}"
{
fix j
assume AS2:"j∈range(h)"
from bij have "converse(h):range(h)→M" using bij_def inj_def by auto
with AS2 have "converse(h)`j∈M" by simp
with AS have "N`(converse(h)`j)≠0" by auto
then have "(N`(converse(h)`j))×{j}≠0" by auto
}
then have noEmpty:"0∉?T" by auto
moreover
{
fix A B
assume AS2:"A∈?T""B∈?T""A∩B≠0"
then obtain j t where A_def:"A=N`(converse(h)`j)×{j}" and B_def:"B=N`(converse(h)`t)×{t}"
and Range:"j∈range(h)" "t∈range(h)" by auto
from AS2(3) obtain x where "x∈A∩B" by auto
with A_def B_def have "j=t" by auto
with A_def B_def have "A=B" by auto
}
then have "(∀A∈?T. ∀B∈?T. A=B∨ A∩B=0)" by auto
ultimately
have Part:"?T {is a partition of} ⋃?T" unfolding IsAPartition_def by auto
let ?τ="PTopology ⋃?T ?T"
from Part have top:"?τ {is a topology}" and base:"?T {is a base for}?τ"
using Ptopology_is_a_topology by auto
let ?f="{⟨i,(N`(converse(h)`i))×{i}⟩. i∈range(h)}"
have "?f:range(h)→?T" using functionI[of "?f"] Pi_def by auto
then have "?f∈surj(range(h),?T)" unfolding surj_def using apply_equality by auto
moreover
have "range(h)⊆Q" using inj unfolding inj_def range_def domain_def Pi_def by auto
ultimately have "?T≲ Q" using surj_fun_inv[of "?f""range(h)""?T""Q"] assms(2) Card_is_Ord lepoll_trans
subset_imp_lepoll by auto
then have "?T≺csucc(Q)" using Card_less_csucc_eq_le assms(2) by auto
with base have "(?τ{is of second type of cardinal}csucc(Q))" using IsSecondOfCard_def by auto
with top have "?τ{is separable of cardinal}csucc(Q)" using assms(1) by auto
then obtain D where sub:"D∈Pow(⋃?τ)" and clos:"Closure(D,?τ)=⋃?τ" and cardd:"D≺csucc(Q)"
using IsSeparableOfCard_def by auto
then have "D≲Q" using Card_less_csucc_eq_le assms(2) by auto
then obtain r where r:"r∈inj(D,Q)" using lepoll_def by auto
then have bij2:"converse(r):bij(range(r),D)" using inj_bij_range bij_converse_bij by auto
then have surj2:"converse(r):surj(range(r),D)" using bij_def by auto
let ?R="λi∈range(h). {j∈range(r). converse(r)`j∈((N`(converse(h)`i))×{i})}"
{
fix i
assume AS:"i∈range(h)"
then have T:"(N`(converse(h)`i))×{i}∈?T" by auto
then have P: "(N`(converse(h)`i))×{i}∈?τ" using base unfolding IsAbaseFor_def by blast
with top sub clos have "∀U∈?τ. U≠0 ⟶ D∩U≠0" using dense_int_open by auto
with P have "(N`(converse(h)`i))×{i}≠0 ⟶ D∩(N`(converse(h)`i))×{i}≠0" by auto
with T noEmpty have "D∩(N`(converse(h)`i))×{i}≠0" by auto
then obtain x where "x∈D" and px:"x∈(N`(converse(h)`i))×{i}" by auto
with surj2 obtain j where "j∈range(r)" and "converse(r)`j=x" unfolding surj_def by blast
with px have "j∈{j∈range(r). converse(r)`j∈((N`(converse(h)`i))×{i})}" by auto
then have "?R`i≠0" using beta_if[of "range(h)" _ i] AS by auto
}
then have nonE:"∀i∈range(h). ?R`i≠0" by auto
{
fix i j
assume i:"i∈range(h)" and j:"j∈?R`i"
from j i have "converse(r)`j∈((N`(converse(h)`i))×{i})" using beta_if by auto
}
then have pp:"∀i∈range(h). ∀j∈?R`i. converse(r)`j∈((N`(converse(h)`i))×{i})" by auto
let ?E="{⟨m,fst(converse(r)`(μ j. j∈?R`(h`m)))⟩. m∈M}"
have ff:"function(?E)" unfolding function_def by auto
moreover
{
fix m
assume M:"m∈M"
with inj have hm:"h`m∈range(h)" using apply_rangeI inj_def by auto
{
fix j
assume "j∈?R`(h`m)"
with hm have "j∈range(r)" using beta_if by auto
from r have "r:surj(D,range(r))" using fun_is_surj inj_def by auto
with ‹j∈range(r)› obtain d where "d∈D" and "r`d=j" using surj_def by auto
then have "j∈Q" using r inj_def by auto
}
then have subcar:"?R`(h`m)⊆Q" by blast
from nonE hm obtain ee where P:"ee∈?R`(h`m)" by blast
with subcar have "ee∈Q" by auto
then have "Ord(ee)" using assms(2) Card_is_Ord Ord_in_Ord by auto
with P have "(μ j. j∈?R`(h`m))∈?R`(h`m)" using LeastI[where i=ee and P="λj. j∈?R`(h`m)"]
by auto
with pp hm have "converse(r)`(μ j. j∈?R`(h`m))∈((N`(converse(h)`(h`m)))×{(h`m)})" by auto
then have "converse(r)`(μ j. j∈?R`(h`m))∈((N`(m))×{(h`m)})" using left_inverse[OF inj M]
by simp
then have "fst(converse(r)`(μ j. j∈?R`(h`m)))∈(N`(m))" by auto
}
ultimately have thesis1:"∀m∈M. ?E`m∈(N`(m))" using function_apply_equality by auto
{
fix e
assume "e∈?E"
then obtain m where "m∈M" and "e=⟨m,?E`m⟩" using function_apply_equality ff by auto
with thesis1 have "e∈Sigma(M,λt. N`t)" by auto
}
then have "?E∈Pow(Sigma(M,λt. N`t))" by auto
with ff have "?E∈Pi(M,λm. N`m)" using Pi_iff by auto
then have "(∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using thesis1 by auto
}
then show ?thesis using AxiomCardinalChoiceGen_def assms(2) by auto
qed
text‹Here is the equivalence from the two previous results.›
theorem Q_choice_eq_secon_imp_sepa:
assumes "Card(Q)"
shows "(∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ (T{is separable of cardinal}csucc(Q)))
⟷({the axiom of} Q {choice holds})"
using Q_choice_imp_second_imp_separable choice_subset_imp_choice
using second_imp_separable_imp_Q_choice assms by auto
text‹Given 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 ≲Q" "B {is a base for}T"
shows "∃N. {N`i. i∈Q}{is a base for}T"
proof-
from assms obtain f where f_def:"f∈inj(B,Q)" unfolding lepoll_def by auto
let ?ff="{⟨b,f`b⟩. b∈B}"
have "domain(?ff)=B" by auto
moreover
have "relation(?ff)" unfolding relation_def by auto
moreover
have "function(?ff)" unfolding function_def by auto
ultimately
have fun:"?ff:B→range(?ff)" using function_imp_Pi[of "?ff"] by auto
then have injj:"?ff∈inj(B,range(?ff))" unfolding inj_def
proof
{
fix w x
assume AS:"w∈B""x∈B""{⟨b, f ` b⟩ . b ∈ B} ` w = {⟨b, f ` b⟩ . b ∈ B} ` x"
then have "f`w=f`x" using apply_equality[OF _ fun] by auto
then have "w=x" using f_def inj_def AS(1,2) by auto
}
then show "∀w∈B. ∀x∈B. {⟨b, f ` b⟩ . b ∈ B} ` w = {⟨b, f ` b⟩ . b ∈ B} ` x ⟶ w = x" by auto
qed
then have bij:"?ff∈bij(B,range(?ff))" using inj_bij_range by auto
from fun have "range(?ff)={f`b. b∈B}" by auto
with f_def have ran:"range(?ff)⊆Q" using inj_def by auto
let ?N="{⟨i,(if i∈range(?ff) then converse(?ff)`i else 0)⟩. i∈Q}"
have FN:"function(?N)" unfolding function_def by auto
have "B ⊆{?N`i. i∈Q}"
proof
fix t
assume a:"t∈B"
from bij have rr:"?ff:B→range(?ff)" unfolding bij_def inj_def by auto
have ig:"?ff`t=f`t" using a apply_equality[OF _ rr] by auto
have r:"?ff`t∈range(?ff)" using apply_type[OF rr a].
from ig have t:"?ff`t∈Q" using apply_type[OF _ a] f_def unfolding inj_def by auto
with r have "?N`(?ff`t)=converse(?ff)`(?ff`t)" using function_apply_equality[OF _ FN] by auto
then have "?N`(?ff`t)=t" using left_inverse[OF injj a] by auto
then have "t=?N`(?ff`t)" by auto
then have "∃i∈Q. t=?N`i" using t(1) by auto
then show "t∈{?N`i. i∈Q}" by simp
qed
moreover
have "∀r∈{?N`i. i∈Q}-B. r=0"
proof
fix r
assume "r∈{?N`i. i∈Q}-B"
then obtain j where R:"j∈Q""r=?N`j""r∉B" by auto
{
assume AS:"j∈range(?ff)"
with R(1) have "?N`j=converse(?ff)`j" using function_apply_equality[OF _ FN] by auto
then have "?N`j∈B" using apply_funtype[OF inj_is_fun[OF bij_is_inj[OF bij_converse_bij[OF bij]]] AS]
by auto
then have "False" using R(3,2) by auto
}
then have "j∉range(?ff)" by auto
then show "r=0" using function_apply_equality[OF _ FN] R(1,2) by auto
qed
ultimately have "{?N`i. i∈Q}=B∨{?N`i. i∈Q}=B ∪{0}" by blast
moreover
have "(B ∪{0})-{0}=B-{0}" by blast
then have "(B ∪{0})-{0} {is a base for}T" using base_no_0[of "B""T"] assms(2) by auto
then have "B ∪{0} {is a base for}T" using base_no_0[of "B ∪{0}""T"] by auto
ultimately
have "{?N`i. i∈Q}{is a base for}T" using assms(2) by auto
then show ?thesis by auto
qed
subsection‹Relation between numerability and compactness›
text‹If the axiom of ‹Q› choice holds, then any topology
of second type of cardinal ‹csucc(Q)› is compact of cardinal ‹csucc(Q)››
theorem compact_of_cardinal_Q:
assumes "{the axiom of} Q {choice holds for subsets} (Pow(Q))"
"T{is of second type of cardinal}csucc(Q)"
"T{is a topology}"
shows "((⋃T){is compact of cardinal}csucc(Q){in}T)"
proof-
from assms(1) have CC:"Card(Q)" and reg:"⋀ M N. (M ≲Q ∧ (∀t∈M. N`t≠0∧N`t⊆Pow(Q))) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using
AxiomCardinalChoice_def by auto
from assms(2) obtain R where "R≲Q""R{is a base for}T" unfolding IsSecondOfCard_def using Card_less_csucc_eq_le CC by auto
with base_to_indexed_base obtain N where base:"{N`i. i∈Q}{is a base for}T" by blast
{
fix M
assume A:"⋃T⊆⋃M""M∈Pow(T)"
let ?α="λU∈M. {i∈Q. N`(i)⊆U}"
have inj:"?α∈inj(M,Pow(Q))" unfolding inj_def
proof
{
show "(λU∈M. {i ∈ Q . N ` i ⊆ U}) ∈ M → Pow(Q)" using lam_type[of "M""λU. {i ∈ Q . N`(i) ⊆ U}""%t. Pow(Q)"] by auto
{
fix w x
assume AS:"w∈M""x∈M""{i ∈ Q . N`(i) ⊆ w} = {i ∈ Q . N`(i) ⊆ x}"
from AS(1,2) A(2) have "w∈T""x∈T" by auto
then have "w=Interior(w,T)""x=Interior(x,T)" using assms(3) topology0.Top_2_L3[of "T"]
topology0_def[of "T"] by auto
then have UN:"w=(⋃{B∈{N`(i). i∈Q}. B⊆w})""x=(⋃{B∈{N`(i). i∈Q}. B⊆x})"
using interior_set_base_topology assms(3) base by auto
{
fix b
assume "b∈w"
then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆w}" using UN(1) by auto
then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆w" by blast
then obtain j where j:"j∈Q""S=N`(j)" by auto
then have "j∈{i ∈ Q . N`(i) ⊆ w}" using S(3) by auto
then have "N`(j)⊆x""b∈N`(j)""j∈Q" using S(2) AS(3) j by auto
then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆x})" by auto
then have "b∈x" using UN(2) by auto
}
moreover
{
fix b
assume "b∈x"
then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆x}" using UN(2) by auto
then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆x" by blast
then obtain j where j:"j∈Q""S=N`(j)" by auto
then have "j∈{i ∈ Q . N`(i) ⊆ x}" using S(3) by auto
then have "j∈{i ∈ Q . N`(i) ⊆ w}" using AS(3) by auto
then have "N`(j)⊆w""b∈N`(j)""j∈Q" using S(2) j(2) by auto
then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆w})" by auto
then have "b∈w" using UN(2) by auto
}
ultimately have "w=x" by auto
}
then show "∀w∈M. ∀x∈M. (λU∈M. {i ∈ Q . N ` i ⊆ U}) ` w = (λU∈M. {i ∈ Q . N ` i ⊆ U}) ` x ⟶ w = x" by auto
}
qed
let ?X="λi∈Q. {?α`U. U∈{V∈M. N`(i)⊆V}}"
let ?M="{i∈Q. ?X`i≠0}"
have subMQ:"?M⊆Q" by auto
then have ddd:"?M ≲Q" using subset_imp_lepoll by auto
then have "?M ≲Q""∀i∈?M. ?X`i≠0""∀i∈?M. ?X`i⊆Pow(Q)" by auto
then have "?M ≲Q""∀i∈?M. ?X`i≠0""∀i∈?M. ?X`i ≲ Pow(Q)" using subset_imp_lepoll by auto
then have "(∃f. f:Pi(?M,λt. ?X`t) ∧ (∀t∈?M. f`t∈?X`t))" using reg[of "?M""?X"] by auto
then obtain f where f:"f:Pi(?M,λt. ?X`t)""(!!t. t∈?M ⟹ f`t∈?X`t)" by auto
{
fix m
assume S:"m∈?M"
from f(2) S obtain YY where YY:"(YY∈M)" "(f`m=?α`YY)" by auto
then have Y:"(YY∈M)∧(f`m=?α`YY)" by auto
moreover
{
fix U
assume "U∈M∧(f`m=?α`U)"
then have "U=YY" using inj inj_def YY by auto
}
then have r:"⋀x. x∈M∧(f`m=?α`x) ⟹ x=YY" by blast
have "∃!YY. YY∈M ∧ f`m=?α`YY" using ex1I[of "%Y. Y∈M∧ f`m=?α`Y",OF Y r] by auto
}
then have ex1YY:"∀m∈?M. ∃!YY. YY∈M ∧ f`m=?α`YY" by auto
let ?YYm="{⟨m,(THE YY. YY∈M ∧ f`m=?α`YY)⟩. m∈?M}"
have aux:"⋀m. m∈?M ⟹ ?YYm`m=(THE YY. YY∈M ∧ f`m=?α`YY)" unfolding apply_def by auto
have ree:"∀m∈?M. (?YYm`m)∈M ∧ f`m=?α`(?YYm`m)"
proof
fix m
assume C:"m∈?M"
then have "∃!YY. YY∈M ∧ f`m=?α`YY" using ex1YY by auto
then have "(THE YY. YY∈M ∧ f`m=?α`YY)∈M∧f`m=?α`(THE YY. YY∈M ∧ f`m=?α`YY)"
using theI[of "%Y. Y∈M∧ f`m=?α`Y"] by blast
then show "(?YYm`m)∈M ∧ f`m=?α`(?YYm`m)" apply (simp only: aux[OF C]) done
qed
have tt:"⋀m. m∈?M ⟹ N`(m)⊆?YYm`m"
proof-
fix m
assume D:"m∈?M"
then have QQ:"m∈Q" by auto
from D have t:"(?YYm`m)∈M ∧ f`m=?α`(?YYm`m)" using ree by blast
then have "f`m=?α`(?YYm`m)" by blast
then have "(?α`(?YYm`m))∈(λi∈Q. {?α`U. U∈{V∈M. N`(i)⊆V}})`m" using f(2)[OF D]
by auto
then have "(?α`(?YYm`m))∈{?α`U. U∈{V∈M. N`(m)⊆V}}" using QQ by auto
then obtain U where "U∈{V∈M. N`(m)⊆V}""?α`(?YYm`m)=?α`U" by auto
then have r:"U∈M""N`(m)⊆U""?α`(?YYm`m)=?α`U""(?YYm`m)∈M" using t by auto
then have "?YYm`m=U" using inj_apply_equality[OF inj] by blast
then show "N`(m)⊆?YYm`m" using r by auto
qed
then have "(⋃m∈?M. N`(m))⊆(⋃m∈?M. ?YYm`m)"
proof-
{
fix s
assume "s∈(⋃m∈?M. N`(m))"
then obtain t where r:"t∈?M""s∈N`(t)" by auto
then have "s∈?YYm`t" using tt[OF r(1)] by blast
then have "s∈(⋃m∈?M. ?YYm`m)" using r(1) by blast
}
then show ?thesis by blast
qed
moreover
{
fix x
assume AT:"x∈⋃T"
with A obtain U where BB:"U∈M""U∈T""x∈U" by auto
then obtain j where BC:"j∈Q" "N`(j)⊆U""x∈N`(j)" using point_open_base_neigh[OF base,of "U""x"] by auto
then have "?X`j≠0" using BB(1) by auto
then have "j∈?M" using BC(1) by auto
then have "x∈(⋃m∈?M. N`(m))" using BC(3) by auto
}
then have "⋃T⊆(⋃m∈?M. N`(m))" by blast
ultimately have covers:"⋃T⊆(⋃m∈?M. ?YYm`m)" using subset_trans[of "⋃T""(⋃m∈?M. N`(m))""(⋃m∈?M. ?YYm`m)"]
by auto
have "relation(?YYm)" unfolding relation_def by auto
moreover
have f:"function(?YYm)" unfolding function_def by auto
moreover
have d:"domain(?YYm)=?M" by auto
moreover
have r:"range(?YYm)=?YYm``?M" by auto
ultimately
have fun:"?YYm:?M→?YYm``?M" using function_imp_Pi[of "?YYm"] by auto
have "?YYm∈surj(?M,?YYm``?M)" using fun_is_surj[OF fun] r by auto
with surj_fun_inv[OF this subMQ Card_is_Ord[OF CC]]
have "?YYm``?M ≲ ?M" by auto
with ddd have Rw:"?YYm``?M ≲Q" using lepoll_trans by blast
{
fix m assume "m∈?M"
then have "⟨m,?YYm`m⟩∈?YYm" using function_apply_Pair[OF f] d by blast
then have "?YYm`m∈?YYm``?M" by auto}
then have l1:"{?YYm`m. m∈?M}⊆?YYm``?M" by blast
{
fix t assume "t∈?YYm``?M"
then have "∃x∈?M. ⟨x,t⟩∈?YYm" unfolding image_def by auto
then obtain r where S:"r∈?M""⟨r,t⟩∈?YYm" by auto
have "?YYm`r=t" using apply_equality[OF S(2) fun] by auto
with S(1) have "t∈{?YYm`m. m∈?M}" by auto
}
with l1 have "{?YYm`m. m∈?M}=?YYm``?M" by blast
with Rw have "{?YYm`m. m∈?M} ≲Q" by auto
with covers have "{?YYm`m. m∈?M}∈Pow(M)∧⋃T⊆⋃{?YYm`m. m∈?M}∧{?YYm`m. m∈?M} ≺csucc(Q)" using ree
Card_less_csucc_eq_le[OF CC] by blast
then have "∃N∈Pow(M). ⋃T⊆⋃N∧N≺csucc(Q)" by auto
}
then have "∀M∈Pow(T). ⋃T ⊆ ⋃M ⟶ (∃N∈Pow(M). ⋃T ⊆ ⋃N ∧ N ≺ csucc(Q))" by auto
then show ?thesis using IsCompactOfCard_def Card_csucc CC Card_is_Ord by auto
qed
text‹In the following proof, we have chosen an infinite cardinal
to be able to apply the equation @{prop "Q×Q≈Q"}. For finite cardinals;
both, the assumption and the axiom of choice, are always true.›
theorem second_imp_compact_imp_Q_choice_PowQ:
assumes "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T)"
and "InfCard(Q)"
shows "{the axiom of} Q {choice holds for subsets} (Pow(Q))"
proof-
{
fix N M
assume AS:"M ≲Q ∧ (∀t∈M. N`t≠0 ∧ N`t⊆Pow(Q))"
then obtain h where "h∈inj(M,Q)" using lepoll_def by auto
have discTop:"Pow(Q×M) {is a topology}" using Pow_is_top by auto
{
fix A
assume AS:"A∈Pow(Q×M)"
have "A=⋃{{i}. i∈A}" by auto
with AS have "∃T∈Pow({{i}. i∈Q×M}). A=⋃T" by auto
then have "A∈{⋃U. U∈Pow({{i}. i∈Q×M})}" by auto
}
moreover
{
fix A
assume AS:"A∈{⋃U. U∈Pow({{i}. i∈Q×M})}"
then have "A∈Pow(Q×M)" by auto
}
ultimately
have base:"{{x}. x∈Q×M} {is a base for} Pow(Q×M)" unfolding IsAbaseFor_def by blast
let ?f="{⟨i,{i}⟩. i∈Q×M}"
have fff:"?f∈Q×M→{{i}. i∈Q×M}" using Pi_def function_def by auto
then have "?f∈inj(Q×M,{{i}. i∈Q×M})" unfolding inj_def using apply_equality by auto
then have "?f∈bij(Q×M,{{i}. i∈Q×M})" unfolding bij_def surj_def using fff
apply_equality fff by auto
then have "Q×M≈{{i}. i∈Q×M}" using eqpoll_def by auto
then have "{{i}. i∈Q×M}≈Q×M" using eqpoll_sym by auto
then have "{{i}. i∈Q×M}≲Q×M" using eqpoll_imp_lepoll by auto
then have "{{i}. i∈Q×M}≲Q×Q" using AS prod_lepoll_mono[of "Q""Q""M""Q"] lepoll_refl[of "Q"]
lepoll_trans by blast
then have "{{i}. i∈Q×M}≲Q" using InfCard_square_eqpoll assms(2) lepoll_eq_trans by auto
then have "{{i}. i∈Q×M}≺csucc(Q)" using Card_less_csucc_eq_le assms(2) InfCard_is_Card by auto
then have "Pow(Q×M) {is of second type of cardinal} csucc(Q)" using IsSecondOfCard_def base by auto
then have comp:"(Q×M) {is compact of cardinal}csucc(Q){in}Pow(Q×M)" using discTop assms(1) by auto
{
fix W
assume "W∈Pow(Q×M)"
then have T:"W{is closed in} Pow(Q×M)" and "(Q×M)∩W=W" using IsClosed_def by auto
with compact_closed[OF comp T] have "(W {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
}
then have subCompact:"∀W∈Pow(Q×M). (W {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
let ?cub="⋃{{(U)×{t}. U∈N`t}. t∈M}"
from AS have "(⋃?cub)∈Pow((Q)×M)" by auto
with subCompact have Ncomp:"((⋃?cub) {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
have cond:"(?cub)∈Pow(Pow(Q×M))∧ ⋃?cub⊆⋃?cub" using AS by auto
have "∃S∈Pow(?cub). (⋃?cub) ⊆ ⋃S ∧ S ≺ csucc(Q)"
proof-
{
have "((⋃?cub) {is compact of cardinal}csucc(Q){in}Pow(Q×M))" using Ncomp by auto
then have "∀M∈Pow(Pow(Q×M)). ⋃?cub ⊆ ⋃M ⟶ (∃Na∈Pow(M). ⋃?cub ⊆ ⋃Na ∧ Na ≺ csucc(Q))"
unfolding IsCompactOfCard_def by auto
with cond have "∃S∈Pow(?cub). ⋃?cub ⊆ ⋃S ∧ S ≺ csucc(Q)" by auto
}
then show ?thesis by auto
qed
then have ttt:"∃S∈Pow(?cub). (⋃?cub) ⊆ ⋃S ∧ S ≲ Q" using Card_less_csucc_eq_le assms(2) InfCard_is_Card by auto
then obtain S where S_def:"S∈Pow(?cub)""(⋃?cub) ⊆ ⋃S" "S ≲ Q" by auto
{
fix t
assume AA:"t∈M""N`t≠{0}"
from AA(1) AS have "N`t≠0" by auto
with AA(2) obtain U where G:"U∈N`t" and notEm:"U≠0" by blast
then have "U×{t}∈?cub" using AA by auto
then have "U×{t}⊆⋃?cub" by auto
with G notEm AA have "∃s. ⟨s,t⟩∈⋃?cub" by auto
}
then have "∀t∈M. (N`t≠{0})⟶ (∃s. ⟨s,t⟩∈⋃?cub)" by auto
then have A:"∀t∈M. (N`t≠{0})⟶ (∃s. ⟨s,t⟩∈⋃S)" using S_def(2) by blast
from S_def(1) have B:"∀f∈S. ∃t∈M. ∃U∈N`t. f=U×{t}" by blast
from A B have "∀t∈M. (N`t≠{0})⟶ (∃U∈N`t. U×{t}∈S)" by blast
then have noEmp:"∀t∈M. (N`t≠{0})⟶ (S∩({U×{t}. U∈N`t})≠0)" by auto
from S_def(3) obtain r where r:"r:inj(S,Q)" using lepoll_def by auto
then have bij2:"converse(r):bij(range(r),S)" using inj_bij_range bij_converse_bij by auto
then have surj2:"converse(r):surj(range(r),S)" using bij_def by auto
let ?R="λt∈M. {j∈range(r). converse(r)`j∈({U×{t}. U∈N`t})}"
{
fix t
assume AA:"t∈M""N`t≠{0}"
then have "(S∩({U×{t}. U∈N`t})≠0)" using noEmp by auto
then obtain s where ss:"s∈S""s∈{U×{t}. U∈N`t}" by blast
then obtain j where "converse(r)`j=s" "j∈range(r)" using surj2 unfolding surj_def by blast
then have "j∈{j∈range(r). converse(r)`j∈({U×{t}. U∈N`t})}" using ss by auto
then have "?R`t≠0" using beta_if AA by auto
}
then have nonE:"∀t∈M. N`t≠{0}⟶?R`t≠0" by auto
{
fix t j
assume "t∈M""j∈?R`t"
then have "converse(r)`j∈{U×{t}. U∈N`t}" using beta_if by auto
}
then have pp:"∀t∈M. ∀j∈?R`t. converse(r)`j∈{U×{t}. U∈N`t}" by auto
have reg:"∀t U V. U×{t}=V×{t}⟶U=V"
proof-
{
fix t U V
assume AA:"U×{t}=V×{t}"
{
fix v
assume "v∈V"
then have "⟨v,t⟩∈V ×{t}" by auto
then have "⟨v,t⟩∈U ×{t}" using AA by auto
then have "v∈U" by auto
}
then have "V⊆U" by auto
moreover
{
fix u
assume "u∈U"
then have "⟨u,t⟩∈U ×{t}" by auto
then have "⟨u,t⟩∈V ×{t}" using AA by auto
then have "u∈V" by auto
}
then have "U⊆V" by auto
ultimately have "U=V" by auto
}
then show ?thesis by auto
qed
let ?E="{⟨t,if N`t={0} then 0 else (THE U. converse(r)`(μ j. j∈?R`t)=U×{t})⟩. t∈M}"
have ff:"function(?E)" unfolding function_def by auto
moreover
{
fix t
assume pm:"t∈M"
{ assume nonEE:"N`t≠{0}"
{
fix j
assume "j∈?R`t"
with pm(1) have "j∈range(r)" using beta_if by auto
from r have "r:surj(S,range(r))" using fun_is_surj inj_def by auto
with ‹j∈range(r)› obtain d where "d∈S" and "r`d=j" using surj_def by auto
then have "j∈Q" using r inj_def by auto
}
then have sub:"?R`t⊆Q" by blast
from nonE pm nonEE obtain ee where P:"ee∈?R`t" by blast
with sub have "ee∈Q" by auto
then have "Ord(ee)" using assms(2) Card_is_Ord Ord_in_Ord InfCard_is_Card by blast
with P have "(μ j. j∈?R`t)∈?R`t" using LeastI[where i=ee and P="λj. j∈?R`t"] by auto
with pp pm have "converse(r)`(μ j. j∈?R`t)∈{U×{t}. U∈N`t}" by auto
then obtain W where "converse(r)`(μ j. j∈?R`t)=W×{t}" and s:"W∈N`t" by auto
then have "(THE U. converse(r)`(μ j. j∈?R`t)=U×{t})=W" using reg by auto
with s have "(THE U. converse(r)`(μ j. j∈?R`t)=U×{t})∈N`t" by auto
}
then have "(if N`t={0} then 0 else (THE U. converse(r)`(μ j. j∈?R`t)=U×{t}))∈N`t" by auto
}
ultimately have thesis1:"∀t∈M. ?E`t∈N`t" using function_apply_equality by auto
{
fix e
assume "e∈?E"
then obtain m where "m∈M" and "e=⟨m,?E`m⟩" using function_apply_equality ff by auto
with thesis1 have "e∈Sigma(M,λt. N`t)" by auto
}
then have "?E∈Pow(Sigma(M,λt. N`t))" by auto
with ff have "?E∈Pi(M,λm. N`m)" using Pi_iff by auto
then have "(∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using thesis1 by auto}
then show ?thesis using AxiomCardinalChoice_def assms(2) InfCard_is_Card by auto
qed
text‹The two previous results, state the following equivalence:›
theorem Q_choice_Pow_eq_secon_imp_comp:
assumes "InfCard(Q)"
shows "(∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T))
⟷({the axiom of} Q {choice holds for subsets} (Pow(Q)))"
using second_imp_compact_imp_Q_choice_PowQ compact_of_cardinal_Q assms by auto
text‹In 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 "InfCard(Q)" "(Q){is compact of cardinal}csucc(Q){in}Pow(Q)"
shows "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T)"
proof
fix T
{
assume top:"T {is a topology}" and sec:"T{is of second type of cardinal}csucc(Q)"
from assms have "Card(csucc(Q))" "Card(Q)" using InfCard_is_Card Card_is_Ord Card_csucc by auto
moreover
have "⋃T⊆⋃T" by auto
moreover
{
fix M
assume MT:"M∈Pow(T)" and cover:"⋃T⊆⋃M"
from sec obtain B where "B {is a base for} T" "B≺csucc(Q)" using IsSecondOfCard_def by auto
with ‹Card(Q)› obtain N where base:"{N`i. i∈Q}{is a base for}T" using Card_less_csucc_eq_le
base_to_indexed_base by blast
let ?S="{⟨u,{i∈Q. N`i⊆u}⟩. u∈M}"
have "function(?S)" unfolding function_def by auto
then have "?S:M→Pow(Q)" using Pi_iff by auto
then have "?S∈inj(M,Pow(Q))" unfolding inj_def
proof
{
fix w x
assume AS:"w∈M""x∈M""{⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` w = {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` x"
with ‹?S:M→Pow(Q)› have ASS:"{i ∈ Q . N ` i ⊆ w}={i ∈ Q . N ` i ⊆ x}" using apply_equality by auto
from AS(1,2) MT have "w∈T""x∈T" by auto
then have "w=Interior(w,T)""x=Interior(x,T)" using top topology0.Top_2_L3[of "T"]
topology0_def[of "T"] by auto
then have UN:"w=(⋃{B∈{N`(i). i∈Q}. B⊆w})""x=(⋃{B∈{N`(i). i∈Q}. B⊆x})"
using interior_set_base_topology top base by auto
{
fix b
assume "b∈w"
then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆w}" using UN(1) by auto
then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆w" by blast
then obtain j where j:"j∈Q""S=N`(j)" by auto
then have "j∈{i ∈ Q . N`(i) ⊆ w}" using S(3) by auto
then have "N`(j)⊆x""b∈N`(j)""j∈Q" using S(2) ASS j by auto
then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆x})" by auto
then have "b∈x" using UN(2) by auto
}
moreover
{
fix b
assume "b∈x"
then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆x}" using UN(2) by auto
then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆x" by blast
then obtain j where j:"j∈Q""S=N`(j)" by auto
then have "j∈{i ∈ Q . N`(i) ⊆ x}" using S(3) by auto
then have "j∈{i ∈ Q . N`(i) ⊆ w}" using ASS by auto
then have "N`(j)⊆w""b∈N`(j)""j∈Q" using S(2) j(2) by auto
then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆w})" by auto
then have "b∈w" using UN(2) by auto
}
ultimately have "w=x" by auto
}
then show "∀w∈M. ∀x∈M. {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` w = {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` x ⟶ w = x" by auto
qed
then have "?S∈bij(M,range(?S))" using fun_is_surj unfolding bij_def inj_def surj_def by force
have "range(?S)⊆Pow(Q)" by auto
then have "range(?S)∈Pow(Pow(Q))" by auto
moreover
have "(⋃(range(?S))) {is closed in} Pow(Q)" "Q∩(⋃range(?S))=(⋃range(?S))" using IsClosed_def by auto
from this(2) compact_closed[OF assms(2) this(1)] have "(⋃range(?S)){is compact of cardinal}csucc(Q) {in}Pow(Q)"
by auto
moreover
have "⋃(range(?S))⊆⋃(range(?S))" by auto
ultimately have "∃S∈Pow(range(?S)). (⋃(range(?S)))⊆⋃S ∧ S≺ csucc(Q)" using IsCompactOfCard_def by auto
then obtain SS where SS_def:"SS⊆range(?S)" "(⋃(range(?S)))⊆⋃SS" "SS≺ csucc(Q)" by auto
with ‹?S∈bij(M,range(?S))› have con:"converse(?S)∈bij(range(?S),M)" using bij_converse_bij by auto
then have r1:"restrict(converse(?S),SS)∈bij(SS,converse(?S)``SS)" using restrict_bij bij_def SS_def(1) by auto
then have rr:"converse(restrict(converse(?S),SS))∈bij(converse(?S)``SS,SS)" using bij_converse_bij by auto
{
fix x
assume "x∈⋃T"
with cover have "x∈⋃M" by auto
then obtain R where "R∈M" "x∈R" by auto
with MT have "R∈T" "x∈R" by auto
then have "∃V∈{N`i. i∈Q}. V⊆R ∧ x∈V" using point_open_base_neigh base by force
then obtain j where "j∈Q" "N`j⊆R" and x_p:"x∈N`j" by auto
with ‹R∈M› ‹?S:M→Pow(Q)› ‹?S∈bij(M,range(?S))› have "?S`R∈range(?S) ∧ j∈?S`R" using apply_equality
bij_def inj_def by auto
from exI[where P="λt. t∈range(?S) ∧ j∈t", OF this] have "∃A∈range(?S). j∈A" unfolding Bex_def
by auto
then have "j∈(⋃(range(?S)))" by auto
then have "j∈⋃SS" using SS_def(2) by blast
then obtain SR where "SR∈SS" "j∈SR" by auto
moreover
have "converse(restrict(converse(?S),SS))∈surj(converse(?S)``SS,SS)" using rr bij_def by auto
ultimately obtain RR where "converse(restrict(converse(?S),SS))`RR=SR" and p:"RR∈converse(?S)``SS" unfolding surj_def by blast
then have "converse(converse(restrict(converse(?S),SS)))`(converse(restrict(converse(?S),SS))`RR)=converse(converse(restrict(converse(?S),SS)))`SR"
by auto
moreover
have "converse(restrict(converse(?S),SS))∈inj(converse(?S)``SS,SS)" using rr unfolding bij_def by auto
moreover
ultimately have "RR=converse(converse(restrict(converse(?S),SS)))`SR" using left_inverse[OF _ p]
by force
moreover
with r1 have "restrict(converse(?S),SS)∈SS→converse(?S)``SS" unfolding bij_def inj_def by auto
then have "relation(restrict(converse(?S),SS))" using Pi_def relation_def by auto
then have "converse(converse(restrict(converse(?S),SS)))=restrict(converse(?S),SS)" using relation_converse_converse by auto
ultimately have "RR=restrict(converse(?S),SS)`SR" by auto
with ‹SR∈SS› have eq:"RR=converse(?S)`SR" unfolding restrict by auto
then have "converse(converse(?S))`RR=converse(converse(?S))`(converse(?S)`SR)" by auto
moreover
with ‹SR∈SS› have "SR∈range(?S)" using SS_def(1) by auto
from con left_inverse[OF _ this] have "converse(converse(?S))`(converse(?S)`SR)=SR" unfolding bij_def
by auto
ultimately have "converse(converse(?S))`RR=SR" by auto
then have "?S`RR=SR" using relation_converse_converse[of "?S"] unfolding relation_def by auto
moreover
have "converse(?S):range(?S)→M" using con bij_def inj_def by auto
with ‹SR∈range(?S)› have "converse(?S)`SR∈M" using apply_funtype
by auto
with eq have "RR∈M" by auto
ultimately have "SR={i∈Q. N`i⊆RR}" using ‹?S:M→Pow(Q)› apply_equality by auto
then have "N`j⊆RR" using ‹j∈SR› by auto
with x_p have "x∈RR" by auto
with p have "x∈⋃(converse(?S)``SS)" by auto
}
then have "⋃T⊆⋃(converse(?S)``SS)" by blast
moreover
{
from con have "converse(?S)``SS={converse(?S)`R. R∈SS}" using image_function[of "converse(?S)" "SS"]
SS_def(1) unfolding range_def bij_def inj_def Pi_def by auto
have "{converse(?S)`R. R∈SS}⊆{converse(?S)`R. R∈range(?S)}" using SS_def(1) by auto
moreover
have "converse(?S):range(?S)→M" using con unfolding bij_def inj_def by auto
then have "{converse(?S)`R. R∈range(?S)}⊆M" using apply_funtype by force
ultimately
have "(converse(?S)``SS)⊆M" by auto
}
then have "converse(?S)``SS∈Pow(M)" by auto
moreover
with rr have "converse(?S)``SS≈SS" using eqpoll_def by auto
then have "converse(?S)``SS≺csucc(Q)" using SS_def(3) eq_lesspoll_trans by auto
ultimately
have "∃N∈Pow(M). ⋃T⊆⋃N ∧ N≺csucc(Q)" by auto
}
then have "∀M∈Pow(T). ⋃T⊆⋃M ⟶ (∃N∈Pow(M). ⋃T⊆⋃N ∧ N≺csucc(Q))" by auto
ultimately have "(⋃T){is compact of cardinal}csucc(Q){in}T" unfolding IsCompactOfCard_def
by auto
}
then show "(T {is a topology}) ∧ (T {is of second type of cardinal}csucc(Q)) ⟶ ((⋃T){is compact of cardinal}csucc(Q) {in}T)"
by auto
qed
theorem Q_disc_is_second_card_csuccQ:
assumes "InfCard(Q)"
shows "Pow(Q){is of second type of cardinal}csucc(Q)"
proof-
{
fix A
assume AS:"A∈Pow(Q)"
have "A=⋃{{i}. i∈A}" by auto
with AS have "∃T∈Pow({{i}. i∈Q}). A=⋃T" by auto
then have "A∈{⋃U. U∈Pow({{i}. i∈Q})}" by auto
}
moreover
{
fix A
assume AS:"A∈{⋃U. U∈Pow({{i}. i∈Q})}"
then have "A∈Pow(Q)" by auto
}
ultimately
have base:"{{x}. x∈Q} {is a base for} Pow(Q)" unfolding IsAbaseFor_def by blast
let ?f="{⟨i,{i}⟩. i∈Q}"
have "?f∈Q→{{x}. x∈Q}" unfolding Pi_def function_def by auto
then have "?f∈inj(Q,{{x}. x∈Q})" unfolding inj_def using apply_equality by auto
moreover
from ‹?f∈Q→{{x}. x∈Q}› have "?f∈surj(Q,{{x}. x∈Q})" unfolding surj_def using apply_equality
by auto
ultimately have "?f∈bij(Q,{{x}. x∈Q})" unfolding bij_def by auto
then have "Q≈{{x}. x∈Q}" using eqpoll_def by auto
then have "{{x}. x∈Q}≈Q" using eqpoll_sym by auto
then have "{{x}. x∈Q}≲Q" using eqpoll_imp_lepoll by auto
then have "{{x}. x∈Q}≺csucc(Q)" using Card_less_csucc_eq_le assms InfCard_is_Card by auto
with base show ?thesis using IsSecondOfCard_def by auto
qed
text‹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 "InfCard(Q)"
shows "(Q{is compact of cardinal}csucc(Q){in}(Pow(Q))) ⟷ ({the axiom of}Q{choice holds for subsets}(Pow(Q)))"
proof
assume "Q{is compact of cardinal}csucc(Q) {in}Pow(Q)"
with assms show "{the axiom of}Q{choice holds for subsets}(Pow(Q))" using Q_choice_Pow_eq_secon_imp_comp Q_csuccQ_comp_eq_Q_choice_Pow
by auto
next
assume "{the axiom of}Q{choice holds for subsets}(Pow(Q))"
with assms show "Q{is compact of cardinal}csucc(Q){in}(Pow(Q))" using Q_disc_is_second_card_csuccQ Q_choice_Pow_eq_secon_imp_comp Pow_is_top[of "Q"]
by force
qed
end