author huffman Mon, 08 Jun 2009 19:45:24 -0700 changeset 31535 f5bde0d3c385 parent 31534 0de814d2ff95 child 31536 d1b7f1f682ce
generalize compact/closure lemmas
```--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 19:18:47 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 19:45:24 2009 -0700
@@ -3941,11 +3941,18 @@
thus ?thesis unfolding Lim_at by auto
qed

+lemma bounded_linear_continuous_at:
+  assumes "bounded_linear f"  shows "continuous (at a) f"
+  unfolding continuous_at using assms
+  apply (rule bounded_linear.tendsto)
+  apply (rule Lim_at_id [unfolded id_def])
+  done
+
lemma linear_continuous_at:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
assumes "linear f"  shows "continuous (at a) f"
-  unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms]
-  unfolding Lim_null[of "\<lambda>x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto
+  using assms unfolding linear_conv_bounded_linear
+  by (rule bounded_linear_continuous_at)

lemma linear_continuous_within:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
@@ -4276,24 +4283,25 @@

text{* Hence some useful properties follow quite easily.                         *}

+lemma compact_scaleR_image:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
+proof-
+  let ?f = "\<lambda>x. scaleR c x"
+  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
+  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
+    using bounded_linear_continuous_at[OF *] assms by auto
+qed
+
lemma compact_scaling:
fixes s :: "(real ^ _) set"
assumes "compact s"  shows "compact ((\<lambda>x. c *s x) ` s)"
-proof-
-  let ?f = "\<lambda>x. c *s x"
-  have *:"linear ?f" unfolding linear_def vector_smult_assoc vector_add_ldistrib real_mult_commute by auto
-  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
-    using linear_continuous_at[OF *] assms by auto
-qed
+  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)

lemma compact_negations:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
-proof-
-  have "(\<lambda>x. - x) ` s = (\<lambda>x. (- 1) *s x) ` s"
-    unfolding vector_sneg_minus1 ..
-  thus ?thesis using compact_scaling[OF assms, of "-1"] by auto
-qed
+  using compact_scaleR_image [OF assms, of "- 1"] by auto

lemma compact_sums:
fixes s t :: "(real ^ _) set"
@@ -4401,9 +4409,9 @@

text{* Related results with closure as the conclusion.                           *}

-lemma closed_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
+lemma closed_scaleR_image:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
proof(cases "s={}")
case True thus ?thesis by auto
next
@@ -4414,29 +4422,39 @@
case True thus ?thesis apply auto unfolding * using closed_sing by auto
next
case False
-    { fix x l assume as:"\<forall>n::nat. x n \<in> op *s c ` s"  "(x ---> l) sequentially"
-      { fix n::nat have "(1 / c) *s x n \<in> s" using as(1)[THEN spec[where x=n]] using `c\<noteq>0` by (auto simp add: vector_smult_assoc) }
+    { fix x l assume as:"\<forall>n::nat. x n \<in> scaleR c ` s"  "(x ---> l) sequentially"
+      { fix n::nat have "scaleR (1 / c) (x n) \<in> s"
+          using as(1)[THEN spec[where x=n]]
+          using `c\<noteq>0` by (auto simp add: vector_smult_assoc)
+      }
moreover
{ fix e::real assume "e>0"
hence "0 < e *\<bar>c\<bar>"  using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
-	then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>" using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
-	hence "\<exists>N. \<forall>n\<ge>N. dist ((1 / c) *s x n) ((1 / c) *s l) < e" unfolding dist_norm unfolding vector_ssub_ldistrib[THEN sym] norm_mul
+	then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
+          using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
+	hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
+          unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR
using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
-      hence "((\<lambda>n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto
-      ultimately have "l \<in> op *s c ` s"  using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. (1/c) *s x n"], THEN spec[where x="(1/c) *s l"]]
-	unfolding image_iff using `c\<noteq>0` apply(rule_tac x="(1 / c) *s l" in bexI) apply auto unfolding vector_smult_assoc  by auto  }
-    thus ?thesis unfolding closed_sequential_limits by auto
+      hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
+      ultimately have "l \<in> scaleR c ` s"
+        using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]]
+	unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto  }
+    thus ?thesis unfolding closed_sequential_limits by fast
qed
qed

+lemma closed_scaling:
+  fixes s :: "(real ^ _) set"
+  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
+  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
+
lemma closed_negations:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes s :: "'a::real_normed_vector set"
assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaling[OF assms, of "- 1"]
-  unfolding vector_sneg_minus1 by auto
+  using closed_scaleR_image[OF assms, of "- 1"] by simp

lemma compact_closed_sums:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
assumes "compact s"  "closed t"  shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
proof-
let ?S = "{x + y |x y. x \<in> s \<and> y \<in> t}"
@@ -4452,11 +4470,11 @@
using f(3) by auto
hence "l \<in> ?S" using `l' \<in> s` apply auto apply(rule_tac x=l' in exI) apply(rule_tac x="l - l'" in exI) by auto
}
-  thus ?thesis unfolding closed_sequential_limits by auto
+  thus ?thesis unfolding closed_sequential_limits by fast
qed

lemma closed_compact_sums:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
assumes "closed s"  "compact t"
shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
proof-
@@ -4466,7 +4484,7 @@
qed

lemma compact_closed_differences:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
assumes "compact s"  "closed t"
shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
proof-
@@ -4476,7 +4494,7 @@
qed

lemma closed_compact_differences:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
assumes "closed s" "compact t"
shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
proof-
@@ -4486,7 +4504,7 @@
qed

lemma closed_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
assumes "closed s"  shows "closed ((\<lambda>x. a + x) ` s)"
proof-
have "{a + y |y. y \<in> s} = (op + a ` s)" by auto
@@ -4494,21 +4512,26 @@
qed

lemma translation_UNIV:
- "range (\<lambda>x::real^'a. a + x) = UNIV"
+  fixes a :: "'a::ab_group_add" shows "range (\<lambda>x. a + x) = UNIV"
apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto

-lemma translation_diff: "(\<lambda>x::real^'a. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" by auto
+lemma translation_diff:
+  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
+  by auto

lemma closure_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
proof-
-  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"  apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
-  show ?thesis unfolding closure_interior translation_diff translation_UNIV using interior_translation[of a "UNIV - s"] unfolding * by auto
+  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"
+    apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
+  show ?thesis unfolding closure_interior translation_diff translation_UNIV
+    using interior_translation[of a "UNIV - s"] unfolding * by auto
qed

lemma frontier_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
unfolding frontier_def translation_diff interior_translation closure_translation by auto
```