# HG changeset patch
# User huffman
# Date 1313458536 25200
# Node ID f738e3200e24672f59f607fbecf7d21903b98557
# Parent  f0e442e248160c7e29c0514788d6f2144c8e7f01
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space

diff -r f0e442e24816 -r f738e3200e24 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 16:48:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 18:35:36 2011 -0700
@@ -1101,8 +1101,7 @@
 
 lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
   unfolding Collect_all_eq
-  by (intro closed_INT ballI closed_Collect_le continuous_const
-    continuous_at_component)
+  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
 
 lemma Lim_component_cart:
   fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
@@ -1289,14 +1288,12 @@
 lemma closed_interval_left_cart: fixes b::"real^'n"
   shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
   unfolding Collect_all_eq
-  by (intro closed_INT ballI closed_Collect_le continuous_const
-    continuous_at_component)
+  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
 
 lemma closed_interval_right_cart: fixes a::"real^'n"
   shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
   unfolding Collect_all_eq
-  by (intro closed_INT ballI closed_Collect_le continuous_const
-    continuous_at_component)
+  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
 
 lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
@@ -1304,19 +1301,19 @@
 
 lemma closed_halfspace_component_le_cart:
   shows "closed {x::real^'n. x$i \<le> a}"
-  by (intro closed_Collect_le continuous_at_component continuous_const)
+  by (intro closed_Collect_le vec_nth.isCont isCont_const)
 
 lemma closed_halfspace_component_ge_cart:
   shows "closed {x::real^'n. x$i \<ge> a}"
-  by (intro closed_Collect_le continuous_at_component continuous_const)
+  by (intro closed_Collect_le vec_nth.isCont isCont_const)
 
 lemma open_halfspace_component_lt_cart:
   shows "open {x::real^'n. x$i < a}"
-  by (intro open_Collect_less continuous_at_component continuous_const)
+  by (intro open_Collect_less vec_nth.isCont isCont_const)
 
 lemma open_halfspace_component_gt_cart:
   shows "open {x::real^'n. x$i  > a}"
-  by (intro open_Collect_less continuous_at_component continuous_const)
+  by (intro open_Collect_less vec_nth.isCont isCont_const)
 
 lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
   assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$i \<le> b) net"
@@ -1355,8 +1352,8 @@
 proof-
   { fix i::'n
     have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
-      by (cases "P i", simp_all, intro closed_Collect_eq
-        continuous_at_component continuous_const) }
+      by (cases "P i", simp_all,
+        intro closed_Collect_eq vec_nth.isCont isCont_const) }
   thus ?thesis
     unfolding Collect_all_eq by (simp add: closed_INT)
 qed
diff -r f0e442e24816 -r f738e3200e24 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 16:48:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 18:35:36 2011 -0700
@@ -5152,56 +5152,63 @@
 
 subsection {* Closure of halfspaces and hyperplanes *}
 
+lemma isCont_open_vimage:
+  assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
+proof -
+  from assms(1) have "continuous_on UNIV f"
+    unfolding isCont_def continuous_on_def within_UNIV by simp
+  hence "open {x \<in> UNIV. f x \<in> s}"
+    using open_UNIV `open s` by (rule continuous_open_preimage)
+  thus "open (f -` s)"
+    by (simp add: vimage_def)
+qed
+
+lemma isCont_closed_vimage:
+  assumes "\<And>x. isCont f x" and "closed s" shows "closed (f -` s)"
+  using assms unfolding closed_def vimage_Compl [symmetric]
+  by (rule isCont_open_vimage)
+
 lemma open_Collect_less:
-  fixes f g :: "'a::t2_space \<Rightarrow> real"
-  (* FIXME: generalize to topological_space *)
-  assumes f: "\<And>x. continuous (at x) f"
-  assumes g: "\<And>x. continuous (at x) g"
+  fixes f g :: "'a::topological_space \<Rightarrow> real"
+  assumes f: "\<And>x. isCont f x"
+  assumes g: "\<And>x. isCont g x"
   shows "open {x. f x < g x}"
 proof -
   have "open ((\<lambda>x. g x - f x) -` {0<..})"
-    using continuous_sub [OF g f] open_real_greaterThan
-    by (rule continuous_open_vimage [rule_format])
+    using isCont_diff [OF g f] open_real_greaterThan
+    by (rule isCont_open_vimage)
   also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
     by auto
   finally show ?thesis .
 qed
 
 lemma closed_Collect_le:
