author huffman Mon, 15 Aug 2011 15:11:55 -0700 changeset 44216 903bfe95fece parent 44215 786876687ef8 child 44217 5cdad94bdc29
generalized lemma closed_Collect_eq
```--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 14:50:24 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 15:11:55 2011 -0700
@@ -5182,19 +5182,27 @@
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::real_normed_vector"
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
(* FIXME: generalize 'a to topological_space *)
-  (* FIXME: generalize 'b to t2_space *)
assumes f: "\<And>x. continuous (at x) f"
assumes g: "\<And>x. continuous (at x) g"
shows "closed {x. f x = g x}"
proof -
-  have "closed ((\<lambda>x. g x - f x) -` {0})"
-    using continuous_sub [OF g f] closed_singleton
+  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]
+  have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
by (rule continuous_closed_vimage [rule_format])
-  also have "((\<lambda>x. g x - f x) -` {0}) = {x. f x = g x}"
-    by auto
+  also have "\<dots> = {x. f x = g x}" by auto
finally show ?thesis .
qed
```