Commit 0c8f8363 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

New (ZF!) entry Delta_System_Lemma

parent a80f4e41ac2b
This diff is collapsed.
This diff is collapsed.
subsection\<open>Application to Cohen posets\label{sec:cohen}\<close>
theory Cohen_Posets
imports
Delta_System
begin
text\<open>We end this session by applying DSL to the combinatorics of
finite function posets. We first define some basic concepts; we take
a different approach from \cite{2020arXiv200109715G}, in that the
order relation is presented as a predicate (of type @{typ \<open>[i,i] \<Rightarrow> o\<close>}).
Two elements of a poset are \<^emph>\<open>compatible\<close> if they have a common lower
bound.\<close>
definition compat_in :: "[i,[i,i]\<Rightarrow>o,i,i]\<Rightarrow>o" where
"compat_in(A,r,p,q) \<equiv> \<exists>d\<in>A . r(d,p) \<and> r(d,q)"
text\<open>An \<^emph>\<open>antichain\<close> is a subset of pairwise incompatible members.\<close>
definition
antichain :: "[i,[i,i]\<Rightarrow>o,i]\<Rightarrow>o" where
"antichain(P,leq,A) \<equiv> A\<subseteq>P \<and> (\<forall>p\<in>A. \<forall>q\<in>A.
p\<noteq>q \<longrightarrow> \<not>compat_in(P,leq,p,q))"
text\<open>A poset has the \<^emph>\<open>countable chain condition\<close> (ccc) if all of its
antichains are countable.\<close>
definition
ccc :: "[i,[i,i]\<Rightarrow>o]\<Rightarrow>o" where
"ccc(P,leq) \<equiv> \<forall>A. antichain(P,leq,A) \<longrightarrow> countable(A)"
text\<open>Finally, the \<^emph>\<open>Cohen poset\<close> is the set of finite partial functions
between two sets with the order of reverse inclusion.\<close>
definition
Fn :: "[i,i] \<Rightarrow> i" where
"Fn(I,J) \<equiv> \<Union>{(d\<rightarrow>J) . d \<in> {x \<in> Pow(I). Finite(x)}}"
abbreviation
Supset :: "i \<Rightarrow> i \<Rightarrow> o" (infixl \<open>\<supseteq>\<close> 50) where
"f \<supseteq> g \<equiv> g \<subseteq> f"
lemma FnI[intro]:
assumes "p : d \<rightarrow> J" "d \<subseteq> I" "Finite(d)"
shows "p \<in> Fn(I,J)"
using assms unfolding Fn_def by auto
lemma FnD[dest]:
assumes "p \<in> Fn(I,J)"
shows "\<exists>d. p : d \<rightarrow> J \<and> d \<subseteq> I \<and> Finite(d)"
using assms unfolding Fn_def by auto
lemma Fn_is_function: "p \<in> Fn(I,J) \<Longrightarrow> function(p)"
unfolding Fn_def using fun_is_function by auto
lemma restrict_eq_imp_compat:
assumes "f \<in> Fn(I, J)" "g \<in> Fn(I, J)"
"restrict(f, domain(f) \<inter> domain(g)) = restrict(g, domain(f) \<inter> domain(g))"
shows "f \<union> g \<in> Fn(I, J)"
proof -
from assms
obtain d1 d2 where "f : d1 \<rightarrow> J" "d1 \<in> Pow(I)" "Finite(d1)"
"g : d2 \<rightarrow> J" "d2 \<in> Pow(I)" "Finite(d2)"
by blast
with assms
show ?thesis
using domain_of_fun
restrict_eq_imp_Un_into_Pi[of f d1 "\<lambda>_. J" g d2 "\<lambda>_. J"]
by auto
qed
text\<open>We finally arrive to our application of DSL.\<close>
lemma ccc_Fn_nat: "ccc(Fn(I,2), (\<supseteq>))"
proof -
{
fix A
assume "\<not> countable(A)"
assume "A \<subseteq> Fn(I, 2)"
moreover from this
have "countable({p\<in>A. domain(p) = d})" for d
proof (cases "Finite(d) \<and> d \<subseteq> I")
case True
with \<open>A \<subseteq> Fn(I, 2)\<close>
have "{p \<in> A . domain(p) = d} \<subseteq> d \<rightarrow> 2"
using domain_of_fun by fastforce
moreover from True
have "Finite(d \<rightarrow> 2)"
using Finite_Pi lesspoll_nat_is_Finite by auto
ultimately
show ?thesis using subset_Finite[of _ "d\<rightarrow>2" ] Finite_imp_countable
by auto
next
case False
with \<open>A \<subseteq> Fn(I, 2)\<close>
have "{p \<in> A . domain(p) = d} = 0"
by (intro equalityI) (auto dest!: domain_of_fun)
then
show ?thesis using empty_lepollI by auto
qed
moreover
have "uncountable({domain(p) . p \<in> A})"
proof
from \<open>A \<subseteq> Fn(I, 2)\<close>
have "A = (\<Union>d\<in>{domain(p) . p \<in> A}. {p\<in>A. domain(p) = d})"
by auto
moreover
assume "countable({domain(p) . p \<in> A})"
moreover
note \<open>\<And>d. countable({p\<in>A. domain(p) = d})\<close> \<open>\<not>countable(A)\<close>
ultimately
show "False"
using countable_imp_countable_UN[of "{domain(p). p\<in>A}"
"\<lambda>d. {p \<in> A. domain(p) = d }"]
by auto
qed
moreover from \<open>A \<subseteq> Fn(I, 2)\<close>
have "p \<in> A \<Longrightarrow> Finite(domain(p))" for p
using lesspoll_nat_is_Finite[of "domain(p)"]
domain_of_fun[of p _ "\<lambda>_. 2"] by auto
ultimately
obtain D where "delta_system(D)" "D \<subseteq> {domain(p) . p \<in> A}" "D \<approx> \<aleph>\<^bsub>1\<^esub>"
using delta_system_uncountable[of "{domain(p) . p \<in> A}"] by auto
then
have delta:"\<forall>d1\<in>D. \<forall>d2\<in>D. d1 \<noteq> d2 \<longrightarrow> d1 \<inter> d2 = \<Inter>D"
using delta_system_root_eq_Inter
by simp
moreover from \<open>D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
have "uncountable(D)"
using uncountable_iff_subset_eqpoll_Aleph1 by auto
moreover from this and \<open>D \<subseteq> {domain(p) . p \<in> A}\<close>
obtain p1 where "p1 \<in> A" "domain(p1) \<in> D"
using uncountable_not_empty[of D] by blast
moreover from this and \<open>p1 \<in> A \<Longrightarrow> Finite(domain(p1))\<close>
have "Finite(domain(p1))" using Finite_domain by simp
moreover
define r where "r \<equiv> \<Inter>D"
ultimately
have "Finite(r)" using subset_Finite[of "r" "domain(p1)"] by auto
have "countable({restrict(p,r) . p\<in>A})"
proof -
have "f \<in> Fn(I, 2) \<Longrightarrow> restrict(f,r) \<in> Pow(r \<times> 2)" for f
using restrict_subset_Sigma[of f _ "\<lambda>_. 2" r]
by (auto dest!:FnD simp: Pi_def) auto
with \<open>A \<subseteq> Fn(I, 2)\<close>
have "{restrict(f,r) . f \<in> A } \<subseteq> Pow(r \<times> 2)"
by fast
with \<open>Finite(r)\<close>
show ?thesis
using Finite_Sigma[THEN Finite_Pow, of r "\<lambda>_. 2"]
by (intro Finite_imp_countable) (auto intro:subset_Finite)
qed
moreover
have "uncountable({p\<in>A. domain(p) \<in> D})" (is "uncountable(?X)")
proof
from \<open>D \<subseteq> {domain(p) . p \<in> A}\<close>
have "(\<lambda>p\<in>?X. domain(p)) \<in> surj(?X, D)"
using lam_type unfolding surj_def by auto
moreover
assume "countable(?X)"
moreover
note \<open>uncountable(D)\<close>
ultimately
show False
using surj_countable by auto
qed
moreover
have "D = (\<Union>f\<in>Pow(r\<times>2) . {domain(p) . p\<in>{ x\<in>A. restrict(x,r) = f \<and> domain(x) \<in> D}})"
proof -
{
fix z
assume "z \<in> D"
with \<open>D \<subseteq> _\<close>
obtain p where "domain(p) = z" "p \<in> A"
by auto
moreover from \<open>A \<subseteq> Fn(I, 2)\<close> and this
have "p : z \<rightarrow> 2"
using domain_of_fun by (auto dest!:FnD)
moreover from this
have "restrict(p,r) \<subseteq> r \<times> 2"
using function_restrictI[of p r] fun_is_function[of p z "\<lambda>_. 2"]
restrict_subset_Sigma[of p z "\<lambda>_. 2" r]
by (auto simp:Pi_def)
ultimately
have "\<exists>p\<in>A. restrict(p,r) \<in> Pow(r\<times>2) \<and> domain(p) = z" by auto
}
then
show ?thesis
by (intro equalityI) (force)+
qed
obtain f where "uncountable({domain(p) . p\<in>{x\<in>A. restrict(x,r) = f \<and> domain(x) \<in> D}})"
(is "uncountable(?Y(f))")
proof -
{
from \<open>Finite(r)\<close>
have "countable(Pow(r\<times>2))"
using Finite_Sigma[THEN Finite_Pow, THEN Finite_imp_countable]
by simp
moreover
assume "countable(?Y(f))" for f
moreover
note \<open>D = (\<Union>f\<in>Pow(r\<times>2) .?Y(f))\<close>
moreover
note \<open>uncountable(D)\<close>
ultimately
have "False"
using countable_imp_countable_UN[of "Pow(r\<times>2)" ?Y] by auto
}
with that
show ?thesis by auto
qed
then
obtain j where "j \<in> inj(nat, ?Y(f))"
using uncountable_iff_nat_lt_cardinal[THEN iffD1, THEN leI,
THEN cardinal_le_imp_lepoll, THEN lepollD]
by auto
then
have "j`0 \<noteq> j`1" "j`0 \<in> ?Y(f)" "j`1 \<in> ?Y(f)"
using inj_is_fun[THEN apply_type, of j nat "?Y(f)"]
unfolding inj_def by auto
then
obtain p q where "domain(p) \<noteq> domain(q)" "p \<in> A" "q \<in> A"
"domain(p) \<in> D" "domain(q) \<in> D"
"restrict(p,r) = restrict(q,r)" by auto
moreover from this and delta
have "domain(p) \<inter> domain(q) = r" unfolding r_def by simp
moreover
note \<open>A \<subseteq> Fn(I, 2)\<close>
moreover from calculation
have "p \<union> q \<in> Fn(I, 2)"
by (rule_tac restrict_eq_imp_compat) auto
ultimately
have "\<exists>p\<in>A. \<exists>q\<in>A. p \<noteq> q \<and> compat_in(Fn(I, 2), (\<supseteq>), p, q)"
unfolding compat_in_def
by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
}
then
show ?thesis unfolding ccc_def antichain_def by auto
qed
text\<open>The fact that a poset $P$ has the ccc has useful consequences for the
theory of forcing, since it implies that cardinals from the original
model are exactly the cardinals in any generic extension by $P$
\cite[Chap.~IV]{kunen2011set}.\<close>
end
\ No newline at end of file
section\<open>The Delta System Lemma\label{sec:dsl}\<close>
theory Delta_System
imports
Cardinal_Library
begin
text\<open>A \<^emph>\<open>delta system\<close> is family of sets with a common pairwise
intersection.\<close>
definition
delta_system :: "i \<Rightarrow> o" where
"delta_system(D) \<equiv> \<exists>r. \<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
lemma delta_systemI[intro]:
assumes "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
shows "delta_system(D)"
using assms unfolding delta_system_def by simp
lemma delta_systemD[dest]:
"delta_system(D) \<Longrightarrow> \<exists>r. \<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
unfolding delta_system_def by simp
text\<open>Hence, pairwise intersections equal the intersection of the whole
family.\<close>
lemma delta_system_root_eq_Inter:
assumes "delta_system(D)"
shows "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = \<Inter>D"
proof (clarify, intro equalityI, auto)
fix A' B' x C
assume hyp:"A'\<in>D" "B'\<in> D" "A'\<noteq>B'" "x\<in>A'" "x\<in>B'" "C\<in>D"
with assms
obtain r where delta:"\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
by auto
show "x \<in> C"
proof (cases "C=A'")
case True
with hyp and assms
show ?thesis by simp
next
case False
moreover
note hyp
moreover from calculation and delta
have "r = C \<inter> A'" "A' \<inter> B' = r" "x\<in>r" by auto
ultimately
show ?thesis by simp
qed
qed
text\<open>The \<^emph>\<open>Delta System Lemma\<close> (DSL) states that any uncountable family of
finite sets includes an uncountable delta system. This is the simplest
non trivial version; others, for cardinals greater than \<^term>\<open>\<aleph>\<^bsub>1\<^esub>\<close> assume
some weak versions of the generalized continuum hypothesis for the
cardinals involved.
The proof is essentially the one in \cite[III.2.6]{kunen2011set} for the
case \<^term>\<open>\<aleph>\<^bsub>1\<^esub>\<close>; another similar presentation can be found in
\cite[Chap.~16]{JW}.\<close>
lemma delta_system_Aleph1:
assumes "\<forall>A\<in>F. Finite(A)" "F \<approx> \<aleph>\<^bsub>1\<^esub>"
shows "\<exists>D. D \<subseteq> F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
proof -
text\<open>Since all members are finite,\<close>
from \<open>\<forall>A\<in>F. Finite(A)\<close>
have "(\<lambda>A\<in>F. |A|) : F \<rightarrow> \<omega>" (is "?cards : _")
by (rule_tac lam_type) simp
moreover from this
have a:"?cards -`` {n} = { A\<in>F . |A| = n }" for n
using vimage_lam by auto
moreover
note \<open>F \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
moreover from calculation
text\<open>there are uncountably many have the same cardinal:\<close>
obtain n where "n\<in>\<omega>" "|?cards -`` {n}| = \<aleph>\<^bsub>1\<^esub>"
using eqpoll_Aleph1_cardinal_vimage[of F ?cards] by auto
moreover
define G where "G \<equiv> ?cards -`` {n}"
moreover from calculation
have "G \<subseteq> F" by auto
ultimately
text\<open>Therefore, without loss of generality, we can assume that all
elements of the family have cardinality \<^term>\<open>n\<in>\<omega>\<close>.\<close>
have "A\<in>G \<Longrightarrow> |A| = n" and "G \<approx> \<aleph>\<^bsub>1\<^esub>" for A
using cardinal_Card_eqpoll_iff by auto
with \<open>n\<in>\<omega>\<close>
text\<open>So we prove the result by induction on this \<^term>\<open>n\<close> and
generalizing \<^term>\<open>G\<close>, since the argument requires changing the
family in order to apply the inductive hypothesis.\<close>
have "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
proof (induct arbitrary:G)
case 0 \<comment> \<open>This case is impossible\<close>
then
have "G \<subseteq> {0}"
using cardinal_0_iff_0 by auto
with \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
show ?case
using nat_lt_Aleph1 subset_imp_le_cardinal[of G "{0}"]
lt_trans2 cardinal_Card_eqpoll_iff by auto
next
case (succ n)
then
have "\<forall>a\<in>G. Finite(a)"
using Finite_cardinal_iff' nat_into_Finite[of "succ(n)"]
by fastforce
show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
proof (cases "\<exists>p. {A\<in>G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>")
case True \<comment> \<open>the positive case, uncountably many sets with a
common element\<close>
then
obtain p where "{A\<in>G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>" by blast
moreover from this
have "{A-{p} . A\<in>{X\<in>G. p\<in>X}} \<approx> \<aleph>\<^bsub>1\<^esub>" (is "?F \<approx> _")
using Diff_bij[of "{A\<in>G . p \<in> A}" "{p}"]
comp_bij[OF bij_converse_bij, where C="\<aleph>\<^bsub>1\<^esub>"] by fast
text\<open>Now using the hypothesis of the successor case,\<close>
moreover from \<open>\<And>A. A\<in>G \<Longrightarrow> |A|=succ(n)\<close> \<open>\<forall>a\<in>G. Finite(a)\<close>
and this
have "p\<in>A \<Longrightarrow> A\<in>G \<Longrightarrow> |A - {p}| = n" for A
using Finite_imp_succ_cardinal_Diff[of _ p] by force
moreover from this and \<open>n\<in>\<omega>\<close>
have "\<forall>a\<in>?F. Finite(a)"
using Finite_cardinal_iff' nat_into_Finite by auto
moreover
text\<open>we may apply the inductive hypothesis to the new family \<^term>\<open>?F\<close>:\<close>
note \<open>(\<And>A. A \<in> ?F \<Longrightarrow> |A| = n) \<Longrightarrow> ?F \<approx> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow>
\<exists>D. D \<subseteq> ?F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
ultimately
obtain D where "D\<subseteq>{A-{p} . A\<in>{X\<in>G. p\<in>X}}" "delta_system(D)" "D \<approx> \<aleph>\<^bsub>1\<^esub>"
by auto
moreover from this
obtain r where "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
by fastforce
then
have "\<forall>A\<in>D.\<forall>B\<in>D. A\<union>{p} \<noteq> B\<union>{p}\<longrightarrow>(A \<union> {p}) \<inter> (B \<union> {p}) = r\<union>{p}"
by blast
ultimately
have "delta_system({B \<union> {p} . B\<in>D})" (is "delta_system(?D)")
by fastforce
moreover from \<open>D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
have "|D| = \<aleph>\<^bsub>1\<^esub>" "Infinite(D)"
using cardinal_eqpoll_iff
by (auto intro!: uncountable_iff_subset_eqpoll_Aleph1[THEN iffD2]
uncountable_imp_Infinite) force
moreover from this
have "?D \<approx> \<aleph>\<^bsub>1\<^esub>"
using cardinal_map_Un[of D "{p}"] naturals_lt_nat
cardinal_eqpoll_iff[THEN iffD1] by simp
moreover
note \<open>D \<subseteq> {A-{p} . A\<in>{X\<in>G. p\<in>X}}\<close>
have "?D \<subseteq> G"
proof -
{
fix A
assume "A\<in>G" "p\<in>A"
moreover from this
have "A = A - {p} \<union> {p}"
by blast
ultimately
have "A -{p} \<union> {p} \<in> G"
by auto
}
with \<open>D \<subseteq> {A-{p} . A\<in>{X\<in>G. p\<in>X}}\<close>
show ?thesis
by blast
qed
ultimately
show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>" by auto
next
case False
note \<open>\<not> (\<exists>p. {A \<in> G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>)\<close> \<comment> \<open>the other case\<close>
moreover from \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
have "{A \<in> G . p \<in> A} \<lesssim> \<aleph>\<^bsub>1\<^esub>" (is "?G(p) \<lesssim> _") for p
by (blast intro:lepoll_eq_trans[OF subset_imp_lepoll])
ultimately
have "?G(p) \<prec> \<aleph>\<^bsub>1\<^esub>" for p
unfolding lesspoll_def by simp
then (* may omit the previous step if unfolding here: *)
have "?G(p) \<lesssim> \<omega>" for p
using lesspoll_aleph_plus_one[of 0] Aleph_zero_eq_nat by auto
moreover
have "{A \<in> G . S \<inter> A \<noteq> 0} = (\<Union>p\<in>S. ?G(p))" for S
by auto
ultimately
have "countable(S) \<Longrightarrow> countable({A \<in> G . S \<inter> A \<noteq> 0})" for S
using InfCard_nat Card_nat
le_Card_iff[THEN iffD2, THEN [3] leqpoll_imp_cardinal_UN_le,
THEN [2] le_Card_iff[THEN iffD1], of \<omega> S]
unfolding countable_def by simp
text\<open>For every countable subfamily of \<^term>\<open>G\<close> there is another some
element disjoint from all of them:\<close>
have "\<exists>A\<in>G. \<forall>S\<in>X. S \<inter> A = 0" if "|X| < \<aleph>\<^bsub>1\<^esub>" "X \<subseteq> G" for X
proof -
from \<open>n\<in>\<omega>\<close> \<open>\<And>A. A\<in>G \<Longrightarrow> |A| = succ(n)\<close>
have "A\<in>G \<Longrightarrow> Finite(A)" for A
using cardinal_Card_eqpoll_iff
unfolding Finite_def by fastforce
with \<open>X\<subseteq>G\<close>
have "A\<in>X \<Longrightarrow> countable(A)" for A
using Finite_imp_countable by auto
with \<open>|X| < \<aleph>\<^bsub>1\<^esub>\<close>
have "countable(\<Union>X)"
using Card_nat[THEN cardinal_lt_csucc_iff, of X]
countable_union_countable countable_iff_cardinal_le_nat
unfolding Aleph_def by simp
with \<open>countable(_) \<Longrightarrow> countable({A \<in> G . _ \<inter> A \<noteq> 0})\<close>
have "countable({A \<in> G . (\<Union>X) \<inter> A \<noteq> 0})" .
with \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
obtain B where "B\<in>G" "B \<notin> {A \<in> G . (\<Union>X) \<inter> A \<noteq> 0}"
using nat_lt_Aleph1 cardinal_Card_eqpoll_iff[of "\<aleph>\<^bsub>1\<^esub>" G]
uncountable_not_subset_countable[of "{A \<in> G . (\<Union>X) \<inter> A \<noteq> 0}" G]
uncountable_iff_nat_lt_cardinal
by auto
then
show "\<exists>A\<in>G. \<forall>S\<in>X. S \<inter> A = 0" by auto
qed
moreover from \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
obtain b where "b\<in>G"
using uncountable_iff_subset_eqpoll_Aleph1
uncountable_not_empty by blast
ultimately
text\<open>Hence, the hypotheses to perform a bounded-cardinal selection
are satisfied,\<close>
obtain S where "S:\<aleph>\<^bsub>1\<^esub>\<rightarrow>G" "\<alpha>\<in>\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<beta>\<in>\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<alpha><\<beta> \<Longrightarrow> S`\<alpha> \<inter> S`\<beta> = 0"
for \<alpha> \<beta>
using bounded_cardinal_selection[of "\<aleph>\<^bsub>1\<^esub>" G "\<lambda>s a. s \<inter> a = 0" b]
by force
then
have "\<alpha> \<in> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<beta> \<in> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<alpha>\<noteq>\<beta> \<Longrightarrow> S`\<alpha> \<inter> S`\<beta> = 0" for \<alpha> \<beta>
using lt_neq_symmetry[of "\<aleph>\<^bsub>1\<^esub>" "\<lambda>\<alpha> \<beta>. S`\<alpha> \<inter> S`\<beta> = 0"] Card_is_Ord
by auto blast
text\<open>and a symmetry argument shows that obtained \<^term>\<open>S\<close> is
an injective \<^term>\<open>\<aleph>\<^bsub>1\<^esub>\<close>-sequence of disjoint elements of \<^term>\<open>G\<close>.\<close>
moreover from this and \<open>\<And>A. A\<in>G \<Longrightarrow> |A| = succ(n)\<close> \<open>S : \<aleph>\<^bsub>1\<^esub> \<rightarrow> G\<close>
have "S \<in> inj(\<aleph>\<^bsub>1\<^esub>, G)"
using cardinal_succ_not_0 Int_eq_zero_imp_not_eq[of "\<aleph>\<^bsub>1\<^esub>" "\<lambda>x. S`x"]
unfolding inj_def by fastforce
moreover from calculation
have "range(S) \<approx> \<aleph>\<^bsub>1\<^esub>"
using inj_bij_range eqpoll_sym unfolding eqpoll_def by fast
moreover from calculation
have "range(S) \<subseteq> G"
using inj_is_fun range_fun_subset_codomain by fast
ultimately
show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
using inj_is_fun range_eq_image[of S "\<aleph>\<^bsub>1\<^esub>" G]
image_function[OF fun_is_function, OF inj_is_fun, of S "\<aleph>\<^bsub>1\<^esub>" G]
domain_of_fun[OF inj_is_fun, of S "\<aleph>\<^bsub>1\<^esub>" G]
by (rule_tac x="S``\<aleph>\<^bsub>1\<^esub>" in exI) auto
text\<open>This finishes the successor case and hence the proof.\<close>
qed
qed
with \<open>G \<subseteq> F\<close>
show ?thesis by blast
qed
lemma delta_system_uncountable:
assumes "\<forall>A\<in>F. Finite(A)" "uncountable(F)"
shows "\<exists>D. D \<subseteq> F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
proof -
from assms
obtain S where "S \<subseteq> F" "S \<approx> \<aleph>\<^bsub>1\<^esub>"
using uncountable_iff_subset_eqpoll_Aleph1[of F] by auto
moreover from \<open>\<forall>A\<in>F. Finite(A)\<close> and this
have "\<forall>A\<in>S. Finite(A)" by auto
ultimately
show ?thesis using delta_system_Aleph1[of S]
by auto
qed
end
\ No newline at end of file
theory Konig
imports
Cofinality
Cardinal_Library
begin
text\<open>Now, using the Axiom of choice, we can show that all successor
cardinals are regular.\<close>
lemma cf_csucc:
assumes "InfCard(z)"
shows "cf(z\<^sup>+) = z\<^sup>+"
proof (rule ccontr)
assume "cf(z\<^sup>+) \<noteq> z\<^sup>+"
moreover from \<open>InfCard(z)\<close>
have "Ord(z\<^sup>+)" "Ord(z)" "Limit(z)" "Limit(z\<^sup>+)" "Card(z\<^sup>+)" "Card(z)"
using InfCard_csucc Card_is_Ord InfCard_is_Card InfCard_is_Limit
by fastforce+
moreover from calculation
have "cf(z\<^sup>+) < z\<^sup>+"
using cf_le_cardinal[of "z\<^sup>+", THEN le_iff[THEN iffD1]]
Card_cardinal_eq
by simp
ultimately
obtain G where "G:cf(z\<^sup>+)\<rightarrow> z\<^sup>+" "\<forall>\<beta>\<in>z\<^sup>+. \<exists>y\<in>cf(z\<^sup>+). \<beta> < G`y"
using Limit_cofinal_fun_lt[of "z\<^sup>+" _ "cf(z\<^sup>+)"] Ord_cf
cf_le_cf_fun[of "z\<^sup>+" "cf(z\<^sup>+)"] le_refl[of "cf(z\<^sup>+)"]
by auto
with \<open>Card(z)\<close> \<open>Card(z\<^sup>+)\<close> \<open>Ord(z\<^sup>+)\<close>
have "\<forall>\<beta>\<in>cf(z\<^sup>+). |G`\<beta>| \<le> z"
using apply_type[of G "cf(z\<^sup>+)" "\<lambda>_. z\<^sup>+", THEN ltI] Card_lt_iff[THEN iffD2]
Ord_in_Ord[OF Card_is_Ord, of "z\<^sup>+"] cardinal_lt_csucc_iff[THEN iffD1]
by auto
from \<open>cf(z\<^sup>+) < z\<^sup>+\<close> \<open>InfCard(z)\<close> \<open>Ord(z)\<close>
have "cf(z\<^sup>+) \<lesssim> z"
using cardinal_lt_csucc_iff[of "z" "cf(z\<^sup>+)"] Card_csucc[of "z"]
le_Card_iff[of "z" "cf(z\<^sup>+)"] InfCard_is_Card
Card_lt_iff[of "cf(z\<^sup>+)" "z\<^sup>+"] lt_Ord[of "cf(z\<^sup>+)" "z\<^sup>+"]
by simp
with \<open>cf(z\<^sup>+) < z\<^sup>+\<close> \<open>\<forall>\<beta>\<in>cf(z\<^sup>+). |G`\<beta>| \<le> _\<close> \<open>InfCard(z)\<close>
have "|\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>| \<le> z"
using InfCard_csucc[of z]
subset_imp_lepoll[THEN lepoll_imp_Card_le, of "\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>" "z"]
by (rule_tac leqpoll_imp_cardinal_UN_le) auto
moreover
note \<open>Ord(z)\<close>
moreover from \<open>\<forall>\<beta>\<in>z\<^sup>+. \<exists>y\<in>cf(z\<^sup>+). \<beta> < G`y\<close> and this
have "z\<^sup>+ \<subseteq> (\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>)"
by (blast dest:ltD)
ultimately
have "z\<^sup>+ \<le> z"
using subset_imp_le_cardinal[of "z\<^sup>+" "\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>"] le_trans
InfCard_is_Card Card_csucc[of z] Card_cardinal_eq
by auto
with \<open>Ord(z)\<close>
show "False"
using lt_csucc[of z] not_lt_iff_le[THEN iffD2, of z "z\<^sup>+"]
Card_csucc[THEN Card_is_Ord]
by auto
qed
text\<open>And this finishes the calculation of cofinality of Alephs.\<close>
lemma cf_Aleph_succ: "Ord(z) \<Longrightarrow> cf(\<aleph>\<^bsub>succ(z)\<^esub>) = \<aleph>\<^bsub>succ(z)\<^esub>"
using Aleph_succ cf_csucc InfCard_Aleph by simp
subsection\<open>König's Theorem\label{sec:konig}\<close>
text\<open>We end this section by proving König's Theorem on the cofinality
of cardinal exponentiation. This is a strengthening of Cantor's theorem
and it is essentially the only basic way to prove strict cardinal
inequalities.
It is proved rather straightforwardly with the tools already developed.\<close>
lemma konigs_theorem:
notes [dest] = InfCard_is_Card Card_is_Ord
and [trans] = lt_trans1 lt_trans2
assumes
"InfCard(\<kappa>)" "InfCard(\<nu>)" "cf(\<kappa>) \<le> \<nu>"
shows
"\<kappa> < \<kappa>\<^bsup>\<up>\<nu>\<^esup>"