generalized lemma closed_Collect_eq
authorhuffman
Mon Aug 15 15:11:55 2011 -0700 (2011-08-15)
changeset 44216903bfe95fece
parent 44215 786876687ef8
child 44217 5cdad94bdc29
generalized lemma closed_Collect_eq
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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