# Theory ZFC_Library

```theory ZFC_Library
imports "HOL-Library.Countable_Set" "HOL-Library.Equipollence" "HOL-Cardinals.Cardinals"

begin

text‹Equipollence and Lists.›

lemma countable_iff_lepoll: "countable A ⟷ A ≲ (UNIV :: nat set)"
by (auto simp: countable_def lepoll_def)

lemma infinite_times_eqpoll_self:
assumes "infinite A" shows "A × A ≈ A"
by (simp add: Times_same_infinite_bij_betw assms eqpoll_def)

lemma infinite_finite_times_lepoll_self:
assumes "infinite A" "finite B" shows "A × B ≲ A"
proof -
have "B ≲ A"
then have "A × B ≲ A × A"
also have "… ≈ A"
by (simp add: ‹infinite A› infinite_times_eqpoll_self)
finally show ?thesis .
qed

lemma lists_n_lepoll_self:
assumes "infinite A" shows "{l ∈ lists A. length l = n} ≲ A"
proof (induction n)
case 0
have "{l ∈ lists A. length l = 0} = {[]}"
by auto
then show ?case
by (metis Set.set_insert assms ex_in_conv finite.emptyI singleton_lepoll)
next
case (Suc n)
have "{l ∈ lists A. length l = Suc n} = (⋃x∈A. ⋃l ∈ {l ∈ lists A. length l = n}. {x#l})"
by (auto simp: length_Suc_conv)
also have "… ≲ A × {l ∈ lists A. length l = n}"
unfolding lepoll_iff
by (rule_tac x="λ(x,l). Cons x l" in exI) auto
also have "… ≲ A"
proof (cases "finite {l ∈ lists A. length l = n}")
case True
then show ?thesis
using assms infinite_finite_times_lepoll_self by blast
next
case False
have "A × {l ∈ lists A. length l = n} ≲ A × A"
by (simp add: Suc.IH subset_imp_lepoll times_lepoll_mono)
also have "… ≈ A"
finally show ?thesis .
qed
finally show ?case .
qed

lemma infinite_eqpoll_lists:
assumes "infinite A" shows "lists A ≈ A"
proof -
have "lists A ≲ Sigma UNIV (λn. {l ∈ lists A. length l = n})"
unfolding lepoll_iff
by (rule_tac x=snd in exI) (auto simp: in_listsI snd_image_Sigma)
also have "… ≲ (UNIV::nat set) × A"
by (rule Sigma_lepoll_mono) (auto simp: lists_n_lepoll_self assms)
also have "… ≲ A × A"
by (metis assms infinite_le_lepoll order_refl subset_imp_lepoll times_lepoll_mono)
also have "… ≈ A"