author huffman Mon Aug 15 15:11:55 2011 -0700 (2011-08-15) changeset 44216 903bfe95fece parent 44215 786876687ef8 child 44217 5cdad94bdc29
generalized lemma closed_Collect_eq
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 14:50:24 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 15:11:55 2011 -0700
1.3 @@ -5182,19 +5182,27 @@
1.4    finally show ?thesis .
1.5  qed
1.6
1.7 +lemma continuous_at_Pair: (* TODO: move *)
1.8 +  assumes f: "continuous (at x) f"
1.9 +  assumes g: "continuous (at x) g"
1.10 +  shows "continuous (at x) (\<lambda>x. (f x, g x))"
1.11 +  using assms unfolding continuous_at by (rule tendsto_Pair)
1.12 +
1.13  lemma closed_Collect_eq:
1.14 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.15 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
1.16    (* FIXME: generalize 'a to topological_space *)
1.17 -  (* FIXME: generalize 'b to t2_space *)
1.18    assumes f: "\<And>x. continuous (at x) f"
1.19    assumes g: "\<And>x. continuous (at x) g"
1.20    shows "closed {x. f x = g x}"
1.21  proof -
1.22 -  have "closed ((\<lambda>x. g x - f x) -` {0})"
1.23 -    using continuous_sub [OF g f] closed_singleton
1.24 +  have "open {(x::'b, y::'b). x \<noteq> y}"
1.25 +    unfolding open_prod_def by (auto dest!: hausdorff)
1.26 +  hence "closed {(x::'b, y::'b). x = y}"
1.27 +    unfolding closed_def split_def Collect_neg_eq .
1.28 +  with continuous_at_Pair [OF f g]
1.29 +  have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
1.30      by (rule continuous_closed_vimage [rule_format])
1.31 -  also have "((\<lambda>x. g x - f x) -` {0}) = {x. f x = g x}"
1.32 -    by auto
1.33 +  also have "\<dots> = {x. f x = g x}" by auto
1.34    finally show ?thesis .
1.35  qed
1.36
```