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.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.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 -