diff --git a/thys/Cardinality_Continuum/Cardinality_Continuum.thy b/thys/Cardinality_Continuum/Cardinality_Continuum.thy
new file mode 100644
--- /dev/null
+++ b/thys/Cardinality_Continuum/Cardinality_Continuum.thy
@@ -0,0 +1,402 @@
+(*
+  File:     Cardinality_Continuum/Cardinality_Continuum.thy
+  Author:   Manuel Eberl (University of Innsbruck)
+
+  The cardinality of the continuum, i.e. the real numbers, in a few different variations.
+*)
+section \<open>The Cardinality of the Continuum\<close>
+theory Cardinality_Continuum
+  imports Complex_Main Cardinality_Continuum_Library
+begin
+
+subsection \<open>$|\mathbb{R}| \leq |2^\mathbb{Q}|$ via Dedekind cuts\<close>
+
+lemma le_cSup_iff:
+  fixes A :: "'a :: conditionally_complete_linorder set"
+  assumes "A \<noteq> {}" "bdd_above A"
+  shows   "Sup A \<ge> c \<longleftrightarrow> (\<forall>x<c. \<exists>y\<in>A. y > x)"
+  using assms by (meson less_cSup_iff not_le_imp_less order_less_irrefl order_less_le_trans)
+
+text \<open>
+  We show that the function mapping a real number to all the rational numbers below it is an
+  injective map from the reals to $2^\mathbb{Q}$. This is the same idea that is used in
+  the Dedekind cut definition of the reals.
+\<close>
+lemma inj_Dedekind_cut:
+  fixes f :: "real \<Rightarrow> rat set"
+  defines "f \<equiv> (\<lambda>x::real. {r::rat. of_rat r < x})"
+  shows   "inj f"
+proof
+  fix x y :: real
+  assume "f x = f y"
+
+  have *: "Sup (real_of_rat ` {r. real_of_rat r < z}) = z" for z :: real
+  proof -
+    have "real_of_rat ` {r. real_of_rat r < z} = {r\<in>\<rat>. r < z}"
+      by (auto elim!: Rats_cases)
+    also have "Sup \<dots> = z"
+    proof (rule antisym)
+      have "{r \<in> \<rat>. r < z} \<noteq> {}"
+        using Rats_no_bot_less less_eq_real_def by blast
+      hence "Sup {r\<in>\<rat>. r < z} \<le> Sup {..z}"
+        by (rule cSup_subset_mono) auto
+      also have "\<dots> = z"
+        by simp
+      finally show "Sup {r\<in>\<rat>. r < z} \<le> z" .
+    next
+      show "Sup {r\<in>\<rat>. r < z} \<ge> z"
+      proof (subst le_cSup_iff)
+        show "{r\<in>\<rat>. r < z} \<noteq> {}"
+          using Rats_no_bot_less less_eq_real_def by blast
+        show "\<forall>y<z. \<exists>r\<in>{r\<in>\<rat>. r < z}. y < r"
+          using Rats_dense_in_real by fastforce
+        show "bdd_above {r \<in> \<rat>. r < z}"
+          by (rule bdd_aboveI[of _ z]) auto
+      qed
+    qed
+    finally show ?thesis .
+  qed
+
+  from \<open>f x = f y\<close> have "Sup (real_of_rat ` f x) = Sup (real_of_rat ` f y)"
+    by simp
+  thus "x = y"
+    by (simp only: * f_def)
+qed
+
+
+subsection \<open>$2^{|\mathbb{N}|} \leq |\mathbb{R}|$ via ternary fractions\<close>
+
+text \<open>
+  For the other direction, we construct an injective function that maps a set of natural numbers
+  \<open>A\<close> to a real number by constructing a ternary decimal number of the form
+  $d_0. d_1 d_2 d_3 \ldots$ where $d_m$ is 1 if \<open>m \<in> A\<close> and 0 otherwise.
+
+  We will first show a few more general results about such \<open>n\<close>-ary fraction expansions.
+\<close>
+
+lemma geometric_sums':
+  fixes c :: "'a :: real_normed_field"
+  assumes "norm c < 1"
+  shows   "(\<lambda>n. c ^ (n + m)) sums (c ^ m / (1 - c))"
+proof -
+  have "(\<lambda>n. c ^ m * c ^ n) sums (c ^ m * (1 / (1 - c)))"
+    by (intro sums_mult geometric_sums assms)
+  thus ?thesis
+    by (simp add: power_add field_simps)
+qed
+
+lemma summable_nary_fraction:
+  fixes d :: real and f :: "nat \<Rightarrow> real"
+  assumes "\<And>n. norm (f n) \<le> c" "d > 1"
+  shows   "summable (\<lambda>n. f n / d ^ n)"
+proof (rule summable_comparison_test)
+  show "\<exists>N. \<forall>n\<ge>N. norm (f n / d ^ n :: real) \<le> c * (1 / d) ^ n"
+    using assms by (intro exI[of _ 0]) (auto simp: field_simps)
+  show "summable (\<lambda>n. c * (1 / d) ^ n :: real)"
+    using assms by (intro summable_mult summable_geometric) auto
+qed    
+
+text \<open>
+  Consider two \<open>n\<close>-ary fraction expansions $u = u_1. u_2 u_3 \ldots$ and
+  $v = v_1. v_2 v_3 \ldots$ with \<open>n \<ge> 2\<close>.
+  Suppose that all the $u_i$ and $v_i$ are between 0 and \<open>n - 2\<close> (i.e. the highest digit
+  does not occur).
+  Then \<open>u\<close> and \<open>v\<close> are equal if and only if all $u_i = v_i$ for all \<open>i\<close>.
+
+  Note that without the additional restriction the result does not hold, as e.g.
+  the decimal numbers $0.2$ and $0.1\overline{9}$ are equal.
+
+  The reasoning boils down to showing that if \<open>m\<close> is the smallest index where the two sequences
+  differ, then $|u-v| \geq \frac{1}{d-1} > 0$.
+\<close>
+lemma nary_fraction_unique:
+  fixes u v :: "nat \<Rightarrow> nat"
+  assumes f_eq: "(\<Sum>n. real (u n) / real d ^ n) = (\<Sum>n. real (v n) / real d ^ n)"
+  assumes uv: "\<And>n. u n \<le> d - 2" "\<And>n. v n \<le> d - 2" and d: "d \<ge> 2"
+  shows   "u = v"
+proof -
+  define f :: "(nat \<Rightarrow> nat) \<Rightarrow> real" where
+    "f = (\<lambda>u. \<Sum>n. real (u n) / real d ^ n)"
+
+  have "u m = v m" for m
+  proof (induction m rule: less_induct)
+    case (less m)
+    show "u m = v m"
+    proof (rule ccontr)
+      assume "u m \<noteq> v m"
+
+      show False
+        using \<open>u m \<noteq> v m\<close> uv less.IH f_eq
+      proof (induction "u m" "v m" arbitrary: u v rule: linorder_wlog)
+        case (sym u v)
+        from sym(1)[of v u] sym(2-) show ?case
+          by (simp add: eq_commute)
+      next
+        case (le u v)
+        have uv': "real (u n) \<le> real d - 2" "real (v n) \<le> real d - 2" for n
+          by (metis d of_nat_diff of_nat_le_iff of_nat_numeral le(3,4))+
+        have "f u - f v - (real (u m) - real (v m)) / real d ^ m \<le> 
+                (real d - 2) * ((1 / real d) ^ m / (real d - 1))"
+        proof (rule sums_le)
+          have "(\<lambda>n. (real (u n) - real (v n)) / real d ^ n) sums (f u - f v)"
+            unfolding diff_divide_distrib f_def using le d uv'
+            by (intro sums_diff summable_sums summable_nary_fraction[where c = "real d - 2"]) auto
+          hence "(\<lambda>n. (real (u (n + m)) - real (v (n + m))) / real d ^ (n + m)) sums
+                   (f u - f v - (\<Sum>n<m. (real (u n) - real (v n)) / real d ^ n))"
+            by (rule sums_split_initial_segment)
+          also have "(\<Sum>n<m. (real (u n) - real (v n)) / real d ^ n) = 0"
+            by (intro sum.neutral) (use le in auto)
+          finally have "(\<lambda>n. (real (u (n + m)) - real (v (n + m))) / real d ^ (n + m)) sums (f u - f v)"
+            by simp
+          thus "(\<lambda>n. (real (u (Suc n + m)) - real (v (Suc n + m))) / real d ^ (Suc n + m)) sums
+                   (f u - f v - (real (u m) - real (v m)) / real d ^ m)"
+            by (subst sums_Suc_iff) auto
+        next
+          have "(\<lambda>n. (real d - 2) * ((1 / real d) ^ (n + Suc m))) sums
+                  ((real d - 2) * ((1 / real d) ^ Suc m / (1 - 1 / real d)))"
+            using d by (intro sums_mult geometric_sums') auto
+          thus "(\<lambda>n. (real d - 2) * ((1 / real d) ^ (n + Suc m))) sums
+                  ((real d - 2) * ((1 / real d) ^ m / (real d - 1)) :: real)"
+            using d by (simp add: sums_iff field_simps)
+        next
+          fix n :: nat
+          have "(real (u (Suc n + m)) - real (v (Suc n + m))) / real d ^ (Suc n + m) \<le>
+                  ((real d - 2) - 0) / real d ^ (Suc n + m)"
+            using uv' by (intro divide_right_mono diff_mono) auto
+          thus "(real (u (Suc n + m)) - real (v (Suc n + m))) / real d ^ (Suc n + m) \<le>
+                  (real d - 2) * (1 / real d) ^ (n + Suc m)"
+            by (simp add: field_simps)
+        qed
+        hence "f u - f v \<le>
+                 (real d - 2) / (real d - 1) / real d ^ m + (real (u m) - real (v m)) / real d ^ m"
+          by (simp add: field_simps)
+        also have "\<dots> = ((real d - 2) / (real d - 1) + real (u m) - real (v m)) / real d ^ m"
+          by (simp add: add_divide_distrib diff_divide_distrib)
+        also have "\<dots> = ((real d - 2) / (real d - 1) + real_of_int (int (u m) - int (v m))) / real d ^ m"
+          using \<open>u m \<le> v m\<close> by simp
+        also have "\<dots> \<le> ((real d - 2) / (real d - 1) + -1) / real d ^ m"
+          using le d by (intro divide_right_mono add_mono) auto
+        also have "(real d - 2) / (real d - 1) + -1 = -1 / (real d - 1)"
+          using d by (simp add: field_simps)
+        also have "\<dots> < 0"
+          using d by (simp add: field_simps)
+        finally have "f u - f v < 0"
+          using d by (simp add: field_simps)
+        with le show False
+          by (simp add: f_def)
+      qed
+    qed
+  qed
+  thus ?thesis
+    by blast
+qed
+
+text \<open>
+  It now follows straightforwardly that mapping sets of natural numbers to ternary fraction
+  expansions is indeed injective. For binary fractions, this would not work due to the
+  aforementioned issue.
+\<close>
+lemma inj_nat_set_to_ternary:
+  fixes f :: "nat set \<Rightarrow> real"
+  defines "f \<equiv> (\<lambda>A. \<Sum>n. (if n \<in> A then 1 else 0) / 3 ^ n)"
+  shows   "inj f"
+proof
+  fix A B :: "nat set"
+  assume "f A = f B"
+  have "(\<lambda>n. if n \<in> A then 1 else 0 :: nat) = (\<lambda>n. if n \<in> B then 1 else 0 :: nat)"
+  proof (rule nary_fraction_unique)
+    have *: "(\<Sum>n. (if n \<in> A then 1 else 0) / 3 ^ n) =
+             (\<Sum>n. real (if n \<in> A then 1 else 0) / real 3 ^ n)"
+      for A by (intro suminf_cong) auto
+    show "(\<Sum>n. real (if n \<in> A then 1 else 0) / real 3 ^ n) =
+           (\<Sum>n. real (if n \<in> B then 1 else 0) / real 3 ^ n)"
+      using \<open>f A = f B\<close> by (simp add: f_def *)
+  qed auto
+  thus "A = B"
+    by (metis equalityI subsetI zero_neq_one)
+qed
+
+
+subsection \<open>Equipollence proof\<close>
+
+theorem eqpoll_UNIV_real: "(UNIV :: real set) \<approx> (UNIV :: nat set set)"
+proof (rule lepoll_antisym)
+  show "(UNIV :: nat set set) \<lesssim> (UNIV :: real set)"
+    unfolding lepoll_def using inj_nat_set_to_ternary by blast
+next
+  have "(UNIV :: real set) \<lesssim> (UNIV :: rat set set)"
+    unfolding lepoll_def using inj_Dedekind_cut by blast
+  also have "\<dots> = Pow (UNIV :: rat set)"
+    by simp
+  also have "\<dots> \<approx> Pow (UNIV :: nat set)"
+    by (rule eqpoll_Pow) (auto simp: infinite_UNIV_char_0 eqpoll_UNIV_nat_iff)
+  also have "\<dots> = (UNIV :: nat set set)"
+    by simp
+  finally show "(UNIV :: real set) \<lesssim> (UNIV :: nat set set)" .
+qed
+
+text \<open>
+  We can also write the language in the language of cardinal numbers as
+  $|\mathbb{R}| = 2^{\aleph_0}$ using Isabelle's cardinal number library:
+\<close>
+corollary card_of_UNIV_real: "|UNIV :: real set| =o ctwo ^c natLeq"
+proof -
+  have "|UNIV :: real set| =o |UNIV :: nat set set|"
+    using eqpoll_UNIV_real by (simp add: eqpoll_iff_card_of_ordIso)
+  also have "|UNIV :: nat set set| =o cpow |UNIV :: nat set|"
+    by (simp add: cpow_def)
+  also have "cpow |UNIV :: nat set| =o ctwo ^c |UNIV :: nat set|"
+    by (rule cpow_cexp_ctwo)
+  also have "ctwo ^c |UNIV :: nat set| =o ctwo ^c natLeq"
+    by (intro cexp_cong2) (simp_all add: card_of_nat Card_order_ctwo)
+  finally show ?thesis .
+qed
+
+
+subsection \<open>Corollaries for real intervals\<close>
+
+text \<open>
+  It is easy to show that any real interval (whether open, closed, or infinite) is equipollent
+  to the full set of real numbers.
+\<close>
+lemma eqpoll_Ioo_real:
+  fixes a b :: real
+  assumes "a < b"
+  shows   "{a<..<b} \<approx> (UNIV :: real set)"
+proof -
+  have Ioo: "{a<..<b} \<approx> {0::real<..<1}" if "a < b" for a b :: real
+  proof -
+    have "bij_betw (\<lambda>x. x * (b - a) + a) {0<..<1} {a<..<b}"
+    proof (rule bij_betwI[of _ _ _ "\<lambda>y. (y - a) / (b - a)"], goal_cases)
+      case 1
+      show ?case
+      proof
+        fix x :: real assume x: "x \<in> {0<..<1}"
+        have "x * (b - a) + a > 0 + a"
+          using x \<open>a < b\<close> by (intro add_strict_right_mono mult_pos_pos) auto
+        moreover have "x * (b - a) + a < 1 * (b - a) + a"
+          using x \<open>a < b\<close> by (intro add_strict_right_mono mult_strict_right_mono) auto
+        ultimately show "x * (b - a) + a \<in> {a<..<b}"
+          by simp
+      qed
+    qed (use \<open>a < b\<close> in \<open>auto simp: field_simps\<close>)
+    thus ?thesis
+      using eqpoll_def eqpoll_sym by blast
+  qed
+
+  have "{a<..<b} \<approx> {-pi/2<..<pi/2}"
+    using eqpoll_trans[OF Ioo[of a b] eqpoll_sym[OF Ioo[of "-pi/2" "pi/2"]]] assms
+    by simp
+  also have "bij_betw tan {-pi/2<..<pi/2} (UNIV :: real set)"
+    by (rule bij_betwI[of _ _ _ arctan]) 
+       (use arctan_lbound arctan_ubound in \<open>auto simp: arctan_tan tan_arctan\<close>)
+  hence "{-pi/2<..<pi/2} \<approx> (UNIV :: real set)"
+    using eqpoll_def by blast
+  finally show ?thesis .
+qed
+
+lemma eqpoll_real: 
+  assumes "{a::real<..<b} \<subseteq> X" "a < b"
+  shows   "X \<approx> (UNIV :: real set)"
+  using eqpoll_Ioo_real[OF assms(2)] assms(1)
+  by (meson eqpoll_sym lepoll_antisym lepoll_trans1 subset_UNIV subset_imp_lepoll)
+  
+lemma eqpoll_Icc_real: "(a::real) < b \<Longrightarrow> {a..b} \<approx> (UNIV :: real set)"
+  and eqpoll_Ioc_real: "(a::real) < b \<Longrightarrow> {a<..b} \<approx> (UNIV :: real set)"
+  and eqpoll_Ico_real: "(a::real) < b \<Longrightarrow> {a..<b} \<approx> (UNIV :: real set)"
+  by (rule eqpoll_real[of a b]; force)+
+
+lemma eqpoll_Ici_real: "{a::real..} \<approx> (UNIV :: real set)"
+  and eqpoll_Ioi_real: "{a::real<..} \<approx> (UNIV :: real set)"
+  by (rule eqpoll_real[of a "a + 1"]; force)+
+
+lemma eqpoll_Iic_real: "{..a::real} \<approx> (UNIV :: real set)"
+  and eqpoll_Iio_real: "{..<a::real} \<approx> (UNIV :: real set)"
+  by (rule eqpoll_real[of "a - 1" a]; force)+
+
+lemmas eqpoll_real_ivl =
+  eqpoll_Ioo_real eqpoll_Ioc_real eqpoll_Ico_real eqpoll_Icc_real
+  eqpoll_Iio_real eqpoll_Iic_real eqpoll_Ici_real eqpoll_Ioi_real
+
+lemmas card_of_ivl_real = 
+  eqpoll_real_ivl[THEN eqpoll_imp_card_of_ordIso, THEN ordIso_transitive[OF _ card_of_UNIV_real]]
+
+
+subsection \<open>Corollaries for vector spaces\<close>
+
+text \<open>
+  We will now also show some results about the cardinality of vector spaces. To do this,
+  we use the obvious isomorphism between a vector space \<open>V\<close> with a basis \<open>B\<close> and the set of 
+  finite-support functions \<open>B \<rightarrow> V\<close>.
+\<close>
+lemma (in vector_space) card_of_span:
+  assumes "independent B"
+  shows   "|span B| =o |Func_finsupp 0 B (UNIV :: 'a set)|"
+proof -
+  define f :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b" where "f = (\<lambda>g. \<Sum>b | g b \<noteq> 0. scale (g b) b)"
+  define g :: "'b \<Rightarrow> 'b \<Rightarrow> 'a" where "g = representation B"
+  have "bij_betw g (span B) (Func_finsupp 0 B UNIV)"
+  proof (rule bij_betwI[of _ _ _ f], goal_cases)
+    case 1
+    thus ?case
+      by (auto simp: g_def Func_finsupp_def finite_representation intro: representation_ne_zero)
+  next
+    case 2
+    thus ?case
+      by (auto simp: f_def Func_finsupp_def intro!: span_sum span_scale intro: span_base)
+  next
+    case (3 x)
+    show "f (g x) = x" unfolding g_def f_def
+      by (intro sum_nonzero_representation_eq) (use 3 assms in auto)
+  next
+    case (4 v)
+    show "g (f v) = v" unfolding g_def using 4
+      by (intro representation_eqI)
+         (auto simp: assms f_def Func_finsupp_def intro: span_base
+               intro!: sum.cong span_sum span_scale split: if_splits)
+  qed
+  thus "|span B| =o |Func_finsupp 0 B (UNIV :: 'a set)|"
+    by (simp add: card_of_ordIsoI)
+qed
+
+text \<open>
+  We can now easily show the following: Let \<open>K\<close> be an infinite field and $V$ a non-trivial
+  finite-dimensional \<open>K\<close>-vector space. Then \<open>|V| = |K|\<close>.
+\<close>
+lemma (in vector_space) card_of_span_finite_dim_infinite_field:
+  assumes "independent B" and "finite B" and "B \<noteq> {}" and "infinite (UNIV :: 'a set)"
+  shows   "|span B| =o |UNIV :: 'a set|"
+proof -
+  have "|span B| =o |Func_finsupp 0 B (UNIV :: 'a set)|"
+    by (rule card_of_span) fact
+  also have "|Func_finsupp 0 B (UNIV :: 'a set)| =o cmax |B| |UNIV :: 'a set|"
+  proof (rule card_of_Func_finsupp_infinite)
+    show "UNIV - {0 :: 'a} \<noteq> {}"
+      using assms by (metis finite.emptyI infinite_remove)
+  qed (use assms in auto)
+  also have "cmax |B| |UNIV :: 'a set| =o |UNIV :: 'a set|"
+    using assms by (intro cmax2 ordLeq3_finite_infinite) auto
+  finally show ?thesis .
+qed
+
+text \<open>
+  Similarly, we can show the following: Let \<open>V\<close> be an infinite-dimensional vector space \<open>V\<close> over 
+  some (not necessarily infinite) field \<open>K\<close>. Then $|V| = \text{max}(\text{dim}_K(V), |K|)$.
+\<close>
+lemma (in vector_space) card_of_span_infinite_dim_infinite_field:
+  assumes "independent B" "infinite B"
+  shows   "|span B| =o cmax |B| |UNIV :: 'a set|"
+proof -
+  have "|span B| =o |Func_finsupp 0 B (UNIV :: 'a set)|"
+    by (rule card_of_span) fact
+  also have "|Func_finsupp 0 B (UNIV :: 'a set)| =o cmax |B| |UNIV :: 'a set|"
+  proof (rule card_of_Func_finsupp_infinite)
+    have "(1 :: 'a) \<in> UNIV" "(1 :: 'a) \<noteq> 0"
+      by auto
+    thus "UNIV - {0 :: 'a} \<noteq> {}"
+      by blast
+  qed (use assms in auto)
+  finally show "|span B| =o cmax |B| |UNIV :: 'a set|" .
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Cardinality_Continuum/Cardinality_Continuum_Library.thy b/thys/Cardinality_Continuum/Cardinality_Continuum_Library.thy
new file mode 100644
--- /dev/null
+++ b/thys/Cardinality_Continuum/Cardinality_Continuum_Library.thy
@@ -0,0 +1,453 @@
+(*
+  File:     Cardinality_Continuum/Cardinality_Continuum_Library.thy
+  Author:   Manuel Eberl (University of Innsbruck)
+
+  Some missing facts about cardinality and equipollence, but most notably
+  the definition and cardinality results about the "finite subsets of" operator and the
+  "functions with finite support" operator.
+*)
+section \<open>Auxiliary material\<close>
+theory Cardinality_Continuum_Library
+  imports "HOL-Library.Equipollence" "HOL-Cardinals.Cardinals"
+begin
+
+subsection \<open>Miscellaneous facts about cardinalities\<close>
+
+(* Equipollence *)
+lemma eqpoll_Pow [intro]:
+  assumes "A \<approx> B"
+  shows   "Pow A \<approx> Pow B"
+proof -
+  from assms obtain f where "bij_betw f A B"
+    unfolding eqpoll_def by blast
+  hence "bij_betw ((`) f) (Pow A) (Pow B)"
+    by (rule bij_betw_Pow)
+  thus ?thesis
+    unfolding eqpoll_def by blast
+qed
+
+lemma lepoll_UNIV_nat_iff: "A \<lesssim> (UNIV :: nat set) \<longleftrightarrow> countable A"
+  unfolding countable_def lepoll_def by simp
+
+lemma countable_eqpoll:     
+  assumes "countable A" "A \<approx> B"
+  shows   "countable B"
+  using assms countable_iff_bij unfolding eqpoll_def by blast
+
+lemma countable_eqpoll_cong: "A \<approx> B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
+  using countable_eqpoll[of A B] countable_eqpoll[of B A]
+  by (auto simp: eqpoll_sym)
+
+lemma eqpoll_UNIV_nat_iff: "A \<approx> (UNIV :: nat set) \<longleftrightarrow> countable A \<and> infinite A"
+proof
+  assume *: "A \<approx> (UNIV :: nat set)"
+  show "countable A \<and> infinite A"
+    using eqpoll_finite_iff[OF *] countable_eqpoll_cong[OF *] by simp
+next
+  assume *: "countable A \<and> infinite A"
+  thus "A \<approx> (UNIV :: nat set)"
+    by (meson countableE_infinite eqpoll_def)
+qed
+
+
+(* HOL-Cardinals *)
+lemma ordLeq_finite_infinite:
+  "finite A \<Longrightarrow> infinite B \<Longrightarrow> (card_of A, card_of B) \<in> ordLeq"
+  by (meson card_of_Well_order card_of_ordLeq_finite ordLeq_total)
+
+lemma eqpoll_imp_card_of_ordIso: "A \<approx> B \<Longrightarrow> |A| =o |B|"
+  by (simp add: eqpoll_iff_card_of_ordIso)
+
+lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
+  by (simp add: cexp_def)
+
+lemma card_of_leq_natLeq_iff_countable:
+  "|X| \<le>o natLeq \<longleftrightarrow> countable X"
+proof -
+  have "countable X  \<longleftrightarrow> |X| \<le>o |UNIV :: nat set|"
+    unfolding countable_def by (meson card_of_ordLeq top_greatest)
+  with card_of_nat show ?thesis
+    using ordIso_symmetric ordLeq_ordIso_trans by blast
+qed
+
+lemma card_of_Sigma_cong:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> |B x| =o |B' x|"
+  shows   "|SIGMA x:A. B x| =o |SIGMA x:A. B' x|"
+proof -
+  have "\<exists>f. bij_betw f (B x) (B' x)" if "x \<in> A" for x
+    using assms that card_of_ordIso by blast
+  then obtain f where f: "\<And>x. x \<in> A \<Longrightarrow> bij_betw (f x) (B x) (B' x)"
+    by metis
+  have "bij_betw (\<lambda>(x,y). (x, f x y)) (SIGMA x:A. B x) (SIGMA x:A. B' x)"
+    using f by (fastforce simp: bij_betw_def inj_on_def image_def)
+  thus ?thesis
+    by (rule card_of_ordIsoI)
+qed
+
+lemma Cfinite_cases:
+  assumes "Cfinite c"
+  obtains n :: nat where "(c, natLeq_on n) \<in> ordIso"
+proof -
+  from assms have "card_of (Field c) =o natLeq_on (card (Field c))"
+    by (simp add: cfinite_def finite_imp_card_of_natLeq_on)
+  with that[of "card (Field c)"] show ?thesis
+    using assms card_of_unique ordIso_transitive by blast
+qed
+
+lemma empty_nat_ordIso_czero: "({} :: (nat \<times> nat) set) =o czero"
+proof -
+  have "({} :: (nat \<times> nat) set) =o |{} :: nat set|"
+    using finite_imp_card_of_natLeq_on[of "{} :: nat set"] by (simp add: ordIso_symmetric)
+  moreover have "|{} :: nat set| =o czero"
+    by (simp add: card_of_ordIso_czero_iff_empty)
+  ultimately show "({} :: (nat \<times> nat) set) =o czero"
+    using ordIso_symmetric ordIso_transitive by blast
+qed
+
+lemma card_order_on_empty: "card_order_on {} {}"
+  unfolding card_order_on_def well_order_on_def linear_order_on_def partial_order_on_def
+            preorder_on_def antisym_def trans_def refl_on_def total_on_def ordLeq_def embed_def
+  by (auto intro!: ordLeq_refl)
+
+lemma natLeq_on_plus_ordIso: "natLeq_on (m + n) =o natLeq_on m +c natLeq_on n"
+proof -
+  have "{0..<m+n} = {0..<m} \<union> {m..<m+n}"
+    by auto
+  also have "card_of ({0..<m} \<union> {m..<m+n}) =o card_of ({0..<m} <+> {m..<m+n})"
+    by (rule card_of_Un_Plus_ordIso) auto
+  also have "card_of ({0..<m} <+> {m..<m+n}) =o card_of {0..<m} +c card_of {m..<m+n}"
+    by (rule Plus_csum)
+  also have "card_of {0..<m} +c card_of {m..<m+n} =o natLeq_on m +c natLeq_on n"
+    using finite_imp_card_of_natLeq_on[of "{m..<m+n}"]
+    by (intro csum_cong card_of_less) auto
+  finally have "|{0..<m+n}| =o natLeq_on m +c natLeq_on n" .
+  moreover have "card_of {0..<m+n} =o natLeq_on (m + n)"
+    by (rule card_of_less)
+  ultimately show ?thesis
+    using ordIso_symmetric ordIso_transitive by blast
+qed
+
+lemma natLeq_on_1_ord_iso: "natLeq_on 1 =o BNF_Cardinal_Arithmetic.cone"
+proof -
+  have "|{0..<1::nat}| =o natLeq_on 1"
+    by (rule card_of_less)
+  hence "|{0::nat}| =o natLeq_on 1"
+    by simp
+  moreover have "|{0::nat}| =o BNF_Cardinal_Arithmetic.cone"
+    by (rule single_cone)
+  ultimately show ?thesis
+    using ordIso_symmetric ordIso_transitive by blast
+qed
+
+lemma cexp_infinite_finite_ordLeq:
+  assumes "Cinfinite c" "Cfinite c'"
+  shows   "c ^c c' \<le>o c"
+proof -
+  have c: "Card_order c"
+    using assms by auto
+  from assms obtain n where n: "c' =o natLeq_on n"
+    using Cfinite_cases by auto
+  have "c ^c c' =o c ^c natLeq_on n"
+    using assms(2) by (intro cexp_cong2 c n) auto
+  also have "c ^c natLeq_on n \<le>o c"
+  proof (induction n)
+    case 0
+    have "c ^c natLeq_on 0 =o c ^c czero"
+      by (intro cexp_cong2) (use assms in \<open>auto simp: empty_nat_ordIso_czero card_order_on_empty\<close>)
+    also have "c ^c czero =o BNF_Cardinal_Arithmetic.cone"
+      by (rule cexp_czero)
+    also have "BNF_Cardinal_Arithmetic.cone \<le>o c"
+      using assms by (simp add: Cfinite_cone Cfinite_ordLess_Cinfinite ordLess_imp_ordLeq)
+    finally show ?case .
+  next
+    case (Suc n)
+    have "c ^c natLeq_on (Suc n) =o c ^c (natLeq_on n +c natLeq_on 1)"
+      using assms natLeq_on_plus_ordIso[of n 1]
+      by (intro cexp_cong2) (auto simp: natLeq_on_Card_order intro: ordIso_symmetric)
+    also have "c ^c (natLeq_on n +c natLeq_on 1) =o c ^c natLeq_on n *c c ^c natLeq_on 1"
+      by (rule cexp_csum)
+    also have "c ^c natLeq_on n *c c ^c natLeq_on 1 \<le>o c *c c"
+    proof (rule cprod_mono)
+      show "c ^c natLeq_on n \<le>o c"
+        by (rule Suc.IH)
+      have "c ^c natLeq_on 1 =o c ^c BNF_Cardinal_Arithmetic.cone"
+        by (intro cexp_cong2 c natLeq_on_1_ord_iso natLeq_on_Card_order)
+      also have "c ^c BNF_Cardinal_Arithmetic.cone =o c"
+        by (intro cexp_cone c)
+      finally show "c ^c natLeq_on 1 \<le>o c"
+        by (rule ordIso_imp_ordLeq)
+    qed
+    also have "c *c c =o c"
+      using assms(1) by (rule cprod_infinite)
+    finally show "c ^c natLeq_on (Suc n) \<le>o c" .
+  qed
+  finally show ?thesis .  
+qed
+
+lemma cexp_infinite_finite_ordIso:
+  assumes "Cinfinite c" "Cfinite c'" "BNF_Cardinal_Arithmetic.cone \<le>o c'"
+  shows   "c ^c c' =o c"
+proof -
+  have c: "Card_order c"
+    using assms by auto
+  have "c =o c ^c BNF_Cardinal_Arithmetic.cone"
+    by (rule ordIso_symmetric, rule cexp_cone) fact
+  also have "c ^c BNF_Cardinal_Arithmetic.cone \<le>o c ^c c'"
+    by (intro cexp_mono2 c assms Card_order_cone) (use cone_not_czero in auto)
+  finally have "c \<le>o c ^c c'" .
+  moreover have "c ^c c' \<le>o c"
+    by (rule cexp_infinite_finite_ordLeq) fact+
+  ultimately show ?thesis
+    by (simp add: ordIso_iff_ordLeq)
+qed
+
+lemma Cfinite_ordLeq_Cinfinite:
+  assumes "Cfinite c" "Cinfinite c'"
+  shows   "c \<le>o c'"
+  using assms Cfinite_ordLess_Cinfinite ordLess_imp_ordLeq by blast
+
+lemma cfinite_card_of_iff [simp]: "BNF_Cardinal_Arithmetic.cfinite (card_of X) \<longleftrightarrow> finite X"
+  by (simp add: cfinite_def)
+
+lemma cinfinite_card_of_iff [simp]: "BNF_Cardinal_Arithmetic.cinfinite (card_of X) \<longleftrightarrow> infinite X"
+  by (simp add: cinfinite_def)
+
+lemma Func_conv_PiE: "Func A B = PiE A (\<lambda>_. B)"
+  by (auto simp: Func_def PiE_def extensional_def)
+
+lemma finite_Func [intro]:
+  assumes "finite A" "finite B"
+  shows   "finite (Func A B)"
+  using assms unfolding Func_conv_PiE by (intro finite_PiE)
+
+lemma ordLeq_antisym: "(c, c') \<in> ordLeq \<Longrightarrow> (c', c) \<in> ordLeq \<Longrightarrow> (c, c') \<in> ordIso"
+  using ordIso_iff_ordLeq by auto
+
+lemma cmax_cong:
+  assumes "(c1, c1') \<in> ordIso" "(c2, c2') \<in> ordIso" "Card_order c1" "Card_order c2"
+  shows   "cmax c1 c2 =o cmax c1' c2'"
+proof -
+  have [intro]: "Card_order c1'" "Card_order c2'"
+    using assms Card_order_ordIso2 by auto
+  have "c1 \<le>o c2 \<or> c2 \<le>o c1"
+    by (intro ordLeq_total) (use assms in auto)
+  thus ?thesis
+  proof
+    assume le: "c1 \<le>o c2"
+    with assms have le': "c1' \<le>o c2'"
+      by (meson ordIso_iff_ordLeq ordLeq_transitive)
+    have "cmax c1 c2 =o c2"
+      by (rule cmax2) (use le assms in auto)
+    moreover have "cmax c1' c2' =o c2'"
+      by (rule cmax2) (use le' assms in auto)
+    ultimately show ?thesis
+      using assms ordIso_symmetric ordIso_transitive by metis
+  next
+    assume le: "c2 \<le>o c1"
+    with assms have le': "c2' \<le>o c1'"
+      by (meson ordIso_iff_ordLeq ordLeq_transitive)
+    have "cmax c1 c2 =o c1"
+      by (rule cmax1) (use le assms in auto)
+    moreover have "cmax c1' c2' =o c1'"
+      by (rule cmax1) (use le' assms in auto)
+    ultimately show ?thesis
+      using assms ordIso_symmetric ordIso_transitive by metis
+  qed
+qed
+
+
+subsection \<open>The set of finite subsets\<close>
+
+text \<open>
+  We define an operator \<open>FinPow(X)\<close> that, given a set \<open>X\<close>, returns the set of all
+  finite subsets of that set. For finite \<open>X\<close>, this is boring since it is obviously just the
+  power set. For infinite \<open>X\<close>, it is however a useful concept to have.
+
+  We will show that if \<open>X\<close> is infinite then the cardinality of \<open>FinPow(X)\<close> is exactly
+  the same as that of \<open>X\<close>.
+\<close>
+definition FinPow :: "'a set \<Rightarrow> 'a set set" where
+  "FinPow X = {Y. Y \<subseteq> X \<and> finite Y}"
+
+lemma finite_FinPow [intro]: "finite A \<Longrightarrow> finite (FinPow A)"
+  by (auto simp: FinPow_def)
+
+lemma in_FinPow_iff: "Y \<in> FinPow X \<longleftrightarrow> Y \<subseteq> X \<and> finite Y"
+  by (auto simp: FinPow_def)
+
+lemma FinPow_subseteq_Pow: "FinPow X \<subseteq> Pow X"
+  unfolding FinPow_def by blast
+
+lemma FinPow_eq_Pow: "finite X \<Longrightarrow> FinPow X = Pow X"
+  unfolding FinPow_def using finite_subset by blast
+
+theorem card_of_FinPow_infinite:
+  assumes "infinite A"
+  shows   "|FinPow A| =o |A|"
+proof -
+  have "set ` lists A = FinPow A"
+    using finite_list[where ?'a = 'a] by (force simp: FinPow_def)
+  hence "|FinPow A| \<le>o |lists A|"
+    by (metis card_of_image)
+  also have "|lists A| =o |A|"
+    using assms by (rule card_of_lists_infinite)
+  finally have "|FinPow A| \<le>o |A|" .
+  moreover have "inj_on (\<lambda>x. {x}) A" "(\<lambda>x. {x}) ` A \<subseteq> FinPow A"
+    by (auto simp: inj_on_def FinPow_def)
+  hence "|A| \<le>o |FinPow A|"
+    using card_of_ordLeq by blast
+  ultimately show ?thesis
+    by (simp add: ordIso_iff_ordLeq)
+qed
+
+
+subsection \<open>The set of functions with finite support\<close>
+
+text \<open>
+  Next, we define an operator $\text{Func\_finsupp}_z(A, B)$ that, given sets \<open>A\<close> and \<open>B\<close> and
+  an element \<open>z \<in> B\<close>, returns the set of functions \<open>f : A \<rightarrow> B\<close> that have \<^emph>\<open>finite support\<close>, i.e.\ 
+  that map all but a finite subset of \<open>A\<close> to \<open>z\<close>.
+\<close>
+definition Func_finsupp :: "'b \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+  "Func_finsupp z A B = {f\<in>A \<rightarrow> B. (\<forall>x. x \<notin> A \<longrightarrow> f x = z) \<and> finite {x. f x \<noteq> z}}"
+
+lemma bij_betw_Func_finsup_Func_finite:
+  assumes "finite A"
+  shows   "bij_betw (\<lambda>f. restrict f A) (Func_finsupp z A B) (Func A B)"
+  by (rule bij_betwI[of _ _ _ "\<lambda>f x. if x \<in> A then f x else z"])
+     (use assms in \<open>auto simp: Func_finsupp_def Func_def\<close>)
+
+lemma eqpoll_Func_finsup_Func_finite: "finite A \<Longrightarrow> Func_finsupp z A B \<approx> Func A B"
+  by (meson bij_betw_Func_finsup_Func_finite eqpoll_def)
+
+lemma card_of_Func_finsup_finite: "finite A \<Longrightarrow> |Func_finsupp z A B| =o |B| ^c |A|"
+  using eqpoll_Func_finsup_Func_finite
+  by (metis Field_card_of cexp_def eqpoll_imp_card_of_ordIso)
+
+text \<open>
+  The cases where $A$ and $B$ are both finite or $B = \{0\}$ or $A = \emptyset$ are of course
+  trivial.
+
+  Perhaps not completely obviously, it turns out that in all other cases, the cardinality of
+  $\text{Func\_finsupp}_z(A, B)$ is exactly $\text{max}(|A|, |B|)$.
+\<close>
+theorem card_of_Func_finsupp_infinite:
+  assumes "z \<in> B" and "B - {z} \<noteq> {}" and "A \<noteq> {}"
+  assumes "infinite A \<or> infinite B"
+  shows   "|Func_finsupp z A B| =o cmax |A| |B|"
+proof -
+  have inf_cmax: "Cinfinite (cmax |A| |B| )"
+    using assms by (simp add: Card_order_cmax cinfinite_def finite_cmax)
+
+  have "bij_betw (\<lambda>f. ({x. f x \<noteq> z}, restrict f {x. f x \<noteq> z}))
+          (Func_finsupp z A B) (SIGMA X:FinPow A. Func X (B - {z}))"
+    by (rule bij_betwI[of _ _ _ "\<lambda>(X,f) x. if x \<in> -X \<union> -A then z else f x"])
+       (fastforce simp: Func_def Func_finsupp_def FinPow_def fun_eq_iff \<open>z \<in> B\<close> split: if_splits)+
+  hence "|Func_finsupp z A B| =o |SIGMA X:FinPow A. Func X (B - {z})|"
+    by (rule card_of_ordIsoI)
+
+  also have "|SIGMA X:FinPow A. Func X (B - {z})| =o cmax |A| |B|"
+  proof (rule ordLeq_antisym)
+    show "|SIGMA X:FinPow A. Func X (B - {z})| \<le>o cmax |A| |B|"
+    proof (intro card_of_Sigma_ordLeq_infinite_Field ballI)
+      show "infinite (Field (cmax |A| |B| ))"
+        using assms by (simp add: finite_cmax)
+    next
+      show "Card_order (cmax |A| |B| )"
+        by (intro Card_order_cmax) auto
+    next
+      show "|FinPow A| \<le>o cmax |A| |B|"
+      proof (cases "finite A")
+        assume "infinite A"
+        hence "|FinPow A| =o |A|"
+          by (rule card_of_FinPow_infinite)
+        also have "|A| \<le>o cmax |A| |B|"
+          by (simp add: ordLeq_cmax)
+        finally show ?thesis .
+      next
+        assume A: "finite A"
+        have "finite (FinPow A)"
+          using A by auto
+        thus "|FinPow A| \<le>o cmax |A| |B|"
+          using A by (intro Cfinite_ordLeq_Cinfinite inf_cmax) auto
+      qed
+    next
+      show "|Func X (B - {z})| \<le>o cmax |A| |B|" if "X \<in> FinPow A" for X
+      proof (cases "finite B")
+        case True
+        have "finite X"
+          using that by (auto simp: FinPow_def)
+        hence "finite (Func X (B - {z}))"
+          using True by blast
+        with inf_cmax show ?thesis
+          by (intro Cfinite_ordLeq_Cinfinite) auto
+      next
+        case False
+        have "|Func X (B - {z})| =o |B - {z}| ^c |X|"
+          by (rule card_of_Func)
+        also have "|B - {z}| ^c |X| \<le>o |B - {z}|"
+          by (rule cexp_infinite_finite_ordLeq) (use False that in \<open>auto simp: FinPow_def\<close>)
+        also have "|B - {z}| =o |B|"
+          using False by (simp add: infinite_card_of_diff_singl)
+        also have "|B| \<le>o cmax |A| |B|"
+          by (simp add: ordLeq_cmax)
+        finally show ?thesis .
+      qed
+    qed
+  next
+    have "cmax |A| |B| =o |A| *c |B - {z}|"
+    proof (cases "|A| \<le>o |B|")
+      case False
+      have "\<not>|B - {z}| =o czero"
+        using \<open>B - {z} \<noteq> {}\<close> by (subst card_of_ordIso_czero_iff_empty) auto
+      from False and assms have "infinite A"
+        using ordLeq_finite_infinite by blast
+      from False have "|B| \<le>o |A|"
+        by (simp add: ordLess_imp_ordLeq)
+      have "|B - {z}| \<le>o |B|"
+        by (rule card_of_mono1) auto
+      also note \<open>|B| \<le>o |A|\<close>
+      finally have "|A| *c |B - {z}| =o |A|"
+        using \<open>infinite A\<close> \<open>\<not>|B - {z}| =o czero\<close> by (intro cprod_infinite1') auto
+      moreover have "cmax |A| |B| =o |A|"
+        using \<open>|B| \<le>o |A|\<close> by (simp add: cmax1)
+      ultimately show ?thesis
+        using ordIso_symmetric ordIso_transitive by blast
+    next
+      case True
+      from True and assms have "infinite B"
+        using card_of_ordLeq_finite by blast
+      have "|A| *c |B - {z}| =o |A| *c |B|"
+        using \<open>infinite B\<close>  by (intro cprod_cong2) (simp add: infinite_card_of_diff_singl)
+      also have "|A| *c |B| =o |B|"
+        using True \<open>infinite B\<close> assms(3)
+        by (simp add: card_of_ordIso_czero_iff_empty cprod_infinite2')
+      also have "|B| =o cmax |A| |B|"
+        using True by (meson card_of_Card_order cmax2 ordIso_symmetric)
+      finally show ?thesis
+        using ordIso_symmetric ordIso_transitive by blast
+    qed
+    also have "|A| *c |B - {z}| =o |A \<times> (B - {z})|"
+      by (metis Field_card_of card_of_refl cprod_def)
+    also have "|A \<times> (B - {z})| \<le>o |SIGMA X:(\<lambda>x. {x})`A. B - {z}|"
+      by (intro card_of_Sigma_mono[of "\<lambda>x. {x}"]) auto
+    also have "|SIGMA X:(\<lambda>x. {x})`A. B - {z}| =o |SIGMA X:(\<lambda>x. {x})`A. Func X (B - {z})|"
+    proof (rule card_of_Sigma_cong; safe)
+      fix x assume x: "x \<in> A"
+      have "|Func {x} (B - {z})| =o |B - {z}| ^c |{x}|"
+        by (simp add: card_of_Func)
+      also have "|B - {z}| ^c |{x}| =o |B - {z}| ^c BNF_Cardinal_Arithmetic.cone"
+        by (intro cexp_cong2) (auto simp: single_cone)
+      also have "|B - {z}| ^c Wellorder_Constructions.cone =o |B - {z}|"
+        using card_of_Card_order cexp_cone by blast
+      finally show "|B - {z}| =o |Func {x} (B - {z})|"
+        using ordIso_symmetric by blast
+    qed
+    also have "|SIGMA X:(\<lambda>x. {x})`A. Func X (B - {z})| \<le>o |SIGMA X:FinPow A. Func X (B - {z})|"
+      by (rule card_of_Sigma_mono) (auto simp: FinPow_def)
+    finally show "cmax |A| |B| \<le>o |SIGMA X:FinPow A. Func X (B - {z})|" .
+  qed
+  finally show ?thesis .
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Cardinality_Continuum/Cardinality_Euclidean_Space.thy b/thys/Cardinality_Continuum/Cardinality_Euclidean_Space.thy
new file mode 100644
--- /dev/null
+++ b/thys/Cardinality_Continuum/Cardinality_Euclidean_Space.thy
@@ -0,0 +1,38 @@
+(*
+  File:     Cardinality_Continuum/Cardinality_Euclidean_Space.thy
+  Author:   Manuel Eberl (University of Innsbruck)
+
+  The cardinality of a Euclidean space.
+  This is a separate file because we need HOL-Analysis for Euclidean spaces, which is a 
+  rather hefty library to import.
+*)
+theory Cardinality_Euclidean_Space
+  imports "HOL-Analysis.Analysis" Cardinality_Continuum
+begin
+
+text \<open>
+  With these results, it is now easy to see that any Euclidean space 
+  (i.e.\ finite-dimensional real vector space) has the same cardinality as \<open>\<real>\<close>:
+\<close>
+corollary card_of_UNIV_euclidean_space:
+  "|UNIV :: 'a :: euclidean_space set| =o ctwo ^c natLeq"
+proof -
+  have "|span Basis :: 'a set| =o |UNIV :: real set|"
+    by (rule card_of_span_finite_dim_infinite_field) 
+       (simp_all add: independent_Basis infinite_UNIV_char_0)
+  also have "|UNIV :: real set| =o ctwo ^c natLeq"
+    by (rule card_of_UNIV_real)
+  finally show ?thesis
+    by simp
+qed
+
+text \<open>
+  In particular, this applies to \<open>\<complex>\<close> and $\mathbb{R}^n$:
+\<close>
+corollary card_of_complex: "|UNIV :: complex set| =o ctwo ^c natLeq"
+  by (rule card_of_UNIV_euclidean_space)
+
+corollary card_of_real_vec: "|UNIV :: (real ^ 'n :: finite) set| =o ctwo ^c natLeq"
+  by (rule card_of_UNIV_euclidean_space)
+
+end
\ No newline at end of file
diff --git a/thys/Cardinality_Continuum/ROOT b/thys/Cardinality_Continuum/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Cardinality_Continuum/ROOT
@@ -0,0 +1,12 @@
+chapter AFP
+
+session Cardinality_Continuum (AFP) = "HOL-Analysis" +
+  options [timeout = 300]
+  sessions
+    "HOL-Library"
+    "HOL-Cardinals"
+  theories
+    Cardinality_Continuum
+    Cardinality_Euclidean_Space
+  document_files
+    "root.tex"
diff --git a/thys/Cardinality_Continuum/document/root.tex b/thys/Cardinality_Continuum/document/root.tex
new file mode 100755
--- /dev/null
+++ b/thys/Cardinality_Continuum/document/root.tex
@@ -0,0 +1,37 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{amsfonts, amsmath, amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+\usepackage[shortcuts]{extdash}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{rm}
+
+
+\begin{document}
+
+\title{The Cardinality of the Continuum}
+\author{Manuel Eberl}
+\maketitle
+
+\begin{abstract}
+This entry presents a short derivation of the cardinality of $\mathbb{R}$,
+namely that $|\mathbb{R}| = |2^{\mathbb{N}}| = 2^{\aleph_0}$. This is done by showing the
+injection $\mathbb{R}\to 2^{\mathbb{Q}},\ x \mapsto (-\infty, x)\cap\mathbb{Q}$ (i.e.\ Dedekind cuts)
+for one direction and the injection $2^\mathbb{N}\to\mathbb{Q},\ X \mapsto \sum_{n\in X} 3^{-n}$,
+i.e.\ ternary fractions, for the other direction.
+\end{abstract}
+
+
+\tableofcontents
+
+\newpage
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}
+
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,785 +1,786 @@
 ABY3_Protocols
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AOT
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Balog_Szemeredi_Gowers
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binary_Code_Imprimitive
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Birkhoff_Finite_Distributive_Lattices
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Boolos_Curious_Inference_Automated
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CHERI-C_Memory_Model
 CISC-Kernel
 CRDT
 CRYSTALS-Kyber
 CSP_RefTK
 CVP_Hardness
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
+Cardinality_Continuum
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Catoids
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Ceva
 Chandy_Lamport
 Chebyshev_Polynomials
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 CommCSL
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 Cook_Levin
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 Coupledsim_Contrasim
 CryptHOL
 CryptoBasedCompositionalProperties
 Crypto_Standards
 Cubic_Quartic_Equations
 DCR-ExecutionEquivalence
 DFS_Framework
 DOM_Components
 DPRM_Theorem
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 DigitsInBase
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Directed_Sets
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 Disintegration
 DiskPaxos
 Distributed_Distinct_Elements
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Earley_Parser
 Echelon_Form
 EdmondsKarp_Maxflow
 Edwards_Elliptic_Curves_Group
 Efficient-Mergesort
 Efficient_Weighted_Path_Order
 Elimination_Of_Repeated_Factors
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Euler_Polyhedron_Formula
 Eudoxus_Reals
 Eval_FO
 Example-Submission
 Executable_Randomized_Algorithms
 Expander_Graphs
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FO_Theory_Rewriting
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Fixed_Length_Vector
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 Given_Clause_Loops
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Gray_Codes
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 HoareForDivergence
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 HyperHoareLogic
 Hyperdual
 Hypergraph_Basics
 Hypergraph_Colourings
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IO_Language_Conformance
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 IsaNet
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Kneser_Cauchy_Davenport
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LP_Duality
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lovasz_Local
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Maximum_Segment_Sum
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MHComputation
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 MLSS_Decision_Proc
 ML_Unification
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Multirelations_Heterogeneous
 Multiset_Ordering_NPC
 Multitape_To_Singletape_TM
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 No_FTL_observers_Gen_Rel
 Nominal2
 Nominal_Myhill_Nerode
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PAPP_Impossibility
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Package_logic
 Padic_Field
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect_Fields
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polygonal_Number_Theorem
 Polylog
 Polynomial_Crit_Geometry
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Probability_Inequality_Completeness
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Logic_Class
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 Q0_Metatheory
 QHLProver
 QR_Decomposition
 Quantales
 Quantales_Converse
 Quantifier_Elimination_Hybrid
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Cardinality
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rensets
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SCC_Bloemen_Sequential
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 S_Finite_Measure_Monad
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 Sauer_Shelah_Lemma
 Schutz_Spacetime
 Schwartz_Zippel
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Clause_Learning
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Solidity
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 Standard_Borel_Spaces
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 StrictOmegaCategories
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Suppes_Theorem
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Synthetic_Completeness
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Three_Squares
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 TsirelsonBound
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Transport
 Treaps
 Tree-Automata
 Tree_Decomposition
 Tree_Enumeration
 Triangle
 Trie
 Turans_Graph_Theorem
 Twelvefold_Way
 Two_Generated_Word_Monoids_Intersection
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 VYDRA_MDL
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeckendorf
 Zeta_3_Irrational
 Zeta_Function
 pGCL
 Labeled_Transition_Systems
 Pushdown_Systems