clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
authorhoelzl
Wed Jun 11 13:39:38 2014 +0200 (2014-06-11)
changeset 57234596a499318ab
parent 57233 8fcbfce2a2a9
child 57235 b0b9a10e4bf4
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Countable_Set.thy
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Thu Jun 12 08:48:59 2014 +0200
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Jun 11 13:39:38 2014 +0200
     1.3 @@ -1,11 +1,12 @@
     1.4  (*  Title:      HOL/Library/ContNonDenum.thy
     1.5      Author:     Benjamin Porter, Monash University, NICTA, 2005
     1.6 +    Author:     Johannes Hölzl, TU München
     1.7  *)
     1.8  
     1.9  header {* Non-denumerability of the Continuum. *}
    1.10  
    1.11  theory ContNotDenum
    1.12 -imports Complex_Main
    1.13 +imports Complex_Main Countable_Set
    1.14  begin
    1.15  
    1.16  subsection {* Abstract *}
    1.17 @@ -29,295 +30,96 @@
    1.18  "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
    1.19  by generating a sequence of closed intervals then using the NIP. *}
    1.20  
    1.21 +theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
    1.22 +proof
    1.23 +  assume "\<exists>f::nat \<Rightarrow> real. surj f"
    1.24 +  then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    1.25  
    1.26 -subsection {* Closed Intervals *}
    1.27 -
    1.28 -subsection {* Nested Interval Property *}
    1.29 +  txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
    1.30  
    1.31 -theorem NIP:
    1.32 -  fixes f :: "nat \<Rightarrow> real set"
    1.33 -  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    1.34 -    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    1.35 -  shows "(\<Inter>n. f n) \<noteq> {}"
    1.36 -proof -
    1.37 -  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    1.38 -  {
    1.39 -    fix n
    1.40 -    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    1.41 -      by auto
    1.42 -    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    1.43 -      by auto
    1.44 -  }
    1.45 -  note f_eq = this
    1.46 -  {
    1.47 -    fix n m :: nat
    1.48 -    assume "n \<le> m"
    1.49 -    then have "f m \<subseteq> f n"
    1.50 -      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
    1.51 -  }
    1.52 -  note subset' = this
    1.53 +  have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
    1.54 +    using assms
    1.55 +    by (auto simp add: not_le cong: conj_cong)
    1.56 +       (metis dense le_less_linear less_linear less_trans order_refl)
    1.57 +  then obtain i j where ij:
    1.58 +    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
    1.59 +    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
    1.60 +    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    1.61 +    by metis
    1.62  
    1.63 -  have "compact (f 0)"
    1.64 -    by (subst f_eq) (rule compact_Icc)
    1.65 -  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
    1.66 -  proof (rule compact_imp_fip_image)
    1.67 -    fix I :: "nat set"
    1.68 -    assume I: "finite I"
    1.69 -    have "{} \<subset> f (Max (insert 0 I))"
    1.70 -      using f_eq[of "Max (insert 0 I)"] by auto
    1.71 -    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    1.72 -    proof (rule INF_greatest)
    1.73 -      fix i
    1.74 -      assume "i \<in> insert 0 I"
    1.75 -      with I show "f (Max (insert 0 I)) \<subseteq> f i"
    1.76 -        by (intro subset') auto
    1.77 -    qed
    1.78 -    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    1.79 -      by auto
    1.80 -  qed (subst f_eq, auto)
    1.81 -  then show "(\<Inter>n. f n) \<noteq> {}"
    1.82 -    by auto
    1.83 -qed
    1.84 +  def ivl \<equiv> "rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
    1.85 +  def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
    1.86  
    1.87 +  have ivl[simp]:
    1.88 +    "ivl 0 = (f 0 + 1, f 0 + 2)"
    1.89 +    "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
    1.90 +    unfolding ivl_def by simp_all
    1.91  
    1.92 -subsection {* Generating the intervals *}
    1.93 +  txt {* This is a decreasing sequence of non-empty intervals. *}
    1.94  
    1.95 -subsubsection {* Existence of non-singleton closed intervals *}
    1.96 +  { fix n have "fst (ivl n) < snd (ivl n)"
    1.97 +      by (induct n) (auto intro!: ij) }
    1.98 +  note less = this
    1.99  
   1.100 -text {* This lemma asserts that given any non-singleton closed
   1.101 -interval (a,b) and any element c, there exists a closed interval that
   1.102 -is a subset of (a,b) and that does not contain c and is a
   1.103 -non-singleton itself. *}
   1.104 +  have "decseq I"
   1.105 +    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
   1.106 +
   1.107 +  txt {* Now we apply the finite intersection property of compact sets. *}
   1.108  
   1.109 -lemma closed_subset_ex:
   1.110 -  fixes c :: real
   1.111 -  assumes "a < b"
   1.112 -  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
   1.113 -proof (cases "c < b")
   1.114 -  case True
   1.115 -  show ?thesis
   1.116 -  proof (cases "c < a")
   1.117 -    case True
   1.118 -    with `a < b` `c < b` have "c \<notin> {a..b}"
   1.119 -      by auto
   1.120 -    with `a < b` show ?thesis
   1.121 -      by auto
   1.122 -  next
   1.123 -    case False
   1.124 -    then have "a \<le> c" by simp
   1.125 -    def ka \<equiv> "(c + b)/2"
   1.126 -    from ka_def `c < b` have "ka < b"
   1.127 +  have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
   1.128 +  proof (rule compact_imp_fip_image)
   1.129 +    fix S :: "nat set" assume fin: "finite S"
   1.130 +    have "{} \<subset> I (Max (insert 0 S))"
   1.131 +      unfolding I_def using less[of "Max (insert 0 S)"] by auto
   1.132 +    also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
   1.133 +      using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
   1.134 +    also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
   1.135        by auto
   1.136 -    moreover from ka_def `c < b` have "ka > c"
   1.137 -      by simp
   1.138 -    ultimately have "c \<notin> {ka..b}"
   1.139 -      by auto
   1.140 -    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
   1.141 -      by simp
   1.142 -    then have "{ka..b} \<subseteq> {a..b}"
   1.143 -      by auto
   1.144 -    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   1.145 -      using `ka < b` by auto
   1.146 -    then show ?thesis
   1.147 +    finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
   1.148        by auto
   1.149 -  qed
   1.150 -next
   1.151 -  case False
   1.152 -  then have "c \<ge> b" by simp
   1.153 -  def kb \<equiv> "(a + b)/2"
   1.154 -  with `a < b` have "kb < b" by auto
   1.155 -  with kb_def `c \<ge> b` have "a < kb" "kb < c"
   1.156 -    by auto
   1.157 -  from `kb < c` have c: "c \<notin> {a..kb}"
   1.158 -    by auto
   1.159 -  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   1.160 -    by auto
   1.161 -  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   1.162 -    by simp
   1.163 -  then show ?thesis
   1.164 -    by auto
   1.165 +  qed (auto simp: I_def)
   1.166 +  then obtain x where "\<And>n. x \<in> I n"
   1.167 +    by blast
   1.168 +  moreover from `surj f` obtain j where "x = f j"
   1.169 +    by blast
   1.170 +  ultimately have "f j \<in> I (Suc j)"
   1.171 +    by blast
   1.172 +  with ij(3)[OF less] show False
   1.173 +    unfolding I_def ivl fst_conv snd_conv by auto
   1.174  qed
   1.175  
   1.176 -
   1.177 -subsection {* newInt: Interval generation *}
   1.178 -
   1.179 -text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   1.180 -closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   1.181 -does not contain @{text "f (Suc n)"}. With the base case defined such
   1.182 -that @{text "(f 0)\<notin>newInt 0 f"}. *}
   1.183 -
   1.184 -
   1.185 -subsubsection {* Definition *}
   1.186 -
   1.187 -primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
   1.188 -where
   1.189 -  "newInt 0 f = {f 0 + 1..f 0 + 2}"
   1.190 -| "newInt (Suc n) f =
   1.191 -    (SOME e.
   1.192 -      (\<exists>e1 e2.
   1.193 -         e1 < e2 \<and>
   1.194 -         e = {e1..e2} \<and>
   1.195 -         e \<subseteq> newInt n f \<and>
   1.196 -         f (Suc n) \<notin> e))"
   1.197 -
   1.198 -
   1.199 -subsubsection {* Properties *}
   1.200 -
   1.201 -text {* We now show that every application of newInt returns an
   1.202 -appropriate interval. *}
   1.203 -
   1.204 -lemma newInt_ex:
   1.205 -  "\<exists>a b. a < b \<and>
   1.206 -    newInt (Suc n) f = {a..b} \<and>
   1.207 -    newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.208 -    f (Suc n) \<notin> newInt (Suc n) f"
   1.209 -proof (induct n)
   1.210 -  case 0
   1.211 -  let ?e = "SOME e. \<exists>e1 e2.
   1.212 -    e1 < e2 \<and>
   1.213 -    e = {e1..e2} \<and>
   1.214 -    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.215 -    f (Suc 0) \<notin> e"
   1.216 +lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
   1.217 +  using real_non_denum unfolding uncountable_def by auto
   1.218  
   1.219 -  have "newInt (Suc 0) f = ?e" by auto
   1.220 -  moreover
   1.221 -  have "f 0 + 1 < f 0 + 2" by simp
   1.222 -  with closed_subset_ex
   1.223 -  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
   1.224 -  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
   1.225 -    by simp
   1.226 -  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   1.227 -    by (rule someI_ex)
   1.228 -  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   1.229 -      newInt (Suc 0) f = {e1..e2} \<and>
   1.230 -      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.231 -      f (Suc 0) \<notin> newInt (Suc 0) f"
   1.232 -    by simp
   1.233 -  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   1.234 -      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   1.235 -    by simp
   1.236 -next
   1.237 -  case (Suc n)
   1.238 -  then have "\<exists>a b.
   1.239 -      a < b \<and>
   1.240 -      newInt (Suc n) f = {a..b} \<and>
   1.241 -      newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.242 -      f (Suc n) \<notin> newInt (Suc n) f"
   1.243 -    by simp
   1.244 -  then obtain a and b where ab: "a < b \<and>
   1.245 -      newInt (Suc n) f = {a..b} \<and>
   1.246 -      newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.247 -      f (Suc n) \<notin> newInt (Suc n) f"
   1.248 -    by auto
   1.249 -  then have cab: "{a..b} = newInt (Suc n) f"
   1.250 -    by simp
   1.251 -
   1.252 -  let ?e = "SOME e. \<exists>e1 e2.
   1.253 -      e1 < e2 \<and>
   1.254 -      e = {e1..e2} \<and>
   1.255 -      e \<subseteq> {a..b} \<and>
   1.256 -      f (Suc (Suc n)) \<notin> e"
   1.257 -  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
   1.258 -    by auto
   1.259 -
   1.260 -  from ab have "a < b" by simp
   1.261 -  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   1.262 -    f (Suc (Suc n)) \<notin> {ka..kb}" .
   1.263 -  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.264 -      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   1.265 -    by simp
   1.266 -  then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
   1.267 -    by simp
   1.268 -  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
   1.269 -    by (rule someI_ex)
   1.270 -  with ab ni show "\<exists>ka kb. ka < kb \<and>
   1.271 -      newInt (Suc (Suc n)) f = {ka..kb} \<and>
   1.272 -      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   1.273 -      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
   1.274 -    by auto
   1.275 +lemma bij_betw_open_intervals:
   1.276 +  fixes a b c d :: real
   1.277 +  assumes "a < b" "c < d"
   1.278 +  shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
   1.279 +proof -
   1.280 +  def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
   1.281 +  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
   1.282 +    moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
   1.283 +      by (intro mult_strict_left_mono) simp_all
   1.284 +    moreover from * have "0 < (d - c) * (x - a) / (b - a)"
   1.285 +      by simp
   1.286 +    ultimately have "f a b c d x < d" "c < f a b c d x"
   1.287 +      by (simp_all add: f_def field_simps) }
   1.288 +  with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
   1.289 +    by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
   1.290 +  thus ?thesis by auto
   1.291  qed
   1.292  
   1.293 -lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
   1.294 -  using newInt_ex by auto
   1.295 -
   1.296 -
   1.297 -text {* Another fundamental property is that no element in the range
   1.298 -of f is in the intersection of all closed intervals generated by
   1.299 -newInt. *}
   1.300 +lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
   1.301 +  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
   1.302  
   1.303 -lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.304 -proof
   1.305 -  fix n :: nat
   1.306 -  have "f n \<notin> newInt n f"
   1.307 -  proof (cases n)
   1.308 -    case 0
   1.309 -    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
   1.310 -      by simp
   1.311 -    ultimately show ?thesis by simp
   1.312 -  next
   1.313 -    case (Suc m)
   1.314 -    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.315 -      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   1.316 -    then have "f (Suc m) \<notin> newInt (Suc m) f"
   1.317 -      by auto
   1.318 -    with Suc show ?thesis by simp
   1.319 -  qed
   1.320 -  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
   1.321 -qed
   1.322 -
   1.323 -lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
   1.324 +lemma uncountable_open_interval:
   1.325 +  fixes a b :: real assumes ab: "a < b"
   1.326 +  shows "uncountable {a<..<b}"
   1.327  proof -
   1.328 -  let ?g = "\<lambda>n. newInt n f"
   1.329 -  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   1.330 -  proof
   1.331 -    fix n
   1.332 -    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   1.333 -  qed
   1.334 -  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   1.335 -  proof
   1.336 -    fix n :: nat
   1.337 -    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   1.338 -    proof (cases n)
   1.339 -      case 0
   1.340 -      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.341 -        by simp
   1.342 -      then show ?thesis
   1.343 -        by blast
   1.344 -    next
   1.345 -      case (Suc m)
   1.346 -      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.347 -        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   1.348 -        by (rule newInt_ex)
   1.349 -      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
   1.350 -        by auto
   1.351 -      with Suc have "?g n = {a..b} \<and> a \<le> b"
   1.352 -        by auto
   1.353 -      then show ?thesis
   1.354 -        by blast
   1.355 -    qed
   1.356 -  qed
   1.357 -  ultimately show ?thesis by (rule NIP)
   1.358 -qed
   1.359 -
   1.360 -
   1.361 -subsection {* Final Theorem *}
   1.362 -
   1.363 -theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
   1.364 -proof
   1.365 -  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
   1.366 -  then obtain f :: "nat \<Rightarrow> real" where "surj f"
   1.367 -    by auto
   1.368 -  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
   1.369 -  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
   1.370 -    using newInt_notempty by blast
   1.371 -  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.372 -    by (rule newInt_inter)
   1.373 -  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
   1.374 -    by blast
   1.375 -  moreover from `surj f` have "x \<in> range f"
   1.376 -    by simp
   1.377 -  ultimately show False
   1.378 -    by blast
   1.379 +  obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
   1.380 +    using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
   1.381 +  then show ?thesis
   1.382 +    by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
   1.383  qed
   1.384  
   1.385  end
     2.1 --- a/src/HOL/Library/Countable_Set.thy	Thu Jun 12 08:48:59 2014 +0200
     2.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Jun 11 13:39:38 2014 +0200
     2.3 @@ -296,4 +296,23 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +subsection {* Uncountable *}
     2.8 +
     2.9 +abbreviation uncountable where
    2.10 +  "uncountable A \<equiv> \<not> countable A"
    2.11 +
    2.12 +lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
    2.13 +  by (auto intro: inj_on_inv_into simp: countable_def)
    2.14 +     (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
    2.15 +
    2.16 +lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
    2.17 +  unfolding bij_betw_def by (metis countable_image)
    2.18 +  
    2.19 +lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
    2.20 +  by (metis countable_finite)
    2.21 +  
    2.22 +lemma uncountable_minus_countable:
    2.23 +  "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
    2.24 +  using countable_Un[of B "A - B"] assms by auto
    2.25 +
    2.26  end