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 ― ‹This case is impossible› 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 ― ‹the positive case, uncountably many sets with a common element› 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⇙)› ― ‹the other case› 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 (* may omit the previous step if unfolding here: *) 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