# Theory General_Cardinals

```section ‹ZF sets corresponding to \$\mathbb{R}\$ and \$\mathbb{C}\$ and the cardinality of the contimuum›

theory General_Cardinals
imports ZFC_Typeclasses "HOL-Analysis.Continuum_Not_Denumerable"

begin

subsection ‹Making the embedding from the type class explicit›

definition V_of :: "'a::embeddable ⇒ V"
where "V_of ≡ SOME f. inj f"

lemma inj_V_of: "inj V_of"
unfolding V_of_def by (metis embeddable_class.ex_inj some_eq_imp)

declare inv_f_f [OF inj_V_of, simp]

lemma inv_V_of_image_eq [simp]: "inv V_of ` (V_of ` X) = X"
by (auto simp: image_comp)

lemma infinite_V_of: "infinite (UNIV::'a set) ⟹ infinite (range (V_of::'a::embeddable⇒V))"
using finite_imageD inj_V_of by blast

lemma countable_V_of: "countable (range (V_of::'a::countable⇒V))"
by blast

lemma elts_set_V_of: "small X ⟹ elts (ZFC_in_HOL.set (V_of ` X)) ≈ X"
by (metis inj_V_of inj_eq inj_on_def inj_on_image_eqpoll_self replacement set_of_elts small_iff)

lemma V_of_image_times: "V_of ` (X × Y) ≈ (V_of ` X) × (V_of ` Y)"
proof -
have "V_of ` (X × Y) ≈ X × Y"
by (meson inj_V_of inj_eq inj_onI inj_on_image_eqpoll_self)
also have "… ≈ (V_of ` X) × (V_of ` Y)"
by (metis eqpoll_sym inj_V_of inj_eq inj_onI inj_on_image_eqpoll_self times_eqpoll_cong)
finally show ?thesis .
qed

subsection ‹The cardinality of the continuum›

definition "Real_set ≡ ZFC_in_HOL.set (range (V_of::real⇒V))"
definition "Complex_set ≡ ZFC_in_HOL.set (range (V_of::complex⇒V))"
definition "C_continuum ≡ vcard Real_set"

lemma V_of_Real_set: "bij_betw V_of (UNIV::real set) (elts Real_set)"
by (simp add: Real_set_def bij_betw_def inj_V_of)

lemma uncountable_Real_set: "uncountable (elts Real_set)"
using V_of_Real_set countable_iff_bij uncountable_UNIV_real by blast

lemma "Card C_continuum"

lemma C_continuum_ge: "C_continuum ≥ ℵ1"
by (metis C_continuum_def Ord_ω1 Ord_cardinal Ord_linear2 countable_iff_vcard_less1
uncountable_Real_set)

lemma V_of_Complex_set: "bij_betw V_of (UNIV::complex set) (elts Complex_set)"
by (simp add: Complex_set_def bij_betw_def inj_V_of)

lemma uncountable_Complex_set: "uncountable (elts Complex_set)"
using V_of_Complex_set countableI_bij2 uncountable_UNIV_complex by blast

lemma Complex_vcard: "vcard Complex_set = C_continuum"
proof -
define emb1 where "emb1 ≡ V_of o complex_of_real o inv V_of"
have "elts Real_set ≈ elts Complex_set"
proof (rule lepoll_antisym)
show "elts Real_set ≲ elts Complex_set"
unfolding lepoll_def
proof (intro conjI exI)
show "inj_on emb1 (elts Real_set)"
unfolding emb1_def Real_set_def
by (simp add: inj_V_of inj_compose inj_of_real inj_on_imageI)
show "emb1 ` elts Real_set ⊆ elts Complex_set"
by (simp add: emb1_def Real_set_def Complex_set_def image_subset_iff)
qed
define emb2 where "emb2 ≡ (λz. (V_of (Re z), V_of (Im z))) o inv V_of"
have "elts Complex_set ≲ elts Real_set × elts Real_set"
unfolding lepoll_def
proof (intro conjI exI)
show "inj_on emb2 (elts Complex_set)"
unfolding emb2_def Complex_set_def inj_on_def
by (simp add: complex.expand inj_V_of inj_eq)
show "emb2 ` elts Complex_set ⊆ elts Real_set × elts Real_set"
by (simp add: emb2_def Real_set_def Complex_set_def image_subset_iff)
qed
also have "…  ≈ elts Real_set"
by (simp add: infinite_times_eqpoll_self uncountable_Real_set uncountable_infinite)
finally show "elts Complex_set ≲ elts Real_set" .
qed
then show ?thesis
qed

