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