-  fixes f g :: "'a::t2_space \<Rightarrow> real"
-  (* FIXME: generalize to topological_space *)
-  assumes f: "\<And>x. continuous (at x) f"
-  assumes g: "\<And>x. continuous (at x) g"
+  fixes f g :: "'a::topological_space \<Rightarrow> real"
+  assumes f: "\<And>x. isCont f x"
+  assumes g: "\<And>x. isCont g x"
   shows "closed {x. f x \<le> g x}"
 proof -
   have "closed ((\<lambda>x. g x - f x) -` {0..})"
-    using continuous_sub [OF g f] closed_real_atLeast
-    by (rule continuous_closed_vimage [rule_format])
+    using isCont_diff [OF g f] closed_real_atLeast
+    by (rule isCont_closed_vimage)
   also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
     by auto
   finally show ?thesis .
 qed
 
-lemma continuous_at_Pair: (* TODO: move *)
-  assumes f: "continuous (at x) f"
-  assumes g: "continuous (at x) g"
-  shows "continuous (at x) (\<lambda>x. (f x, g x))"
-  using assms unfolding continuous_at by (rule tendsto_Pair)
-
 lemma closed_Collect_eq:
-  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
-  (* FIXME: generalize 'a to topological_space *)
-  assumes f: "\<And>x. continuous (at x) f"
-  assumes g: "\<And>x. continuous (at x) g"
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+  assumes f: "\<And>x. isCont f x"
+  assumes g: "\<And>x. isCont g x"
   shows "closed {x. f x = g x}"
 proof -
   have "open {(x::'b, y::'b). x \<noteq> y}"
     unfolding open_prod_def by (auto dest!: hausdorff)
   hence "closed {(x::'b, y::'b). x = y}"
     unfolding closed_def split_def Collect_neg_eq .
-  with continuous_at_Pair [OF f g]
+  with isCont_Pair [OF f g]
   have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
-    by (rule continuous_closed_vimage [rule_format])
+    by (rule isCont_closed_vimage)
   also have "\<dots> = {x. f x = g x}" by auto
   finally show ?thesis .
 qed
@@ -5222,41 +5229,37 @@
   unfolding continuous_on by (rule ballI) (intro tendsto_intros)
 
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
-  by (intro closed_Collect_le continuous_at_inner continuous_const)
+  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
 
 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
-  by (intro closed_Collect_le continuous_at_inner continuous_const)
+  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
 
 lemma closed_hyperplane: "closed {x. inner a x = b}"
-  by (intro closed_Collect_eq continuous_at_inner continuous_const)
+  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
 
 lemma closed_halfspace_component_le:
   shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
-  by (intro closed_Collect_le continuous_at_euclidean_component
-    continuous_const)
+  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
 
 lemma closed_halfspace_component_ge:
   shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
-  by (intro closed_Collect_le continuous_at_euclidean_component
-    continuous_const)
+  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
 
 text {* Openness of halfspaces. *}
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
-  by (intro open_Collect_less continuous_at_inner continuous_const)
+  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
 
 lemma open_halfspace_gt: "open {x. inner a x > b}"
-  by (intro open_Collect_less continuous_at_inner continuous_const)
+  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
 
 lemma open_halfspace_component_lt:
   shows "open {x::'a::euclidean_space. x$$i < a}"
-  by (intro open_Collect_less continuous_at_euclidean_component
-    continuous_const)
+  by (intro open_Collect_less euclidean_component.isCont isCont_const)
 
 lemma open_halfspace_component_gt:
-  shows "open {x::'a::euclidean_space. x$$i  > a}"
-  by (intro open_Collect_less continuous_at_euclidean_component
-    continuous_const)
+  shows "open {x::'a::euclidean_space. x$$i > a}"
+  by (intro open_Collect_less euclidean_component.isCont isCont_const)
 
 text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
 
@@ -5295,14 +5298,14 @@
   shows "closed {.. a}"
   unfolding eucl_atMost_eq_halfspaces
   by (intro closed_INT ballI closed_Collect_le
-    continuous_at_euclidean_component continuous_const)
+    euclidean_component.isCont isCont_const)
 
 lemma closed_eucl_atLeast[simp, intro]:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
   shows "closed {a ..}"
   unfolding eucl_atLeast_eq_halfspaces
   by (intro closed_INT ballI closed_Collect_le
-    continuous_at_euclidean_component continuous_const)
+    euclidean_component.isCont isCont_const)
 
 lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
   by (auto intro!: continuous_open_vimage)