Theory HOL_CContinuum

(* Copyright 2021 (C) Mihails Milehins *)

section‹Intermission: upper bound on the cardinality of the continuum (HOL)›
theory HOL_CContinuum
  imports CZH_Sets_Introduction 
begin


text‹
The section presents a proof of ‹|ℝ|≤|𝒫(ℕ)|› in Isabelle/HOL. The proof is 
based on an outline at the beginning of Chapter 4 in the textbook 
‹Set Theory› by Thomas Jech \<^cite>‹"jech_set_2006"›.
›

lemma Pow_lepoll_mono: 
  assumes "A ≲ B"
  shows "Pow A ≲ Pow B"
  using assms by (metis Pow_mono image_Pow_surj lepoll_iff)
  
lemma rat_lepoll_nat: "(UNIV::rat set) ≲ (UNIV::nat set)" 
  unfolding lepoll_def by auto

definition rcut :: "real ⇒ real set" where "rcut r = {x∈ℚ. x < r}"

lemma inj_rcut: "inj rcut"
  unfolding rcut_def
proof(intro inj_onI)
  have xy: "x < y ⟹ {r∈ℚ. r < x} = {r∈ℚ. r < y} ⟹ x = y" for x y :: real
  proof(rule ccontr)
    assume prems: "x < y" "{r∈ℚ. r < x} = {r∈ℚ. r < y}"
    then have "{r∈ℚ. r < y} - {r∈ℚ. r < x} = {}" by simp
    with prems(1) Rats_dense_in_real show False by force
  qed
  then have yx: "y < x ⟹ {r∈ℚ. r < x} = {r∈ℚ. r < y} ⟹ x = y" 
    for x y :: real
    by auto
  show "{z ∈ ℚ. z < x} = {z ∈ ℚ. z < y} ⟹ x = y" for x y :: real 
  proof(rule ccontr)
    fix x y :: real assume prems: "{xa ∈ ℚ. xa < x} = {x ∈ ℚ. x < y}" "x ≠ y"
    from this(2) consider "x < y" | "y < x" by force
    with xy[OF _ prems(1)] yx[OF _ prems(1)] show False by cases auto
  qed
qed

lemma range_rcut_subset_Pow_rat: "range rcut ⊆ Pow ℚ"
proof(intro subsetI)
  fix x assume "x ∈ range rcut" 
  then obtain r where "x = {x∈ℚ. x < r}" unfolding rcut_def by clarsimp
  then show "x ∈ Pow ℚ" by simp
qed

lemma inj_on_inv_of_rat_rat: "inj_on (inv of_rat) ℚ"
  using inv_into_injective by (intro inj_onI) (fastforce simp: Rats_def)

lemma inj_on_inv_image_inv_of_rat_Pow_rat: "inj_on (image (inv of_rat)) (Pow ℚ)"
  by (simp add: inj_on_inv_of_rat_rat inj_on_image_Pow)

lemma inj_on_image_inv_of_rat_range_rcut: 
  "inj_on (image (inv of_rat)) (range rcut)"
  using range_rcut_subset_Pow_rat inj_on_inv_image_inv_of_rat_Pow_rat
  by (auto intro: inj_on_subset)

lemma real_lepoll_ratrat: "(UNIV::real set) ≲ (UNIV::rat set set)" 
  unfolding lepoll_def
proof(intro exI conjI)
  from inj_rcut inj_on_image_inv_of_rat_range_rcut show 
    "inj (image (inv of_rat) ∘ rcut)"
    by (rule comp_inj_on)
qed auto

lemma nat_lepoll_real: "(UNIV::nat set) ≲ (UNIV::real set)"
  using infinite_UNIV_char_0 infinite_countable_subset 
  unfolding lepoll_def 
  by blast

lemma real_lepoll_natnat: "(UNIV::real set) ≲ Pow (UNIV::nat set)"
proof-
  have "(UNIV::rat set set) ≲ (UNIV::nat set set)" 
    unfolding Pow_UNIV[symmetric] by (intro Pow_lepoll_mono rat_lepoll_nat)
  from lepoll_trans[OF real_lepoll_ratrat this] show ?thesis by simp
qed

text‹\newpage›

end