imports Topology_ZF_examples Topology_ZF_examples_1

(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2012 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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 @{text "Q"} for some topology, it is compact of cardinality @{text "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 @{text "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 @{text "csucc(Q)"} is separable of cardinality @{text "csucc(Q)"}. \item The axiom of @{text "Q"} choice. \end{itemize} In the article \cite{HH1} there is a proof of this statement for @{text "Q"}$=\mathbb{N}$, with more equivalences.*} text{*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 @{text "Q"} on subsets of @{text "⋃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 @{text "Q"} choice for subsets of @{text "⋃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 "∀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)" (* First we build a topology using N and M such that it is of second type of cardinal csucc(Q). It will be a partition topology.*) 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 (*We now build a dense subset of D such that it has only one point in each basic set. The first coordinate of those points will give us a choice function.*) 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 op:"(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 op 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 (*We now have to prove that ?E is a choice function for M and N*) { 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 @{text "Q"} choice holds, then any topology of second type of cardinal @{text "csucc(Q)"} is compact of cardinal @{text "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 (* First we build a topology that it is of second type of cardinal csucc(Q). It will be a discrete topology.*) 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 (*The last part is to prove that ?E is the choice function.*) 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 @{text "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