summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/ContNotDenum.thy

changeset 61880 | ff4d33058566 |

parent 61585 | a9599d3d7610 |

child 61975 | b4b11391c676 |

1.1 --- a/src/HOL/Library/ContNotDenum.thy Sun Dec 20 13:56:02 2015 +0100 1.2 +++ b/src/HOL/Library/ContNotDenum.thy Thu Dec 17 16:43:36 2015 +0100 1.3 @@ -143,4 +143,20 @@ 1.4 using uncountable_open_interval [of a b] 1.5 by (metis countable_Un_iff ivl_disj_un_singleton(4)) 1.6 1.7 +lemma real_interval_avoid_countable_set: 1.8 + fixes a b :: real and A :: "real set" 1.9 + assumes "a < b" and "countable A" 1.10 + shows "\<exists>x\<in>{a<..<b}. x \<notin> A" 1.11 +proof - 1.12 + from `countable A` have "countable (A \<inter> {a<..<b})" by auto 1.13 + moreover with `a < b` have "\<not> countable {a<..<b}" 1.14 + by (simp add: uncountable_open_interval) 1.15 + ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto 1.16 + hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 1.17 + by (intro psubsetI, auto) 1.18 + hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}" 1.19 + by (rule psubset_imp_ex_mem) 1.20 + thus ?thesis by auto 1.21 +qed 1.22 + 1.23 end