lemma gcard_Union_le_cmult:
assumes "small U" and κ: "⋀x. x ∈ U ⟹ gcard x ≤ κ" and sm: "⋀x. x ∈ U ⟹ small x"
shows "gcard (⋃U) ≤ gcard U ⊗ κ"
proof -
have "∃f. f ∈ x → elts κ ∧ inj_on f x" if "x ∈ U" for x
using κ [OF that] gcard_le_lepoll by (metis image_subset_iff_funcset lepoll_def sm that)
then obtain φ where φ: "⋀x. x ∈ U ⟹ (φ x) ∈ x → elts κ ∧ inj_on (φ x) x"
by metis
define u where "u ≡ λy. @x. x ∈ U ∧ y ∈ x"
have u: "u y ∈ U ∧ y ∈  (u y)" if "y ∈ ⋃( U)" for y
unfolding u_def using that by (fast intro!: someI2)
define ψ where "ψ ≡ λy. (u y, φ (u y) y)"
have U: "elts (gcard U) ≈ U"
using assms by (simp add: gcard_eqpoll)
have "⋃U ≲ U × elts κ"
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on ψ (⋃ U)"
using φ u by (smt (verit) ψ_def inj_on_def prod.inject)
show "ψ ` ⋃ U ⊆ U × elts κ"
using φ u by (auto simp: ψ_def)
qed
also have "…  ≈ elts (gcard U ⊗ κ)"
using U elts_cmult eqpoll_sym eqpoll_trans times_eqpoll_cong by blast
finally have " (⋃U) ≲ elts (gcard U ⊗ κ)" .
then show ?thesis
by (metis cardinal_idem cmult_def gcard_eq_vcard lepoll_imp_gcard_le small_elts)
qed

lemma gcard_Times [simp]: "gcard (X × Y) = gcard X ⊗ gcard Y"
proof (cases "small X ∧ small Y")
case True
have "elts (gcard (X × Y)) ≈ X × Y"
also have "... ≈ elts (gcard X) × elts (gcard Y)"
by (simp add: True eqpoll_sym gcard_eqpoll times_eqpoll_cong)
also have "... ≈ elts (gcard X ⊗ gcard Y)"
finally show ?thesis
using Card_cardinal_eq cmult_def gcardinal_cong by force
next
case False
have "gcard (X × Y) = 0"
by (metis False Times_empty gcard_big_0 gcard_empty_0 small_Times_iff)
then show ?thesis
by (metis False cmult_0 cmult_commute gcard_big_0)
qed

subsection ‹Countable and uncountable sets›

lemma countable_iff_g_le_Aleph0:
assumes "small X"
shows "countable X ⟷ gcard X ≤ ℵ0"
proof -
have "countable X ⟷ X ≲ elts ω"
by (simp add: ω_def countable_iff_lepoll inj_ord_of_nat)
also have "... ⟷ gcard X ≤ ℵ0"
using Card_ω Card_def assms gcard_le_lepoll lepoll_imp_gcard_le by fastforce
finally show ?thesis .
qed

lemma countable_imp_g_le_Aleph0: "countable X ⟹ gcard X ≤ ℵ0"
by (meson countable countable_iff_g_le_Aleph0)

lemma finite_iff_g_le_Aleph0: "small X ⟹ finite X ⟷ gcard X < ℵ0"
by (metis Aleph_0 eqpoll_finite_iff finite_iff_less_Aleph0 gcard_eq_vcard gcard_eqpoll gcardinal_cong)

lemma finite_imp_g_le_Aleph0: "finite X ⟹ gcard X < ℵ0"
by (meson finite_iff_g_le_Aleph0 finite_imp_small)

lemma countable_infinite_gcard: "countable X ∧ infinite X ⟷ gcard X = ℵ0"
proof -
have "gcard X = ω"
if "countable X" and "infinite X"
using that countable countable_imp_g_le_Aleph0 finite_iff_g_le_Aleph0 less_V_def by auto
moreover have "countable X" if "gcard X = ω"
by (metis Aleph_0 countable_iff_g_le_Aleph0 dual_order.refl gcard_big_0 omega_nonzero that)
moreover have False if "gcard X = ω" and "finite X"
by (metis Aleph_0 dual_order.irrefl finite_iff_g_le_Aleph0 finite_imp_small that)
ultimately show ?thesis
by auto
qed

lemma uncountable_gcard: "small X ⟹ uncountable X ⟷ gcard X > ℵ0"
by (simp add: Card_is_Ord Ord_not_le countable_iff_g_le_Aleph0)

lemma uncountable_gcard_ge: "small X ⟹ uncountable X ⟷ gcard X ≥ ℵ1"
by (simp add: uncountable_gcard csucc_le_Card_iff one_V_def)

lemma subset_smaller_gcard:
assumes κ: "κ ≤ gcard X" "Card κ"
obtains Y where "Y ⊆ X" "gcard Y = κ"
proof (cases "small X")
case True
then have "elts κ ≲ X"
by (meson assms(1) eqpoll_imp_lepoll gcard_eqpoll lepoll_trans less_eq_V_def subset_imp_lepoll)
then obtain Y where "Y ⊆ X" "elts κ ≈ Y"
by (metis bij_betw_def eqpoll_def lepoll_def)
then show ?thesis
using Card_def ‹Card κ› gcardinal_cong that by force
next
case False
with assms show ?thesis
by (metis antisym gcard_big_0 le_0 order_refl that)
qed

lemma Real_gcard: "gcard (UNIV::real set) = C_continuum"
by (metis C_continuum_def V_of_Real_set bij_betw_def gcard_eq_vcard gcard_image)

lemma Complex_gcard: "gcard (UNIV::complex set) = C_continuum"
by (metis Complex_vcard V_of_Complex_set bij_betw_def gcard_eq_vcard gcard_image)

end
```