Theory Cardinal_Library
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⇖"
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⇗↑ν⇖"
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]
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
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
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
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
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
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|<γ}"
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