author himmelma Thu, 28 May 2009 17:03:14 +0200 changeset 31282 b98cbfabe824 parent 31281 b4d4dbc5b04f child 31283 86093a969bcd
Moved some lemmas about intervals to Topology
```--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 16:19:34 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 17:03:14 2009 +0200
@@ -3791,11 +3791,11 @@
unfolding continuous_on_def apply (simp del: dist_sym) unfolding dist_vec1 unfolding dist_def ..

lemma continuous_at_vec1_norm:
- "\<forall>x. continuous (at x) (vec1 o norm)"
+ "continuous (at x) (vec1 o norm)"
unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast

lemma continuous_on_vec1_norm:
- "\<forall>s. continuous_on s (vec1 o norm)"
+ "continuous_on s (vec1 o norm)"
unfolding continuous_on_vec1_range norm_vec1[THEN sym] by (metis norm_vec1 order_le_less_trans real_abs_sub_norm)

lemma continuous_at_vec1_component:
@@ -3860,7 +3860,7 @@

lemma continuous_attains_inf:
"compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s (vec1 o f)
-        ==> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
+        \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
using compact_attains_inf[of "f ` s"]
using compact_continuous_image[of s "vec1 \<circ> f"] unfolding image_compose by auto

@@ -4299,8 +4299,12 @@
lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows
"x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a\$i < x\$i \<and> x\$i < b\$i)"
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a\$i \<le> x\$i \<and> x\$i \<le> b\$i)"
-  using interval[of a b]
-  by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+  using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+
+lemma mem_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
+ "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)

lemma interval_eq_empty: fixes a :: "real^'n::finite" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b\$i \<le> a\$i))" (is ?th1) and
@@ -4357,7 +4361,6 @@
apply (auto simp add: not_less less_imp_le)
done

-
lemma interval_open_subset_closed:  fixes a :: "'a::preorder^'n::finite" shows
"{a<..<b} \<subseteq> {a .. b}"