Theory Delta_System
section‹The Delta System Lemma\label{sec:dsl}›
theory Delta_System
imports
Cardinal_Library
begin
text‹The ∗‹Delta System Lemma› (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>‹ℵ⇘1⇙› assume
some weak versions of the generalized continuum hypothesis for the
cardinals involved.
The proof is essentially the one in \<^cite>‹‹III.2.6› in "kunen2011set"› for the
case \<^term>‹ℵ⇘1⇙›; another similar presentation can be found in
\<^cite>‹‹Chap.~16› in "JW"›.›
lemma delta_system_Aleph1:
assumes "∀A∈F. Finite(A)" "F ≈ ℵ⇘1⇙"
shows "∃D. D ⊆ F ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙"
proof -
text‹Since all members are finite,›
from ‹∀A∈F. Finite(A)›
have "(λA∈F. |A|) : F → ω" (is "?cards : _")
by (rule_tac lam_type) simp
moreover from this
have a:"?cards -`` {n} = { A∈F . |A| = n }" for n
using vimage_lam by auto
moreover
note ‹F ≈ ℵ⇘1⇙›
moreover from calculation
text‹there are uncountably many have the same cardinal:›
obtain n where "n∈ω" "|?cards -`` {n}| = ℵ⇘1⇙"
using eqpoll_Aleph1_cardinal_vimage[of F ?cards] by auto
moreover
define G where "G ≡ ?cards -`` {n}"
moreover from calculation
have "G ⊆ F" by auto
ultimately
text‹Therefore, without loss of generality, we can assume that all
elements of the family have cardinality \<^term>‹n∈ω›.›
have "A∈G ⟹ |A| = n" and "G ≈ ℵ⇘1⇙" for A
using cardinal_Card_eqpoll_iff by auto
with ‹n∈ω›
text‹So we prove the result by induction on this \<^term>‹n› and
generalizing \<^term>‹G›, since the argument requires changing the
family in order to apply the inductive hypothesis.›
have "∃D. D ⊆ G ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙"
proof (induct arbitrary:G)
case 0
then
have "G ⊆ {0}"
using cardinal_0_iff_0 by auto
with ‹G ≈ ℵ⇘1⇙›
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 "∀a∈G. Finite(a)"
using Finite_cardinal_iff' nat_into_Finite[of "succ(n)"]
by fastforce
show "∃D. D ⊆ G ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙"
proof (cases "∃p. {A∈G . p ∈ A} ≈ ℵ⇘1⇙")
case True
then
obtain p where "{A∈G . p ∈ A} ≈ ℵ⇘1⇙" by blast
moreover from this
have "{A-{p} . A∈{X∈G. p∈X}} ≈ ℵ⇘1⇙" (is "?F ≈ _")
using Diff_bij[of "{A∈G . p ∈ A}" "{p}"]
comp_bij[OF bij_converse_bij, where C="ℵ⇘1⇙"] by fast
text‹Now using the hypothesis of the successor case,›
moreover from ‹⋀A. A∈G ⟹ |A|=succ(n)› ‹∀a∈G. Finite(a)›
and this
have "p∈A ⟹ A∈G ⟹ |A - {p}| = n" for A
using Finite_imp_succ_cardinal_Diff[of _ p] by force
moreover from this and ‹n∈ω›
have "∀a∈?F. Finite(a)"
using Finite_cardinal_iff' nat_into_Finite by auto
moreover
text‹we may apply the inductive hypothesis to the new family \<^term>‹?F›:›
note ‹(⋀A. A ∈ ?F ⟹ |A| = n) ⟹ ?F ≈ ℵ⇘1⇙ ⟹
∃D. D ⊆ ?F ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙›
ultimately
obtain D where "D⊆{A-{p} . A∈{X∈G. p∈X}}" "delta_system(D)" "D ≈ ℵ⇘1⇙"
by auto
moreover from this
obtain r where "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
by fastforce
then
have "∀A∈D.∀B∈D. A∪{p} ≠ B∪{p}⟶(A ∪ {p}) ∩ (B ∪ {p}) = r∪{p}"
by blast
ultimately
have "delta_system({B ∪ {p} . B∈D})" (is "delta_system(?D)")
by fastforce
moreover from ‹D ≈ ℵ⇘1⇙›
have "|D| = ℵ⇘1⇙" "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 ≈ ℵ⇘1⇙"
using cardinal_map_Un[of D "{p}"] naturals_lt_nat
cardinal_eqpoll_iff[THEN iffD1] by simp
moreover
note ‹D ⊆ {A-{p} . A∈{X∈G. p∈X}}›
have "?D ⊆ G"
proof -
{
fix A
assume "A∈G" "p∈A"
moreover from this
have "A = A - {p} ∪ {p}"
by blast
ultimately
have "A -{p} ∪ {p} ∈ G"
by auto
}
with ‹D ⊆ {A-{p} . A∈{X∈G. p∈X}}›
show ?thesis
by blast
qed
ultimately
show "∃D. D ⊆ G ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙" by auto
next
case False
note ‹¬ (∃p. {A ∈ G . p ∈ A} ≈ ℵ⇘1⇙)›
moreover from ‹G ≈ ℵ⇘1⇙›
have "{A ∈ G . p ∈ A} ≲ ℵ⇘1⇙" (is "?G(p) ≲ _") for p
by (blast intro:lepoll_eq_trans[OF subset_imp_lepoll])
ultimately
have "?G(p) ≺ ℵ⇘1⇙" for p
unfolding lesspoll_def by simp
then
have "?G(p) ≲ ω" for p
using lesspoll_aleph_plus_one[of 0] Aleph_zero_eq_nat by auto
moreover
have "{A ∈ G . S ∩ A ≠ 0} = (⋃p∈S. ?G(p))" for S
by auto
ultimately
have "countable(S) ⟹ countable({A ∈ G . S ∩ A ≠ 0})" for S
using InfCard_nat Card_nat
le_Card_iff[THEN iffD2, THEN [3] lepoll_imp_cardinal_UN_le,
THEN [2] le_Card_iff[THEN iffD1], of ω S]
unfolding countable_def by simp
text‹For every countable subfamily of \<^term>‹G› there is another some
element disjoint from all of them:›
have "∃A∈G. ∀S∈X. S ∩ A = 0" if "|X| < ℵ⇘1⇙" "X ⊆ G" for X
proof -
from ‹n∈ω› ‹⋀A. A∈G ⟹ |A| = succ(n)›
have "A∈G ⟹ Finite(A)" for A
using cardinal_Card_eqpoll_iff
unfolding Finite_def by fastforce
with ‹X⊆G›
have "A∈X ⟹ countable(A)" for A
using Finite_imp_countable by auto
with ‹|X| < ℵ⇘1⇙›
have "countable(⋃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 ‹countable(_) ⟹ countable({A ∈ G . _ ∩ A ≠ 0})›
have "countable({A ∈ G . (⋃X) ∩ A ≠ 0})" .
with ‹G ≈ ℵ⇘1⇙›
obtain B where "B∈G" "B ∉ {A ∈ G . (⋃X) ∩ A ≠ 0}"
using nat_lt_Aleph1 cardinal_Card_eqpoll_iff[of "ℵ⇘1⇙" G]
uncountable_not_subset_countable[of "{A ∈ G . (⋃X) ∩ A ≠ 0}" G]
uncountable_iff_nat_lt_cardinal
by auto
then
show "∃A∈G. ∀S∈X. S ∩ A = 0" by auto
qed
moreover from ‹G ≈ ℵ⇘1⇙›
obtain b where "b∈G"
using uncountable_iff_subset_eqpoll_Aleph1
uncountable_not_empty by blast
ultimately
text‹Hence, the hypotheses to perform a bounded-cardinal selection
are satisfied,›
obtain S where "S:ℵ⇘1⇙→G" "α∈ℵ⇘1⇙ ⟹ β∈ℵ⇘1⇙ ⟹ α<β ⟹ S`α ∩ S`β = 0"
for α β
using bounded_cardinal_selection[of "ℵ⇘1⇙" G "λs a. s ∩ a = 0" b]
by force
then
have "α ∈ ℵ⇘1⇙ ⟹ β ∈ ℵ⇘1⇙ ⟹ α≠β ⟹ S`α ∩ S`β = 0" for α β
using lt_neq_symmetry[of "ℵ⇘1⇙" "λα β. S`α ∩ S`β = 0"] Card_is_Ord
by auto blast
text‹and a symmetry argument shows that obtained \<^term>‹S› is
an injective \<^term>‹ℵ⇘1⇙›-sequence of disjoint elements of \<^term>‹G›.›
moreover from this and ‹⋀A. A∈G ⟹ |A| = succ(n)› ‹S : ℵ⇘1⇙ → G›
have "S ∈ inj(ℵ⇘1⇙, G)"
using cardinal_succ_not_0 Int_eq_zero_imp_not_eq[of "ℵ⇘1⇙" "λx. S`x"]
unfolding inj_def by fastforce
moreover from calculation
have "range(S) ≈ ℵ⇘1⇙"
using inj_bij_range eqpoll_sym unfolding eqpoll_def by fast
moreover from calculation
have "range(S) ⊆ G"
using inj_is_fun range_fun_subset_codomain by fast
ultimately
show "∃D. D ⊆ G ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙"
using inj_is_fun range_eq_image[of S "ℵ⇘1⇙" G]
image_function[OF fun_is_function, OF inj_is_fun, of S "ℵ⇘1⇙" G]
domain_of_fun[OF inj_is_fun, of S "ℵ⇘1⇙" G]
by (rule_tac x="S``ℵ⇘1⇙" in exI) auto
text‹This finishes the successor case and hence the proof.›
qed
qed
with ‹G ⊆ F›
show ?thesis by blast
qed
lemma delta_system_uncountable:
assumes "∀A∈F. Finite(A)" "uncountable(F)"
shows "∃D. D ⊆ F ∧ delta_system(D) ∧ D ≈ ℵ⇘1⇙"
proof -
from assms
obtain S where "S ⊆ F" "S ≈ ℵ⇘1⇙"
using uncountable_iff_subset_eqpoll_Aleph1[of F] by auto
moreover from ‹∀A∈F. Finite(A)› and this
have "∀A∈S. Finite(A)" by auto
ultimately
show ?thesis using delta_system_Aleph1[of S]
by auto
qed
end