equal
deleted
inserted
replaced
141 apply auto |
141 apply auto |
142 using atLeastLessThan_empty_iff apply fastforce |
142 using atLeastLessThan_empty_iff apply fastforce |
143 using uncountable_open_interval [of a b] |
143 using uncountable_open_interval [of a b] |
144 by (metis countable_Un_iff ivl_disj_un_singleton(4)) |
144 by (metis countable_Un_iff ivl_disj_un_singleton(4)) |
145 |
145 |
|
146 lemma real_interval_avoid_countable_set: |
|
147 fixes a b :: real and A :: "real set" |
|
148 assumes "a < b" and "countable A" |
|
149 shows "\<exists>x\<in>{a<..<b}. x \<notin> A" |
|
150 proof - |
|
151 from `countable A` have "countable (A \<inter> {a<..<b})" by auto |
|
152 moreover with `a < b` have "\<not> countable {a<..<b}" |
|
153 by (simp add: uncountable_open_interval) |
|
154 ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto |
|
155 hence "A \<inter> {a<..<b} \<subset> {a<..<b}" |
|
156 by (intro psubsetI, auto) |
|
157 hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}" |
|
158 by (rule psubset_imp_ex_mem) |
|
159 thus ?thesis by auto |
|
160 qed |
|
161 |
146 end |
162 end |