author | hoelzl |
Wed, 06 Jan 2016 12:18:53 +0100 | |
changeset 62083 | 7582b39f51ed |
parent 61975 | b4b11391c676 |
child 63040 | eb4ddd18d635 |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: HOL/Library/ContNotDenum.thy |
56796 | 2 |
Author: Benjamin Porter, Monash University, NICTA, 2005 |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
3 |
Author: Johannes Hölzl, TU München |
23461 | 4 |
*) |
5 |
||
60500 | 6 |
section \<open>Non-denumerability of the Continuum.\<close> |
23461 | 7 |
|
8 |
theory ContNotDenum |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
9 |
imports Complex_Main Countable_Set |
23461 | 10 |
begin |
11 |
||
60500 | 12 |
subsection \<open>Abstract\<close> |
23461 | 13 |
|
60500 | 14 |
text \<open>The following document presents a proof that the Continuum is |
23461 | 15 |
uncountable. It is formalised in the Isabelle/Isar theorem proving |
16 |
system. |
|
17 |
||
61585 | 18 |
{\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other |
19 |
words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is |
|
23461 | 20 |
surjective. |
21 |
||
22 |
{\em Outline:} An elegant informal proof of this result uses Cantor's |
|
23 |
Diagonalisation argument. The proof presented here is not this |
|
24 |
one. First we formalise some properties of closed intervals, then we |
|
25 |
prove the Nested Interval Property. This property relies on the |
|
26 |
completeness of the Real numbers and is the foundation for our |
|
27 |
argument. Informally it states that an intersection of countable |
|
28 |
closed intervals (where each successive interval is a subset of the |
|
61585 | 29 |
last) is non-empty. We then assume a surjective function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f |
60500 | 30 |
by generating a sequence of closed intervals then using the NIP.\<close> |
23461 | 31 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
32 |
theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
33 |
proof |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
34 |
assume "\<exists>f::nat \<Rightarrow> real. surj f" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
35 |
then obtain f :: "nat \<Rightarrow> real" where "surj f" .. |
56796 | 36 |
|
60500 | 37 |
txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close> |
23461 | 38 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
39 |
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})" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
40 |
using assms |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
41 |
by (auto simp add: not_le cong: conj_cong) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
42 |
(metis dense le_less_linear less_linear less_trans order_refl) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
43 |
then obtain i j where ij: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
44 |
"\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
45 |
"\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
46 |
"\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
47 |
by metis |
23461 | 48 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
49 |
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)))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
50 |
def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}" |
23461 | 51 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
52 |
have ivl[simp]: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
53 |
"ivl 0 = (f 0 + 1, f 0 + 2)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
54 |
"\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
55 |
unfolding ivl_def by simp_all |
56796 | 56 |
|
60500 | 57 |
txt \<open>This is a decreasing sequence of non-empty intervals.\<close> |
23461 | 58 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
59 |
{ fix n have "fst (ivl n) < snd (ivl n)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
60 |
by (induct n) (auto intro!: ij) } |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
61 |
note less = this |
23461 | 62 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
63 |
have "decseq I" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
64 |
unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
65 |
|
60500 | 66 |
txt \<open>Now we apply the finite intersection property of compact sets.\<close> |
23461 | 67 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
68 |
have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
69 |
proof (rule compact_imp_fip_image) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
70 |
fix S :: "nat set" assume fin: "finite S" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
71 |
have "{} \<subset> I (Max (insert 0 S))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
72 |
unfolding I_def using less[of "Max (insert 0 S)"] by auto |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
73 |
also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)" |
60500 | 74 |
using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff) |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
75 |
also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)" |
56796 | 76 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
77 |
finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}" |
53372 | 78 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
79 |
qed (auto simp: I_def) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
80 |
then obtain x where "\<And>n. x \<in> I n" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
81 |
by blast |
60500 | 82 |
moreover from \<open>surj f\<close> obtain j where "x = f j" |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
83 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
84 |
ultimately have "f j \<in> I (Suc j)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
85 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
86 |
with ij(3)[OF less] show False |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
87 |
unfolding I_def ivl fst_conv snd_conv by auto |
23461 | 88 |
qed |
89 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
90 |
lemma uncountable_UNIV_real: "uncountable (UNIV::real set)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
91 |
using real_non_denum unfolding uncountable_def by auto |
23461 | 92 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
93 |
lemma bij_betw_open_intervals: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
94 |
fixes a b c d :: real |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
95 |
assumes "a < b" "c < d" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
96 |
shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
97 |
proof - |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
98 |
def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
99 |
{ fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
100 |
moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
101 |
by (intro mult_strict_left_mono) simp_all |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
102 |
moreover from * have "0 < (d - c) * (x - a) / (b - a)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
103 |
by simp |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
104 |
ultimately have "f a b c d x < d" "c < f a b c d x" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
105 |
by (simp_all add: f_def field_simps) } |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
106 |
with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
107 |
by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
108 |
thus ?thesis by auto |
23461 | 109 |
qed |
110 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
111 |
lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV" |
59872
db4000b71fdb
Theorem "arctan" is no longer a default simprule
paulson <lp15@cam.ac.uk>
parents:
59720
diff
changeset
|
112 |
using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan) |
23461 | 113 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
114 |
lemma uncountable_open_interval: |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
115 |
fixes a b :: real |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
116 |
shows "uncountable {a<..<b} \<longleftrightarrow> a < b" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
117 |
proof |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
118 |
assume "uncountable {a<..<b}" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
119 |
then show "a < b" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
120 |
using uncountable_def by force |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
121 |
next |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
122 |
assume "a < b" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
123 |
show "uncountable {a<..<b}" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
124 |
proof - |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
125 |
obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}" |
60500 | 126 |
using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
127 |
then show ?thesis |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
128 |
by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real) |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
129 |
qed |
23461 | 130 |
qed |
131 |
||
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
132 |
lemma uncountable_half_open_interval_1: |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
133 |
fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
134 |
apply auto |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
135 |
using atLeastLessThan_empty_iff apply fastforce |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
136 |
using uncountable_open_interval [of a b] |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
137 |
by (metis countable_Un_iff ivl_disj_un_singleton(3)) |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
138 |
|
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
139 |
lemma uncountable_half_open_interval_2: |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
140 |
fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b" |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
141 |
apply auto |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
142 |
using atLeastLessThan_empty_iff apply fastforce |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
143 |
using uncountable_open_interval [of a b] |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
144 |
by (metis countable_Un_iff ivl_disj_un_singleton(4)) |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
145 |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
146 |
lemma real_interval_avoid_countable_set: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
147 |
fixes a b :: real and A :: "real set" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
148 |
assumes "a < b" and "countable A" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
149 |
shows "\<exists>x\<in>{a<..<b}. x \<notin> A" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
150 |
proof - |
61975 | 151 |
from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto |
152 |
moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}" |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
153 |
by (simp add: uncountable_open_interval) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
154 |
ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
155 |
hence "A \<inter> {a<..<b} \<subset> {a<..<b}" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
156 |
by (intro psubsetI, auto) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
157 |
hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
158 |
by (rule psubset_imp_ex_mem) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
159 |
thus ?thesis by auto |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
160 |
qed |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
161 |
|
62083 | 162 |
lemma open_minus_countable: |
163 |
fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S" |
|
164 |
shows "\<exists>x\<in>S. x \<notin> A" |
|
165 |
proof - |
|
166 |
obtain x where "x \<in> S" |
|
167 |
using \<open>S \<noteq> {}\<close> by auto |
|
168 |
then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S" |
|
169 |
using \<open>open S\<close> by (auto simp: open_dist subset_eq) |
|
170 |
moreover have "{y. dist y x < e} = {x - e <..< x + e}" |
|
171 |
by (auto simp: dist_real_def) |
|
172 |
ultimately have "uncountable (S - A)" |
|
173 |
using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close> |
|
174 |
by (intro uncountable_minus_countable) (auto dest: countable_subset) |
|
175 |
then show ?thesis |
|
176 |
unfolding uncountable_def by auto |
|
177 |
qed |
|
178 |
||
23461 | 179 |
end |