section‹Cardinal Arithmetic under Choice\label{sec:cardinal-lib}› theory Cardinal_Library imports ZF_Library ZF.Cardinal_AC begin text‹This theory includes results on cardinalities that depend on $\AC$› subsection‹Results on cardinal exponentiation› text‹Non trivial instances of cardinal exponentiation require that the relevant function spaces are well-ordered, hence this implies a strong use of choice.› lemma cexp_eqpoll_cong: assumes "A ≈ A'" "B ≈ B'" shows "A⇗↑B⇖ = A'⇗↑B'⇖" unfolding cexp_def using cardinal_eqpoll_iff function_space_eqpoll_cong assms by simp lemma cexp_cexp_cmult: "(κ⇗↑ν1⇖)⇗↑ν2⇖ = κ⇗↑ν2 ⊗ ν1⇖" proof - have "(κ⇗↑ν1⇖)⇗↑ν2⇖ = (ν1 → κ)⇗↑ν2⇖" using cardinal_eqpoll by (intro cexp_eqpoll_cong) (simp_all add:cexp_def) also have " … = κ⇗↑ν2 × ν1⇖" unfolding cexp_def using curry_eqpoll cardinal_cong by blast also have " … = κ⇗↑ν2 ⊗ ν1⇖" using cardinal_eqpoll[THEN eqpoll_sym] unfolding cmult_def by (intro cexp_eqpoll_cong) (simp) finally show ?thesis . qed lemma cardinal_Pow: "|Pow(X)| = 2⇗↑X⇖" ― ‹Perhaps it's better with |X|› using cardinal_eqpoll_iff[THEN iffD2, OF Pow_eqpoll_function_space] unfolding cexp_def by simp lemma cantor_cexp: assumes "Card(ν)" shows "ν < 2⇗↑ν⇖" using assms Card_is_Ord Card_cexp proof (intro not_le_iff_lt[THEN iffD1] notI) assume "2⇗↑ν⇖ ≤ ν" then have "|Pow(ν)| ≤ ν" using cardinal_Pow by simp with assms have "Pow(ν) ≲ ν" using cardinal_eqpoll_iff Card_le_imp_lepoll Card_cardinal_eq by auto then obtain g where "g ∈ inj(Pow(ν), ν)" by blast then show "False" using cantor_inj by simp qed simp lemma cexp_left_mono: assumes "κ1 ≤ κ2" shows "κ1⇗↑ν⇖ ≤ κ2⇗↑ν⇖" (* ― ‹short, unreadable proof: › unfolding cexp_def using subset_imp_lepoll[THEN lepoll_imp_cardinal_le] assms le_subset_iff[THEN iffD1, OF assms] Pi_weaken_type[of _ _ "λ_. κ1" "λ_. κ2"] by auto *) proof - from assms have "κ1 ⊆ κ2" using le_subset_iff by simp then have "ν → κ1 ⊆ ν → κ2" using Pi_weaken_type by auto then show ?thesis unfolding cexp_def using lepoll_imp_cardinal_le subset_imp_lepoll by simp qed lemma cantor_cexp': assumes "2 ≤ κ" "Card(ν)" shows "ν < κ⇗↑ν⇖" using cexp_left_mono assms cantor_cexp lt_trans2 by blast lemma InfCard_cexp: assumes "2 ≤ κ" "InfCard(ν)" shows "InfCard(κ⇗↑ν⇖)" using assms cantor_cexp'[THEN leI] le_trans Card_cexp unfolding InfCard_def by auto lemmas InfCard_cexp' = InfCard_cexp[OF nats_le_InfCard, simplified] ― ‹\<^term>‹InfCard(κ) ⟹ InfCard(ν) ⟹ InfCard(κ⇗↑ν⇖)›› subsection‹Miscellaneous› lemma cardinal_RepFun_le: "|{f(a) . a∈A}| ≤ |A|" proof - have "(λx∈A. f(x)) ∈ surj(A, {f(a) . a∈A})" unfolding surj_def using lam_funtype by auto then show ?thesis using surj_implies_cardinal_le by blast qed lemma subset_imp_le_cardinal: "A ⊆ B ⟹ |A| ≤ |B|" using subset_imp_lepoll[THEN lepoll_imp_cardinal_le] . lemma lt_cardinal_imp_not_subset: "|A| < |B| ⟹ ¬ B ⊆ A" using subset_imp_le_cardinal le_imp_not_lt by blast lemma cardinal_lt_csucc_iff: "Card(K) ⟹ |K'| < K⇧^{+}⟷ |K'| ≤ K" by (simp add: Card_lt_csucc_iff) lemma cardinal_UN_le_nat: "(⋀i. i∈ω ⟹ |X(i)| ≤ ω) ⟹ |⋃i∈ω. X(i)| ≤ ω" by (simp add: cardinal_UN_le InfCard_nat) lemma lepoll_imp_cardinal_UN_le: notes [dest] = InfCard_is_Card Card_is_Ord assumes "InfCard(K)" "J ≲ K" "⋀i. i∈J ⟹ |X(i)| ≤ K" shows "|⋃i∈J. X(i)| ≤ K" proof - from ‹J ≲ K› obtain f where "f ∈ inj(J,K)" by blast define Y where "Y(k) ≡ if k∈range(f) then X(converse(f)`k) else 0" for k have "i∈J ⟹ f`i ∈ K" for i using inj_is_fun[OF ‹f ∈ inj(J,K)›] by auto have "(⋃i∈J. X(i)) ⊆ (⋃i∈K. Y(i))" proof (standard, elim UN_E) fix x i assume "i∈J" "x∈X(i)" with ‹f ∈ inj(J,K)› ‹i∈J ⟹ f`i ∈ K› have "x ∈ Y(f`i)" "f`i ∈ K" unfolding Y_def using inj_is_fun[OF ‹f ∈ inj(J,K)›] right_inverse apply_rangeI by auto then show "x ∈ (⋃i∈K. Y(i))" by auto qed then have "|⋃i∈J. X(i)| ≤ |⋃i∈K. Y(i)|" unfolding Y_def using subset_imp_le_cardinal by simp with assms ‹⋀i. i∈J ⟹ f`i ∈ K› show "|⋃i∈J. X(i)| ≤ K" using inj_converse_fun[OF ‹f ∈ inj(J,K)›] unfolding Y_def by (rule_tac le_trans[OF _ cardinal_UN_le]) (auto intro:Ord_0_le)+ qed ― ‹For backwards compatibility› lemmas leqpoll_imp_cardinal_UN_le = lepoll_imp_cardinal_UN_le lemma cardinal_lt_csucc_iff': includes Ord_dests assumes "Card(κ)" shows "κ < |X| ⟷ κ⇧^{+}≤ |X|" using assms cardinal_lt_csucc_iff[of κ X] Card_csucc[of κ] not_le_iff_lt[of "κ⇧^{+}" "|X|"] not_le_iff_lt[of "|X|" κ] by blast lemma lepoll_imp_subset_bij: "X ≲ Y ⟷ (∃Z. Z ⊆ Y ∧ Z ≈ X)" proof assume "X ≲ Y" then obtain j where "j ∈ inj(X,Y)" by blast then have "range(j) ⊆ Y" "j ∈ bij(X,range(j))" using inj_bij_range inj_is_fun range_fun_subset_codomain by blast+ then show "∃Z. Z ⊆ Y ∧ Z ≈ X" using eqpoll_sym unfolding eqpoll_def by force next assume "∃Z. Z ⊆ Y ∧ Z ≈ X" then obtain Z f where "f ∈ bij(Z,X)" "Z ⊆ Y" unfolding eqpoll_def by force then have "converse(f) ∈ inj(X,Y)" using bij_is_inj inj_weaken_type bij_converse_bij by blast then show "X ≲ Y" by blast qed text‹The following result proves to be very useful when combining \<^term>‹cardinal› and \<^term>‹eqpoll› in a calculation.› lemma cardinal_Card_eqpoll_iff: "Card(κ) ⟹ |X| = κ ⟷ X ≈ κ" using Card_cardinal_eq[of κ] cardinal_eqpoll_iff[of X κ] by auto ― ‹Compare @{thm [source] "le_Card_iff"}› lemma lepoll_imp_lepoll_cardinal: assumes "X ≲ Y" shows "X ≲ |Y|" using assms cardinal_Card_eqpoll_iff[of "|Y|" Y] lepoll_eq_trans[of _ _ "|Y|"] by simp lemma lepoll_Un: assumes "InfCard(κ)" "A ≲ κ" "B ≲ κ" shows "A ∪ B ≲ κ" proof - have "A ∪ B ≲ sum(A,B)" using Un_lepoll_sum . moreover note assms moreover from this have "|sum(A,B)| ≤ κ ⊕ κ" using sum_lepoll_mono[of A κ B κ] lepoll_imp_cardinal_le unfolding cadd_def by auto ultimately show ?thesis using InfCard_cdouble_eq Card_cardinal_eq InfCard_is_Card Card_le_imp_lepoll[of "sum(A,B)" κ] lepoll_trans[of "A∪B"] by auto qed lemma cardinal_Un_le: assumes "InfCard(κ)" "|A| ≤ κ" "|B| ≤ κ" shows "|A ∪ B| ≤ κ" using assms lepoll_Un le_Card_iff InfCard_is_Card by auto text‹This is the unconditional version under choice of @{thm [source] Cardinal.Finite_cardinal_iff}.› lemma Finite_cardinal_iff': "Finite(|i|) ⟷ Finite(i)" using cardinal_eqpoll_iff eqpoll_imp_Finite_iff by fastforce lemma cardinal_subset_of_Card: assumes "Card(γ)" "a ⊆ γ" shows "|a| < γ ∨ |a| = γ" proof - from assms have "|a| < |γ| ∨ |a| = |γ|" using subset_imp_le_cardinal le_iff by simp with assms show ?thesis using Card_cardinal_eq by simp qed lemma cardinal_cases: includes Ord_dests shows "Card(γ) ⟹ |X| < γ ⟷ ¬ |X| ≥ γ" using not_le_iff_lt by auto subsection‹Countable and uncountable sets› lemma countable_iff_cardinal_le_nat: "countable(X) ⟷ |X| ≤ ω" using le_Card_iff[of ω X] Card_nat unfolding countable_def by simp lemma lepoll_countable: "X ≲ Y ⟹ countable(Y) ⟹ countable(X)" using lepoll_trans[of X Y] by blast ― ‹Next lemma can be proved without using AC› lemma surj_countable: "countable(X) ⟹ f ∈ surj(X,Y) ⟹ countable(Y)" using surj_implies_cardinal_le[of f X Y, THEN le_trans] countable_iff_cardinal_le_nat by simp lemma Finite_imp_countable: "Finite(X) ⟹ countable(X)" unfolding Finite_def by (auto intro:InfCard_nat nats_le_InfCard[of _ ω, THEN le_imp_lepoll] dest!:eq_lepoll_trans[of X _ ω]) lemma countable_imp_countable_UN: assumes "countable(J)" "⋀i. i∈J ⟹ countable(X(i))" shows "countable(⋃i∈J. X(i))" using assms lepoll_imp_cardinal_UN_le[of ω J X] InfCard_nat countable_iff_cardinal_le_nat by auto lemma countable_union_countable: assumes "⋀x. x ∈ C ⟹ countable(x)" "countable(C)" shows "countable(⋃C)" using assms countable_imp_countable_UN[of C "λx. x"] by simp abbreviation uncountable :: "i⇒o" where "uncountable(X) ≡ ¬ countable(X)" lemma uncountable_iff_nat_lt_cardinal: "uncountable(X) ⟷ ω < |X|" using countable_iff_cardinal_le_nat not_le_iff_lt by simp lemma uncountable_not_empty: "uncountable(X) ⟹ X ≠ 0" using empty_lepollI by auto lemma uncountable_imp_Infinite: "uncountable(X) ⟹ Infinite(X)" using uncountable_iff_nat_lt_cardinal[of X] lepoll_nat_imp_Infinite[of X] cardinal_le_imp_lepoll[of ω X] leI by simp lemma uncountable_not_subset_countable: assumes "countable(X)" "uncountable(Y)" shows "¬ (Y ⊆ X)" using assms lepoll_trans subset_imp_lepoll[of Y X] by blast subsection‹Results on Alephs› lemma nat_lt_Aleph1: "ω < ℵ⇘1⇙" by (simp add: Aleph_def lt_csucc) lemma zero_lt_Aleph1: "0 < ℵ⇘1⇙" by (rule lt_trans[of _ "ω"], auto simp add: ltI nat_lt_Aleph1) lemma le_aleph1_nat: "Card(k) ⟹ k<ℵ⇘1⇙ ⟹ k ≤ ω" by (simp add: Aleph_def Card_lt_csucc_iff Card_nat) lemma Aleph_succ: "ℵ⇘succ(α)⇙ = ℵ⇘α⇙⇧^{+}" unfolding Aleph_def by simp lemma lesspoll_aleph_plus_one: assumes "Ord(α)" shows "d ≺ ℵ⇘succ(α)⇙ ⟷ d ≲ ℵ⇘α⇙" using assms lesspoll_csucc Aleph_succ Card_is_Ord by simp lemma cardinal_Aleph [simp]: "Ord(α) ⟹ |ℵ⇘α⇙| = ℵ⇘α⇙" using Card_cardinal_eq by simp ― ‹Could be proved without using AC› lemma Aleph_lesspoll_increasing: includes Aleph_intros shows "a < b ⟹ ℵ⇘a⇙ ≺ ℵ⇘b⇙" using cardinal_lt_iff_lesspoll[of "ℵ⇘a⇙" "ℵ⇘b⇙"] Card_cardinal_eq[of "ℵ⇘b⇙"] lt_Ord lt_Ord2 Card_Aleph[THEN Card_is_Ord] by auto lemma uncountable_iff_subset_eqpoll_Aleph1: includes Ord_dests notes Aleph_zero_eq_nat[simp] Card_nat[simp] Aleph_succ[simp] shows "uncountable(X) ⟷ (∃S. S ⊆ X ∧ S ≈ ℵ⇘1⇙)" proof assume "uncountable(X)" then have "ℵ⇘1⇙ ≲ X" using uncountable_iff_nat_lt_cardinal cardinal_lt_csucc_iff' cardinal_le_imp_lepoll by force then obtain S where "S ⊆ X" "S ≈ ℵ⇘1⇙" using lepoll_imp_subset_bij by auto then show "∃S. S ⊆ X ∧ S ≈ ℵ⇘1⇙" using cardinal_cong Card_csucc[of ω] Card_cardinal_eq by auto next assume "∃S. S ⊆ X ∧ S ≈ ℵ⇘1⇙" then have "ℵ⇘1⇙ ≲ X" using subset_imp_lepoll[THEN [2] eq_lepoll_trans, of "ℵ⇘1⇙" _ X, OF eqpoll_sym] by auto then show "uncountable(X)" using Aleph_lesspoll_increasing[of 0 1, THEN [2] lesspoll_trans1, of "ℵ⇘1⇙"] lepoll_trans[of "ℵ⇘1⇙" X ω] by auto qed lemma lt_Aleph_imp_cardinal_UN_le_nat: "function(G) ⟹ domain(G) ≲ ω ⟹ ∀n∈domain(G). |G`n|<ℵ⇘1⇙ ⟹ |⋃n∈domain(G). G`n|≤ω" proof - assume "function(G)" let ?N="domain(G)" and ?R="⋃n∈domain(G). G`n" assume "?N ≲ ω" assume Eq1: "∀n∈?N. |G`n|<ℵ⇘1⇙" { fix n assume "n∈?N" with Eq1 have "|G`n| ≤ ω" using le_aleph1_nat by simp } then have "n∈?N ⟹ |G`n| ≤ ω" for n . with ‹?N ≲ ω› show ?thesis using InfCard_nat lepoll_imp_cardinal_UN_le by simp qed lemma Aleph1_eq_cardinal_vimage: "f:ℵ⇘1⇙→ω ⟹ ∃n∈ω. |f-``{n}| = ℵ⇘1⇙" proof - assume "f:ℵ⇘1⇙→ω" then have "function(f)" "domain(f) = ℵ⇘1⇙" "range(f)⊆ω" by (simp_all add: domain_of_fun fun_is_function range_fun_subset_codomain) let ?G="λn∈range(f). f-``{n}" from ‹f:ℵ⇘1⇙→ω› have "range(f) ⊆ ω" by (simp add: range_fun_subset_codomain) then have "domain(?G) ≲ ω" using subset_imp_lepoll by simp have "function(?G)" by (simp add:function_lam) from ‹f:ℵ⇘1⇙→ω› have "n∈ω ⟹ f-``{n} ⊆ ℵ⇘1⇙" for n using Pi_vimage_subset by simp with ‹range(f) ⊆ ω› have "ℵ⇘1⇙ = (⋃n∈range(f). f-``{n})" proof (intro equalityI, intro subsetI) fix x assume "x ∈ ℵ⇘1⇙" with ‹f:ℵ⇘1⇙→ω› ‹function(f)› ‹domain(f) = ℵ⇘1⇙› have "x ∈ f-``{f`x}" "f`x ∈ range(f)" using function_apply_Pair vimage_iff apply_rangeI by simp_all then show "x ∈ (⋃n∈range(f). f-``{n})" by auto qed auto { assume "∀n∈range(f). |f-``{n}| < ℵ⇘1⇙" then have "∀n∈domain(?G). |?G`n| < ℵ⇘1⇙" using zero_lt_Aleph1 by (auto) with ‹function(?G)› ‹domain(?G) ≲ ω› have "|⋃n∈domain(?G). ?G`n|≤ω" using lt_Aleph_imp_cardinal_UN_le_nat by blast then have "|⋃n∈range(f). f-``{n}|≤ω" by simp with ‹ℵ⇘1⇙ = _› have "|ℵ⇘1⇙| ≤ ω" by simp then have "ℵ⇘1⇙ ≤ ω" using Card_Aleph Card_cardinal_eq by simp then have "False" using nat_lt_Aleph1 by (blast dest:lt_trans2) } with ‹range(f)⊆ω› obtain n where "n∈ω" "¬(|f -`` {n}| < ℵ⇘1⇙)" by blast moreover from this have "ℵ⇘1⇙ ≤ |f-``{n}|" using not_lt_iff_le Card_is_Ord by auto moreover note ‹n∈ω ⟹ f-``{n} ⊆ ℵ⇘1⇙› ultimately show ?thesis using subset_imp_le_cardinal[THEN le_anti_sym, of _ "ℵ⇘1⇙"] Card_Aleph Card_cardinal_eq by auto qed ― ‹There is some asymmetry between assumptions and conclusion (\<^term>‹(≈)› versus \<^term>‹cardinal›)› lemma eqpoll_Aleph1_cardinal_vimage: assumes "X ≈ ℵ⇘1⇙" "f : X → ω" shows "∃n∈ω. |f-``{n}| = ℵ⇘1⇙" proof - from assms obtain g where "g∈bij(ℵ⇘1⇙,X)" using eqpoll_sym by blast with ‹f : X → ω› have "f O g : ℵ⇘1⇙ → ω" "converse(g) ∈ bij(X, ℵ⇘1⇙)" using bij_is_fun comp_fun bij_converse_bij by blast+ then obtain n where "n∈ω" "|(f O g)-``{n}| = ℵ⇘1⇙" using Aleph1_eq_cardinal_vimage by auto then have "ℵ⇘1⇙ = |converse(g) `` (f -``{n})|" using image_comp converse_comp unfolding vimage_def by simp also from ‹converse(g) ∈ bij(X, ℵ⇘1⇙)› ‹f: X→ ω› have "… = |f -``{n}|" using range_of_subset_eqpoll[of "converse(g)" X _ "f -``{n}"] bij_is_inj cardinal_cong bij_is_fun eqpoll_sym Pi_vimage_subset by fastforce finally show ?thesis using ‹n∈ω› by auto qed subsection‹Applications of transfinite recursive constructions› text‹The next lemma is an application of recursive constructions. It works under the assumption that whenever the already constructed subsequence is small enough, another element can be added.› lemma bounded_cardinal_selection: includes Ord_dests assumes "⋀X. |X| < γ ⟹ X ⊆ G ⟹ ∃a∈G. ∀s∈X. Q(s,a)" "b∈G" "Card(γ)" shows "∃S. S : γ → G ∧ (∀α ∈ γ. ∀β ∈ γ. α<β ⟶ Q(S`α,S`β))" proof - let ?cdltγ="{X∈Pow(G) . |X|<γ}" ― ‹``cardinal less than \<^term>‹γ›''› and ?inQ="λY.{a∈G. ∀s∈Y. Q(s,a)}" from assms have "∀Y ∈ ?cdltγ. ∃a. a ∈ ?inQ(Y)" by blast then have "∃f. f ∈ Pi(?cdltγ,?inQ)" using AC_ball_Pi[of ?cdltγ ?inQ] by simp then obtain f where f_type:"f ∈ Pi(?cdltγ,?inQ)" by auto moreover define Cb where "Cb ≡ λ_∈Pow(G)-?cdltγ. b" moreover from ‹b∈G› have "Cb ∈ Pow(G)-?cdltγ → G" unfolding Cb_def by simp moreover note ‹Card(γ)› ultimately have "f ∪ Cb : (∏x∈Pow(G). ?inQ(x) ∪ G)" using fun_Pi_disjoint_Un[ of f ?cdltγ ?inQ Cb "Pow(G)-?cdltγ" "λ_.G"] Diff_partition[of "{X∈Pow(G). |X|<γ}" "Pow(G)", OF Collect_subset] by auto moreover have "?inQ(x) ∪ G = G" for x by auto ultimately have "f ∪ Cb : Pow(G) → G" by simp define S where "S≡λα∈γ. rec_constr(f ∪ Cb, α)" from ‹f ∪ Cb: Pow(G) → G› ‹Card(γ)› have "S : γ → G" using Ord_in_Ord unfolding S_def by (intro lam_type rec_constr_type) auto moreover have "∀α∈γ. ∀β∈γ. α < β ⟶ Q(S ` α, S ` β)" proof (intro ballI impI) fix α β assume "β∈γ" with ‹Card(γ)› have "{rec_constr(f ∪ Cb, x) . x∈β} = {S`x . x ∈ β}" using Ord_trans[OF _ _ Card_is_Ord, of _ β γ] unfolding S_def by auto moreover from ‹β∈γ› ‹S : γ → G› ‹Card(γ)› have "{S`x . x ∈ β} ⊆ G" using Ord_trans[OF _ _ Card_is_Ord, of _ β γ] apply_type[of S γ "λ_. G"] by auto moreover from ‹Card(γ)› ‹β∈γ› have "|{S`x . x ∈ β}| < γ" using cardinal_RepFun_le[of β] Ord_in_Ord lt_trans1[of "|{S`x . x ∈ β}|" "|β|" γ] Card_lt_iff[THEN iffD2, of β γ, OF _ _ ltI] by force moreover have "∀x∈β. Q(S`x, f ` {S`x . x ∈ β})" proof - from calculation and f_type have "f ` {S`x . x ∈ β} ∈ {a∈G. ∀x∈β. Q(S`x,a)}" using apply_type[of f ?cdltγ ?inQ "{S`x . x ∈ β}"] by blast then show ?thesis by simp qed moreover assume "α∈γ" "α < β" moreover note ‹β∈γ› ‹Cb ∈ Pow(G)-?cdltγ → G› ultimately show "Q(S ` α, S ` β)" using fun_disjoint_apply1[of "{S`x . x ∈ β}" Cb f] domain_of_fun[of Cb] ltD[of α β] by (subst (2) S_def, auto) (subst rec_constr_unfold, auto) qed ultimately show ?thesis by blast qed text‹The following basic result can, in turn, be proved by a bounded-cardinal selection.› lemma Infinite_iff_lepoll_nat: "Infinite(X) ⟷ ω ≲ X" proof assume "Infinite(X)" then obtain b where "b∈X" using Infinite_not_empty by auto { fix Y assume "|Y| < ω" then have "Finite(Y)" using Finite_cardinal_iff' ltD nat_into_Finite by blast with ‹Infinite(X)› have "X ≠ Y" by auto } with ‹b∈X› obtain S where "S : ω → X" "∀α∈ω. ∀β∈ω. α < β ⟶ S`α ≠ S`β" using bounded_cardinal_selection[of ω X "λx y. x≠y"] Card_nat by blast moreover from this have "α ∈ ω ⟹ β ∈ ω ⟹ α≠β ⟹ S`α ≠ S`β" for α β by (rule_tac lt_neq_symmetry[of "ω" "λα β. S`α ≠ S`β"]) auto ultimately show "ω ≲ X" unfolding lepoll_def inj_def by blast qed (intro lepoll_nat_imp_Infinite) lemma Infinite_InfCard_cardinal: "Infinite(X) ⟹ InfCard(|X|)" using lepoll_eq_trans eqpoll_sym lepoll_nat_imp_Infinite Infinite_iff_lepoll_nat Inf_Card_is_InfCard cardinal_eqpoll by simp lemma Finite_to_one_surj_imp_cardinal_eq: assumes "F ∈ Finite_to_one(X,Y) ∩ surj(X,Y)" "Infinite(X)" shows "|Y| = |X|" proof - from ‹F ∈ Finite_to_one(X,Y) ∩ surj(X,Y)› have "X = (⋃y∈Y. {x∈X . F`x = y})" using apply_type by fastforce show ?thesis proof (cases "Finite(Y)") case True with ‹X = (⋃y∈Y. {x∈X . F`x = y})› and assms show ?thesis using Finite_RepFun[THEN [2] Finite_Union, of Y "λy. {x∈X . F`x = y}"] by auto next case False moreover from this have "Y ≲ |Y|" using cardinal_eqpoll eqpoll_sym eqpoll_imp_lepoll by simp moreover note assms moreover from calculation have "y ∈ Y ⟹ |{x∈X . F`x = y}| ≤ |Y|" for y using Infinite_imp_nats_lepoll[THEN lepoll_imp_cardinal_le, of Y "|{x∈X . F`x = y}|"] cardinal_idem by auto ultimately have "|⋃y∈Y. {x∈X . F`x = y}| ≤ |Y|" using lepoll_imp_cardinal_UN_le[of "|Y|" Y] Infinite_InfCard_cardinal[of Y] by simp moreover from ‹F ∈ Finite_to_one(X,Y) ∩ surj(X,Y)› have "|Y| ≤ |X|" using surj_implies_cardinal_le by auto moreover note ‹X = (⋃y∈Y. {x∈X . F`x = y})› ultimately show ?thesis using le_anti_sym by auto qed qed lemma cardinal_map_Un: assumes "Infinite(X)" "Finite(b)" shows "|{a ∪ b . a ∈ X}| = |X|" proof - have "(λa∈X. a ∪ b) ∈ Finite_to_one(X,{a ∪ b . a ∈ X})" "(λa∈X. a ∪ b) ∈ surj(X,{a ∪ b . a ∈ X})" unfolding surj_def proof fix d have "Finite({a ∈ X . a ∪ b = d})" (is "Finite(?Y(b,d))") using ‹Finite(b)› proof (induct arbitrary:d) case 0 have "{a ∈ X . a ∪ 0 = d} = (if d∈X then {d} else 0)" by auto then show ?case by simp next case (cons c b) from ‹c ∉ b› have "?Y(cons(c,b),d) ⊆ (if c∈d then ?Y(b,d) ∪ ?Y(b,d-{c}) else 0)" by auto with cons show ?case using subset_Finite by simp qed moreover assume "d ∈ {x ∪ b . x ∈ X}" ultimately show "Finite({a ∈ X . (λx∈X. x ∪ b) ` a = d})" by simp qed (auto intro:lam_funtype) with assms show ?thesis using Finite_to_one_surj_imp_cardinal_eq by fast qed end