# HG changeset patch
# User huffman
# Date 1244759593 25200
# Node ID 0fb78b3a914532011f879804ac4069bbaafe6c27
# Parent  eff95000aae74d0b9ad2abf6ff4ebd458508cf59
new lemmas

diff -r eff95000aae7 -r 0fb78b3a9145 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Jun 11 12:05:41 2009 -0700
+++ b/src/HOL/RealVector.thy	Thu Jun 11 15:33:13 2009 -0700
@@ -828,6 +828,21 @@
   thus "open {a<..<b}" by (simp add: open_Int)
 qed
 
+lemma closed_real_atMost [simp]: 
+  fixes a :: real shows "closed {..a}"
+unfolding closed_open by simp
+
+lemma closed_real_atLeast [simp]:
+  fixes a :: real shows "closed {a..}"
+unfolding closed_open by simp
+
+lemma closed_real_atLeastAtMost [simp]:
+  fixes a b :: real shows "closed {a..b}"
+proof -
+  have "{a..b} = {a..} \<inter> {..b}" by auto
+  thus "closed {a..b}" by (simp add: closed_Int)
+qed
+
 
 subsection {* Extra type constraints *}