author paulson Fri, 29 May 2015 14:35:59 +0100 changeset 60308 f7e406aba90d parent 60307 75e1aa7a450e child 60309 72364a93bcb5
uncountability: open interval equivalences
```--- a/src/HOL/Library/ContNotDenum.thy	Thu May 28 14:33:35 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Fri May 29 14:35:59 2015 +0100
@@ -113,14 +113,35 @@
using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)

lemma uncountable_open_interval:
-  fixes a b :: real assumes ab: "a < b"
-  shows "uncountable {a<..<b}"
-proof -
-  obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
-    using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
-  then show ?thesis
-    by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
+  fixes a b :: real
+  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
+proof
+  assume "uncountable {a<..<b}"
+  then show "a < b"
+    using uncountable_def by force
+next
+  assume "a < b"
+  show "uncountable {a<..<b}"
+  proof -
+    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
+      using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
+    then show ?thesis
+      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
+  qed
qed

+lemma uncountable_half_open_interval_1:
+  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
+  apply auto
+  using atLeastLessThan_empty_iff apply fastforce
+  using uncountable_open_interval [of a b]
+  by (metis countable_Un_iff ivl_disj_un_singleton(3))
+
+lemma uncountable_half_open_interval_2:
+  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
+  apply auto
+  using atLeastLessThan_empty_iff apply fastforce
+  using uncountable_open_interval [of a b]
+  by (metis countable_Un_iff ivl_disj_un_singleton(4))
+
end
-```