src/HOL/Library/ContNotDenum.thy
changeset 60308 f7e406aba90d
parent 59872 db4000b71fdb
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Thu May 28 14:33:35 2015 +0100
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Fri May 29 14:35:59 2015 +0100
     1.3 @@ -113,14 +113,35 @@
     1.4    using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
     1.5  
     1.6  lemma uncountable_open_interval:
     1.7 -  fixes a b :: real assumes ab: "a < b"
     1.8 -  shows "uncountable {a<..<b}"
     1.9 -proof -
    1.10 -  obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
    1.11 -    using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
    1.12 -  then show ?thesis
    1.13 -    by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
    1.14 +  fixes a b :: real 
    1.15 +  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
    1.16 +proof
    1.17 +  assume "uncountable {a<..<b}"
    1.18 +  then show "a < b"
    1.19 +    using uncountable_def by force
    1.20 +next 
    1.21 +  assume "a < b"
    1.22 +  show "uncountable {a<..<b}"
    1.23 +  proof -
    1.24 +    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
    1.25 +      using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
    1.26 +    then show ?thesis
    1.27 +      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
    1.28 +  qed
    1.29  qed
    1.30  
    1.31 +lemma uncountable_half_open_interval_1:
    1.32 +  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
    1.33 +  apply auto
    1.34 +  using atLeastLessThan_empty_iff apply fastforce
    1.35 +  using uncountable_open_interval [of a b]
    1.36 +  by (metis countable_Un_iff ivl_disj_un_singleton(3))
    1.37 +
    1.38 +lemma uncountable_half_open_interval_2:
    1.39 +  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
    1.40 +  apply auto
    1.41 +  using atLeastLessThan_empty_iff apply fastforce
    1.42 +  using uncountable_open_interval [of a b]
    1.43 +  by (metis countable_Un_iff ivl_disj_un_singleton(4))
    1.44 +
    1.45  end
    1.46 -