Theory Equipollence
section ‹Equipollence and Other Relations Connected with Cardinality›
theory "Equipollence"
imports FuncSet Countable_Set
begin
subsection‹Eqpoll›
definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≈› 50)
where "eqpoll A B ≡ ∃f. bij_betw f A B"
definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≲› 50)
where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"
definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50)
where "A ≺ B == A ≲ B ∧ ~(A ≈ B)"
lemma lepoll_def': "lepoll A B ≡ ∃f. inj_on f A ∧ f ∈ A → B"
by (simp add: Pi_iff image_subset_iff lepoll_def)
lemma eqpoll_empty_iff_empty [simp]: "A ≈ {} ⟷ A={}"
by (simp add: bij_betw_iff_bijections eqpoll_def)
lemma lepoll_empty_iff_empty [simp]: "A ≲ {} ⟷ A = {}"
by (auto simp: lepoll_def)
lemma not_lesspoll_empty: "¬ A ≺ {}"
by (simp add: lesspoll_def)
lemma lepoll_relational_full:
assumes "⋀y. y ∈ B ⟹ ∃x. x ∈ A ∧ R x y"
and "⋀x y y'. ⟦x ∈ A; y ∈ B; y' ∈ B; R x y; R x y'⟧ ⟹ y = y'"
shows "B ≲ A"
proof -
obtain f where f: "⋀y. y ∈ B ⟹ f y ∈ A ∧ R (f y) y"
using assms by metis
with assms have "inj_on f B"
by (metis inj_onI)
with f show ?thesis
unfolding lepoll_def by blast
qed
lemma eqpoll_iff_card_of_ordIso: "A ≈ B ⟷ ordIso2 (card_of A) (card_of B)"
by (simp add: card_of_ordIso eqpoll_def)
lemma eqpoll_refl [iff]: "A ≈ A"
by (simp add: card_of_refl eqpoll_iff_card_of_ordIso)
lemma eqpoll_finite_iff: "A ≈ B ⟹ finite A ⟷ finite B"
by (meson bij_betw_finite eqpoll_def)
lemma eqpoll_iff_card:
assumes "finite A" "finite B"
shows "A ≈ B ⟷ card A = card B"
using assms by (auto simp: bij_betw_iff_card eqpoll_def)
lemma eqpoll_singleton_iff: "A ≈ {x} ⟷ (∃u. A = {u})"
by (metis card.infinite card_1_singleton_iff eqpoll_finite_iff eqpoll_iff_card not_less_eq_eq)
lemma eqpoll_doubleton_iff: "A ≈ {x,y} ⟷ (∃u v. A = {u,v} ∧ (u=v ⟷ x=y))"
proof (cases "x=y")
case True
then show ?thesis
by (simp add: eqpoll_singleton_iff)
next
case False
then show ?thesis
by (smt (verit, ccfv_threshold) card_1_singleton_iff card_Suc_eq_finite eqpoll_finite_iff
eqpoll_iff_card finite.insertI singleton_iff)
qed
lemma lepoll_antisym:
assumes "A ≲ B" "B ≲ A" shows "A ≈ B"
using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
lemma lepoll_trans [trans]:
assumes "A ≲ B" " B ≲ C" shows "A ≲ C"
proof -
obtain f g where fg: "inj_on f A" "inj_on g B" and "f : A → B" "g ∈ B → C"
by (metis assms lepoll_def')
then have "g ∘ f ∈ A → C"
by auto
with fg show ?thesis
unfolding lepoll_def
by (metis ‹f ∈ A → B› comp_inj_on image_subset_iff_funcset inj_on_subset)
qed
lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)
lemma lepoll_trans2 [trans]: "⟦A ≲ B; B ≈ C⟧ ⟹ A ≲ C"
by (metis bij_betw_def eqpoll_def lepoll_def lepoll_trans order_refl)
lemma eqpoll_sym: "A ≈ B ⟹ B ≈ A"
unfolding eqpoll_def
using bij_betw_the_inv_into by auto
lemma eqpoll_trans [trans]: "⟦A ≈ B; B ≈ C⟧ ⟹ A ≈ C"
unfolding eqpoll_def using bij_betw_trans by blast
lemma eqpoll_imp_lepoll: "A ≈ B ⟹ A ≲ B"
unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)
lemma subset_imp_lepoll: "A ⊆ B ⟹ A ≲ B"
by (force simp: lepoll_def)
lemma lepoll_refl [iff]: "A ≲ A"
by (simp add: subset_imp_lepoll)
lemma lepoll_iff: "A ≲ B ⟷ (∃g. A ⊆ g ` B)"
unfolding lepoll_def
proof safe
fix g assume "A ⊆ g ` B"
then show "∃f. inj_on f A ∧ f ` A ⊆ B"
by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
qed (metis image_mono the_inv_into_onto)
lemma empty_lepoll [iff]: "{} ≲ A"
by (simp add: lepoll_iff)
lemma subset_image_lepoll: "B ⊆ f ` A ⟹ B ≲ A"
by (auto simp: lepoll_iff)
lemma image_lepoll: "f ` A ≲ A"
by (auto simp: lepoll_iff)
lemma infinite_le_lepoll: "infinite A ⟷ (UNIV::nat set) ≲ A"
by (simp add: infinite_iff_countable_subset lepoll_def)
lemma lepoll_Pow_self: "A ≲ Pow A"
unfolding lepoll_def inj_def
proof (intro exI conjI)
show "inj_on (λx. {x}) A"
by (auto simp: inj_on_def)
qed auto
lemma eqpoll_iff_bijections:
"A ≈ B ⟷ (∃f g. (∀x ∈ A. f x ∈ B ∧ g(f x) = x) ∧ (∀y ∈ B. g y ∈ A ∧ f(g y) = y))"
by (auto simp: eqpoll_def bij_betw_iff_bijections)
lemma lepoll_restricted_funspace:
"{f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A ∧ finite {x. f x ≠ k x}} ≲ Fpow (A × B)"
proof -
have *: "∃U ∈ Fpow (A × B). f = (λx. if ∃y. (x, y) ∈ U then SOME y. (x,y) ∈ U else k x)"
if "f ` A ⊆ B" "{x. f x ≠ k x} ⊆ A" "finite {x. f x ≠ k x}" for f
apply (rule_tac x="(λx. (x, f x)) ` {x. f x ≠ k x}" in bexI)
using that by (auto simp: image_def Fpow_def)
show ?thesis
apply (rule subset_image_lepoll [where f = "λU x. if ∃y. (x,y) ∈ U then @y. (x,y) ∈ U else k x"])
using * by (auto simp: image_def)
qed
lemma singleton_lepoll: "{x} ≲ insert y A"
by (force simp: lepoll_def)
lemma singleton_eqpoll: "{x} ≈ {y}"
by (blast intro: lepoll_antisym singleton_lepoll)
lemma subset_singleton_iff_lepoll: "(∃x. S ⊆ {x}) ⟷ S ≲ {()}"
using lepoll_iff by fastforce
lemma infinite_insert_lepoll:
assumes "infinite A" shows "insert a A ≲ A"
proof -
obtain f :: "nat ⇒ 'a" where "inj f" and f: "range f ⊆ A"
using assms infinite_countable_subset by blast
let ?g = "(λz. if z=a then f 0 else if z ∈ range f then f (Suc (inv f z)) else z)"
show ?thesis
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on ?g (insert a A)"
using inj_on_eq_iff [OF ‹inj f›]
by (auto simp: inj_on_def)
show "?g ` insert a A ⊆ A"
using f by auto
qed
qed
lemma infinite_insert_eqpoll: "infinite A ⟹ insert a A ≈ A"
by (simp add: lepoll_antisym infinite_insert_lepoll subset_imp_lepoll subset_insertI)
lemma finite_lepoll_infinite:
assumes "infinite A" "finite B" shows "B ≲ A"
proof -
have "B ≲ (UNIV::nat set)"
unfolding lepoll_def
using finite_imp_inj_to_nat_seg [OF ‹finite B›] by blast
then show ?thesis
using ‹infinite A› infinite_le_lepoll lepoll_trans by auto
qed
lemma countable_lepoll: "⟦countable A; B ≲ A⟧ ⟹ countable B"
by (meson countable_image countable_subset lepoll_iff)
lemma countable_eqpoll: "⟦countable A; B ≈ A⟧ ⟹ countable B"
using countable_lepoll eqpoll_imp_lepoll by blast
subsection‹The strict relation›
lemma lesspoll_not_refl [iff]: "~ (i ≺ i)"
by (simp add: lepoll_antisym lesspoll_def)
lemma lesspoll_imp_lepoll: "A ≺ B ==> A ≲ B"
by (unfold lesspoll_def, blast)
lemma lepoll_iff_leqpoll: "A ≲ B ⟷ A ≺ B | A ≈ B"
using eqpoll_imp_lepoll lesspoll_def by blast
lemma lesspoll_trans [trans]: "⟦X ≺ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
lemma lesspoll_trans1 [trans]: "⟦X ≲ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
lemma lesspoll_trans2 [trans]: "⟦X ≺ Y; Y ≲ Z⟧ ⟹ X ≺ Z"
by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)
lemma eq_lesspoll_trans [trans]: "⟦X ≈ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
using eqpoll_imp_lepoll lesspoll_trans1 by blast
lemma lesspoll_eq_trans [trans]: "⟦X ≺ Y; Y ≈ Z⟧ ⟹ X ≺ Z"
using eqpoll_imp_lepoll lesspoll_trans2 by blast
lemma lesspoll_Pow_self: "A ≺ Pow A"
unfolding lesspoll_def bij_betw_def eqpoll_def
by (meson lepoll_Pow_self Cantors_theorem)
lemma finite_lesspoll_infinite:
assumes "infinite A" "finite B" shows "B ≺ A"
by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def)
lemma countable_lesspoll: "⟦countable A; B ≺ A⟧ ⟹ countable B"
using countable_lepoll lesspoll_def by blast
lemma lepoll_iff_card_le: "⟦finite A; finite B⟧ ⟹ A ≲ B ⟷ card A ≤ card B"
by (simp add: inj_on_iff_card_le lepoll_def)
lemma lepoll_iff_finite_card: "A ≲ {..<n::nat} ⟷ finite A ∧ card A ≤ n"
by (metis card_lessThan finite_lessThan finite_surj lepoll_iff lepoll_iff_card_le)
lemma eqpoll_iff_finite_card: "A ≈ {..<n::nat} ⟷ finite A ∧ card A = n"
by (metis card_lessThan eqpoll_finite_iff eqpoll_iff_card finite_lessThan)
lemma lesspoll_iff_finite_card: "A ≺ {..<n::nat} ⟷ finite A ∧ card A < n"
by (metis eqpoll_iff_finite_card lepoll_iff_finite_card lesspoll_def order_less_le)
subsection‹Mapping by an injection›
lemma inj_on_image_eqpoll_self: "inj_on f A ⟹ f ` A ≈ A"
by (meson bij_betw_def eqpoll_def eqpoll_sym)
lemma inj_on_image_lepoll_1 [simp]:
assumes "inj_on f A" shows "f ` A ≲ B ⟷ A ≲ B"
by (meson assms image_lepoll lepoll_def lepoll_trans order_refl)
lemma inj_on_image_lepoll_2 [simp]:
assumes "inj_on f B" shows "A ≲ f ` B ⟷ A ≲ B"
by (meson assms eq_iff image_lepoll lepoll_def lepoll_trans)
lemma inj_on_image_lesspoll_1 [simp]:
assumes "inj_on f A" shows "f ` A ≺ B ⟷ A ≺ B"
by (meson assms image_lepoll le_less lepoll_def lesspoll_trans1)
lemma inj_on_image_lesspoll_2 [simp]:
assumes "inj_on f B" shows "A ≺ f ` B ⟷ A ≺ B"
by (meson assms eqpoll_sym inj_on_image_eqpoll_self lesspoll_eq_trans)
lemma inj_on_image_eqpoll_1 [simp]:
assumes "inj_on f A" shows "f ` A ≈ B ⟷ A ≈ B"
by (metis assms eqpoll_trans inj_on_image_eqpoll_self eqpoll_sym)
lemma inj_on_image_eqpoll_2 [simp]:
assumes "inj_on f B" shows "A ≈ f ` B ⟷ A ≈ B"
by (metis assms inj_on_image_eqpoll_1 eqpoll_sym)
subsection ‹Inserting elements into sets›
lemma insert_lepoll_insertD:
assumes "insert u A ≲ insert v B" "u ∉ A" "v ∉ B" shows "A ≲ B"
proof -
obtain f where inj: "inj_on f (insert u A)" and fim: "f ` (insert u A) ⊆ insert v B"
by (meson assms lepoll_def)
show ?thesis
unfolding lepoll_def
proof (intro exI conjI)
let ?g = "λx∈A. if f x = v then f u else f x"
show "inj_on ?g A"
using inj ‹u ∉ A› by (auto simp: inj_on_def)
show "?g ` A ⊆ B"
using fim ‹u ∉ A› image_subset_iff inj inj_on_image_mem_iff by fastforce
qed
qed
lemma insert_eqpoll_insertD: "⟦insert u A ≈ insert v B; u ∉ A; v ∉ B⟧ ⟹ A ≈ B"
by (meson insert_lepoll_insertD eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)
lemma insert_lepoll_cong:
assumes "A ≲ B" "b ∉ B" shows "insert a A ≲ insert b B"
proof -
obtain f where f: "inj_on f A" "f ` A ⊆ B"
by (meson assms lepoll_def)
let ?f = "λu ∈ insert a A. if u=a then b else f u"
show ?thesis
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on ?f (insert a A)"
using f ‹b ∉ B› by (auto simp: inj_on_def)
show "?f ` insert a A ⊆ insert b B"
using f ‹b ∉ B› by auto
qed
qed
lemma insert_eqpoll_cong:
"⟦A ≈ B; a ∉ A; b ∉ B⟧ ⟹ insert a A ≈ insert b B"
by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong lepoll_antisym)
lemma insert_eqpoll_insert_iff:
"⟦a ∉ A; b ∉ B⟧ ⟹ insert a A ≈ insert b B ⟷ A ≈ B"
by (meson insert_eqpoll_insertD insert_eqpoll_cong)
lemma insert_lepoll_insert_iff:
" ⟦a ∉ A; b ∉ B⟧ ⟹ (insert a A ≲ insert b B) ⟷ (A ≲ B)"
by (meson insert_lepoll_insertD insert_lepoll_cong)
lemma less_imp_insert_lepoll:
assumes "A ≺ B" shows "insert a A ≲ B"
proof -
obtain f where "inj_on f A" "f ` A ⊂ B"
using assms by (metis bij_betw_def eqpoll_def lepoll_def lesspoll_def psubset_eq)
then obtain b where b: "b ∈ B" "b ∉ f ` A"
by auto
show ?thesis
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on (f(a:=b)) (insert a A)"
using b ‹inj_on f A› by (auto simp: inj_on_def)
show "(f(a:=b)) ` insert a A ⊆ B"
using ‹f ` A ⊂ B› by (auto simp: b)
qed
qed
lemma finite_insert_lepoll: "finite A ⟹ (insert a A ≲ A) ⟷ (a ∈ A)"
proof (induction A rule: finite_induct)
case (insert x A)
then show ?case
by (metis insertI2 insert_lepoll_insert_iff insert_subsetI lepoll_trans subsetI subset_imp_lepoll)
qed auto
subsection‹Binary sums and unions›
lemma Un_lepoll_mono:
assumes "A ≲ C" "B ≲ D" "disjnt C D" shows "A ∪ B ≲ C ∪ D"
proof -
obtain f g where inj: "inj_on f A" "inj_on g B" and fg: "f ` A ⊆ C" "g ` B ⊆ D"
by (meson assms lepoll_def)
have "inj_on (λx. if x ∈ A then f x else g x) (A ∪ B)"
using inj ‹disjnt C D› fg unfolding disjnt_iff
by (fastforce intro: inj_onI dest: inj_on_contraD split: if_split_asm)
with fg show ?thesis
unfolding lepoll_def
by (rule_tac x="λx. if x ∈ A then f x else g x" in exI) auto
qed
lemma Un_eqpoll_cong: "⟦A ≈ C; B ≈ D; disjnt A B; disjnt C D⟧ ⟹ A ∪ B ≈ C ∪ D"
by (meson Un_lepoll_mono eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)
lemma sum_lepoll_mono:
assumes "A ≲ C" "B ≲ D" shows "A <+> B ≲ C <+> D"
proof -
obtain f g where "inj_on f A" "f ` A ⊆ C" "inj_on g B" "g ` B ⊆ D"
by (meson assms lepoll_def)
then show ?thesis
unfolding lepoll_def
by (rule_tac x="case_sum (Inl ∘ f) (Inr ∘ g)" in exI) (force simp: inj_on_def)
qed
lemma sum_eqpoll_cong: "⟦A ≈ C; B ≈ D⟧ ⟹ A <+> B ≈ C <+> D"
by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym sum_lepoll_mono)
subsection‹Binary Cartesian products›
lemma times_square_lepoll: "A ≲ A × A"
unfolding lepoll_def inj_def
proof (intro exI conjI)
show "inj_on (λx. (x,x)) A"
by (auto simp: inj_on_def)
qed auto
lemma times_commute_eqpoll: "A × B ≈ B × A"
unfolding eqpoll_def
by (force intro: bij_betw_byWitness [where f = "λ(x,y). (y,x)" and f' = "λ(x,y). (y,x)"])
lemma times_assoc_eqpoll: "(A × B) × C ≈ A × (B × C)"
unfolding eqpoll_def
by (force intro: bij_betw_byWitness [where f = "λ((x,y),z). (x,(y,z))" and f' = "λ(x,(y,z)). ((x,y),z)"])
lemma times_singleton_eqpoll: "{a} × A ≈ A"
proof -
have "{a} × A = (λx. (a,x)) ` A"
by auto
also have "… ≈ A"
proof (rule inj_on_image_eqpoll_self)
show "inj_on (Pair a) A"
by (auto simp: inj_on_def)
qed
finally show ?thesis .
qed
lemma times_lepoll_mono:
assumes "A ≲ C" "B ≲ D" shows "A × B ≲ C × D"
proof -
obtain f g where "inj_on f A" "f ` A ⊆ C" "inj_on g B" "g ` B ⊆ D"
by (meson assms lepoll_def)
then show ?thesis
unfolding lepoll_def
by (rule_tac x="λ(x,y). (f x, g y)" in exI) (auto simp: inj_on_def)
qed
lemma times_eqpoll_cong: "⟦A ≈ C; B ≈ D⟧ ⟹ A × B ≈ C × D"
by (metis eqpoll_imp_lepoll eqpoll_sym lepoll_antisym times_lepoll_mono)
lemma
assumes "B ≠ {}" shows lepoll_times1: "A ≲ A × B" and lepoll_times2: "A ≲ B × A"
using assms lepoll_iff by fastforce+
lemma times_0_eqpoll: "{} × A ≈ {}"
by (simp add: eqpoll_iff_bijections)
lemma Sigma_inj_lepoll_mono:
assumes h: "inj_on h A" "h ` A ⊆ C" and "⋀x. x ∈ A ⟹ B x ≲ D (h x)"
shows "Sigma A B ≲ Sigma C D"
proof -
have "⋀x. x ∈ A ⟹ ∃f. inj_on f (B x) ∧ f ` (B x) ⊆ D (h x)"
by (meson assms lepoll_def)
then obtain f where "⋀x. x ∈ A ⟹ inj_on (f x) (B x) ∧ f x ` B x ⊆ D (h x)"
by metis
with h show ?thesis
unfolding lepoll_def inj_on_def
by (rule_tac x="λ(x,y). (h x, f x y)" in exI) force
qed
lemma Sigma_lepoll_mono:
assumes "A ⊆ C" "⋀x. x ∈ A ⟹ B x ≲ D x" shows "Sigma A B ≲ Sigma C D"
using Sigma_inj_lepoll_mono [of id] assms by auto
lemma sum_times_distrib_eqpoll: "(A <+> B) × C ≈ (A × C) <+> (B × C)"
unfolding eqpoll_def
proof
show "bij_betw (λ(x,z). case_sum(λy. Inl(y,z)) (λy. Inr(y,z)) x) ((A <+> B) × C) (A × C <+> B × C)"
by (rule bij_betw_byWitness [where f' = "case_sum (λ(x,z). (Inl x, z)) (λ(y,z). (Inr y, z))"]) auto
qed
lemma Sigma_eqpoll_cong:
assumes h: "bij_betw h A C" and BD: "⋀x. x ∈ A ⟹ B x ≈ D (h x)"
shows "Sigma A B ≈ Sigma C D"
proof (intro lepoll_antisym)
show "Sigma A B ≲ Sigma C D"
by (metis Sigma_inj_lepoll_mono bij_betw_def eqpoll_imp_lepoll subset_refl assms)
have "inj_on (inv_into A h) C ∧ inv_into A h ` C ⊆ A"
by (metis bij_betw_def bij_betw_inv_into h set_eq_subset)
then show "Sigma C D ≲ Sigma A B"
by (smt (verit, best) BD Sigma_inj_lepoll_mono bij_betw_inv_into_right eqpoll_sym h image_subset_iff lepoll_refl lepoll_trans2)
qed
lemma prod_insert_eqpoll:
assumes "a ∉ A" shows "insert a A × B ≈ B <+> A × B"
unfolding eqpoll_def
proof
show "bij_betw (λ(x,y). if x=a then Inl y else Inr (x,y)) (insert a A × B) (B <+> A × B)"
by (rule bij_betw_byWitness [where f' = "case_sum (λy. (a,y)) id"]) (auto simp: assms)
qed
subsection‹General Unions›
lemma Union_eqpoll_Times:
assumes B: "⋀x. x ∈ A ⟹ F x ≈ B" and disj: "pairwise (λx y. disjnt (F x) (F y)) A"
shows "(⋃x∈A. F x) ≈ A × B"
proof (rule lepoll_antisym)
obtain b where b: "⋀x. x ∈ A ⟹ bij_betw (b x) (F x) B"
using B unfolding eqpoll_def by metis
show "⋃(F ` A) ≲ A × B"
unfolding lepoll_def
proof (intro exI conjI)
define χ where "χ ≡ λz. THE x. x ∈ A ∧ z ∈ F x"
have χ: "χ z = x" if "x ∈ A" "z ∈ F x" for x z
unfolding χ_def
by (smt (verit, best) disj disjnt_iff pairwiseD that(1,2) theI_unique)
let ?f = "λz. (χ z, b (χ z) z)"
show "inj_on ?f (⋃(F ` A))"
unfolding inj_on_def
by clarify (metis χ b bij_betw_inv_into_left)
show "?f ` ⋃(F ` A) ⊆ A × B"
using χ b bij_betwE by blast
qed
show "A × B ≲ ⋃(F ` A)"
unfolding lepoll_def
proof (intro exI conjI)
let ?f = "λ(x,y). inv_into (F x) (b x) y"
have *: "inv_into (F x) (b x) y ∈ F x" if "x ∈ A" "y ∈ B" for x y
by (metis b bij_betw_imp_surj_on inv_into_into that)
then show "inj_on ?f (A × B)"
unfolding inj_on_def
by clarsimp (metis (mono_tags, lifting) b bij_betw_inv_into_right disj disjnt_iff pairwiseD)
show "?f ` (A × B) ⊆ ⋃ (F ` A)"
by clarsimp (metis b bij_betw_imp_surj_on inv_into_into)
qed
qed
lemma UN_lepoll_UN:
assumes A: "⋀x. x ∈ A ⟹ B x ≲ C x"
and disj: "pairwise (λx y. disjnt (C x) (C y)) A"
shows "⋃ (B`A) ≲ ⋃ (C`A)"
proof -
obtain f where f: "⋀x. x ∈ A ⟹ inj_on (f x) (B x) ∧ f x ` (B x) ⊆ (C x)"
using A unfolding lepoll_def by metis
show ?thesis
unfolding lepoll_def
proof (intro exI conjI)
define χ where "χ ≡ λz. @x. x ∈ A ∧ z ∈ B x"
have χ: "χ z ∈ A ∧ z ∈ B (χ z)" if "x ∈ A" "z ∈ B x" for x z
unfolding χ_def by (metis (mono_tags, lifting) someI_ex that)
let ?f = "λz. (f (χ z) z)"
show "inj_on ?f (⋃(B ` A))"
using disj f unfolding inj_on_def disjnt_iff pairwise_def image_subset_iff
by (metis UN_iff χ)
show "?f ` ⋃ (B ` A) ⊆ ⋃ (C ` A)"
using χ f unfolding image_subset_iff by blast
qed
qed
lemma UN_eqpoll_UN:
assumes A: "⋀x. x ∈ A ⟹ B x ≈ C x"
and B: "pairwise (λx y. disjnt (B x) (B y)) A"
and C: "pairwise (λx y. disjnt (C x) (C y)) A"
shows "(⋃x∈A. B x) ≈ (⋃x∈A. C x)"
proof (rule lepoll_antisym)
show "⋃ (B ` A) ≲ ⋃ (C ` A)"
by (meson A C UN_lepoll_UN eqpoll_imp_lepoll)
show "⋃ (C ` A) ≲ ⋃ (B ` A)"
by (simp add: A B UN_lepoll_UN eqpoll_imp_lepoll eqpoll_sym)
qed
subsection‹General Cartesian products (Pi)›
lemma PiE_sing_eqpoll_self: "({a} →⇩E B) ≈ B"
proof -
have 1: "x = y"
if "x ∈ {a} →⇩E B" "y ∈ {a} →⇩E B" "x a = y a" for x y
by (metis IntD2 PiE_def extensionalityI singletonD that)
have 2: "x ∈ (λh. h a) ` ({a} →⇩E B)" if "x ∈ B" for x
using that by (rule_tac x="λz∈{a}. x" in image_eqI) auto
show ?thesis
unfolding eqpoll_def bij_betw_def inj_on_def
by (force intro: 1 2)
qed
lemma lepoll_funcset_right:
assumes "B ≲ B'" shows "A →⇩E B ≲ A →⇩E B'"
proof -
obtain f where f: "inj_on f B" "f ` B ⊆ B'"
by (meson assms lepoll_def)
let ?G = "λg. λz ∈ A. f(g z)"
have "inj_on ?G (A →⇩E B)"
using f by (smt (verit, best) PiE_ext PiE_mem inj_on_def restrict_apply')
moreover have "?G ` (A →⇩E B) ⊆ (A →⇩E B')"
using f by fastforce
ultimately show ?thesis
by (meson lepoll_def)
qed
lemma lepoll_funcset_left:
assumes "B ≠ {}" "A ≲ A'"
shows "A →⇩E B ≲ A' →⇩E B"
proof -
obtain b where "b ∈ B"
using assms by blast
obtain f where "inj_on f A" and fim: "f ` A ⊆ A'"
using assms by (auto simp: lepoll_def)
then obtain h where h: "⋀x. x ∈ A ⟹ h (f x) = x"
using the_inv_into_f_f by fastforce
let ?F = "λg. λu ∈ A'. if h u ∈ A then g(h u) else b"
show ?thesis
unfolding lepoll_def inj_on_def
proof (intro exI conjI ballI impI ext)
fix k l x
assume k: "k ∈ A →⇩E B" and l: "l ∈ A →⇩E B" and "?F k = ?F l"
then have "?F k (f x) = ?F l (f x)"
by simp
then show "k x = l x"
by (smt (verit, best) PiE_arb fim h image_subset_iff k l restrict_apply')
next
show "?F ` (A →⇩E B) ⊆ A' →⇩E B"
using ‹b ∈ B› by force
qed
qed
lemma lepoll_funcset:
"⟦B ≠ {}; A ≲ A'; B ≲ B'⟧ ⟹ A →⇩E B ≲ A' →⇩E B'"
by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto
lemma lepoll_PiE:
assumes "⋀i. i ∈ A ⟹ B i ≲ C i"
shows "PiE A B ≲ PiE A C"
proof -
obtain f where f: "⋀i. i ∈ A ⟹ inj_on (f i) (B i) ∧ (f i) ` B i ⊆ C i"
using assms unfolding lepoll_def by metis
let ?G = "λg. λi ∈ A. f i (g i)"
have "inj_on ?G (PiE A B)"
by (smt (verit, ccfv_SIG) PiE_ext PiE_iff f inj_on_def restrict_apply')
moreover have "?G ` (PiE A B) ⊆ (PiE A C)"
using f by fastforce
ultimately show ?thesis
by (meson lepoll_def)
qed
lemma card_le_PiE_subindex:
assumes "A ⊆ A'" "Pi⇩E A' B ≠ {}"
shows "PiE A B ≲ PiE A' B"
proof -
have "⋀x. x ∈ A' ⟹ ∃y. y ∈ B x"
using assms by blast
then obtain g where g: "⋀x. x ∈ A' ⟹ g x ∈ B x"
by metis
let ?F = "λf x. if x ∈ A then f x else if x ∈ A' then g x else undefined"
have "Pi⇩E A B ⊆ (λf. restrict f A) ` Pi⇩E A' B"
proof
show "f ∈ Pi⇩E A B ⟹ f ∈ (λf. restrict f A) ` Pi⇩E A' B" for f
using ‹A ⊆ A'›
by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
qed
then have "Pi⇩E A B ≲ (λf. λi ∈ A. f i) ` Pi⇩E A' B"
by (simp add: subset_imp_lepoll)
also have "… ≲ PiE A' B"
by (rule image_lepoll)
finally show ?thesis .
qed
lemma finite_restricted_funspace:
assumes "finite A" "finite B"
shows "finite {f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A}" (is "finite ?F")
proof (rule finite_subset)
show "finite ((λU x. if ∃y. (x,y) ∈ U then @y. (x,y) ∈ U else k x) ` Pow(A × B))" (is "finite ?G")
using assms by auto
show "?F ⊆ ?G"
proof
fix f
assume "f ∈ ?F"
then show "f ∈ ?G"
by (rule_tac x="(λx. (x,f x)) ` {x. f x ≠ k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
qed
qed
proposition finite_PiE_iff:
"finite(PiE I S) ⟷ PiE I S = {} ∨ finite {i ∈ I. ~(∃a. S i ⊆ {a})} ∧ (∀i ∈ I. finite(S i))"
(is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
case False
define J where "J ≡ {i ∈ I. ∄a. S i ⊆ {a}}"
show ?thesis
proof
assume L: ?lhs
have "infinite (Pi⇩E I S)" if "infinite J"
proof -
have "(UNIV::nat set) ≲ (UNIV::(nat⇒bool) set)"
proof -
have "∀N::nat set. inj_on (=) N"
by (simp add: inj_on_def)
then show ?thesis
by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
qed
also have "… = (UNIV::nat set) →⇩E (UNIV::bool set)"
by auto
also have "… ≲ J →⇩E (UNIV::bool set)"
by (metis empty_not_UNIV infinite_le_lepoll lepoll_funcset_left that)
also have "… ≲ Pi⇩E J S"
proof -
have *: "(UNIV::bool set) ≲ S i" if "i ∈ I" and §: "∀a. ¬ S i ⊆ {a}" for i
proof -
obtain a b where "{a,b} ⊆ S i" "a ≠ b"
by (metis § empty_subsetI insert_subset subsetI)
then show ?thesis
by (metis Set.set_insert UNIV_bool insert_iff insert_lepoll_cong insert_subset singleton_lepoll)
qed
show ?thesis
by (auto simp: * J_def intro: lepoll_PiE)
qed
also have "… ≲ Pi⇩E I S"
using False by (auto simp: J_def intro: card_le_PiE_subindex)
finally have "(UNIV::nat set) ≲ Pi⇩E I S" .
then show ?thesis
by (simp add: infinite_le_lepoll)
qed
moreover have "finite (S i)" if "i ∈ I" for i
proof (rule finite_subset)
obtain f where f: "f ∈ PiE I S"
using False by blast
show "S i ⊆ (λf. f i) ` Pi⇩E I S"
proof
show "s ∈ (λf. f i) ` Pi⇩E I S" if "s ∈ S i" for s
using that f ‹i ∈ I›
by (rule_tac x="λj. if j = i then s else f j" in image_eqI) auto
qed
next
show "finite ((λx. x i) ` Pi⇩E I S)"
using L by blast
qed
ultimately show ?rhs
using L
by (auto simp: J_def False)
next
assume R: ?rhs
have "∀i ∈ I - J. ∃a. S i = {a}"
using False J_def by blast
then obtain a where a: "∀i ∈ I - J. S i = {a i}"
by metis
let ?F = "{f. f ` J ⊆ (⋃i ∈ J. S i) ∧ {i. f i ≠ (if i ∈ I then a i else undefined)} ⊆ J}"
have *: "finite (Pi⇩E I S)"
if "finite J" and "∀i∈I. finite (S i)"
proof (rule finite_subset)
have "⋀f j. ⟦f ∈ Pi⇩E I S; j ∈ J⟧ ⟹ f j ∈ ⋃ (S ` J)"
using J_def by blast
moreover
have "⋀f j. ⟦f ∈ Pi⇩E I S; f j ≠ (if j ∈ I then a j else undefined)⟧ ⟹ j ∈ J"
by (metis DiffI PiE_E a singletonD)
ultimately show "Pi⇩E I S ⊆ ?F" by force
show "finite ?F"
proof (rule finite_restricted_funspace [OF ‹finite J›])
show "finite (⋃ (S ` J))"
using that J_def by blast
qed
qed
show ?lhs
using R by (auto simp: * J_def)
qed
qed auto
corollary finite_funcset_iff:
"finite(I →⇩E S) ⟷ (∃a. S ⊆ {a}) ∨ I = {} ∨ finite I ∧ finite S"
by (fastforce simp: finite_PiE_iff PiE_eq_empty_iff dest: subset_singletonD)
subsection ‹Misc other resultd›
lemma lists_lepoll_mono:
assumes "A ≲ B" shows "lists A ≲ lists B"
proof -
obtain f where f: "inj_on f A" "f ` A ⊆ B"
by (meson assms lepoll_def)
moreover have "inj_on (map f) (lists A)"
using f unfolding inj_on_def
by clarsimp (metis list.inj_map_strong)
ultimately show ?thesis
unfolding lepoll_def by force
qed
lemma lepoll_lists: "A ≲ lists A"
unfolding lepoll_def inj_on_def by(rule_tac x="λx. [x]" in exI) auto
text ‹Dedekind's definition of infinite set›
lemma infinite_iff_psubset: "infinite A ⟷ (∃B. B ⊂ A ∧ A≈B)"
proof
assume "infinite A"
then obtain f :: "nat ⇒ 'a" where "inj f" and f: "range f ⊆ A"
by (meson infinite_countable_subset)
define C where "C ≡ A - range f"
have C: "A = range f ∪ C" "range f ∩ C = {}"
using f by (auto simp: C_def)
have *: "range (f ∘ Suc) ⊂ range f"
using inj_eq [OF ‹inj f›] by (fastforce simp: set_eq_iff)
have "range f ∪ C ≈ range (f ∘ Suc) ∪ C"
proof (intro Un_eqpoll_cong)
show "range f ≈ range (f ∘ Suc)"
by (meson ‹inj f› eqpoll_refl inj_Suc inj_compose inj_on_image_eqpoll_2)
show "disjnt (range f) C"
by (simp add: C disjnt_def)
then show "disjnt (range (f ∘ Suc)) C"
using "*" disjnt_subset1 by blast
qed auto
moreover have "range (f ∘ Suc) ∪ C ⊂ A"
using "*" f C_def by blast
ultimately show "∃B⊂A. A ≈ B"
by (metis C(1))
next
assume "∃B⊂A. A ≈ B" then show "infinite A"
by (metis card_subset_eq eqpoll_finite_iff eqpoll_iff_card psubsetE)
qed
lemma infinite_iff_psubset_le: "infinite A ⟷ (∃B. B ⊂ A ∧ A ≲ B)"
by (meson eqpoll_imp_lepoll infinite_iff_psubset lepoll_antisym psubsetE subset_imp_lepoll)
end