src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 50949 a5689bb4ed7e parent 50948 8c742f9de9f5 child 50955 ada575c605e1
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 19:28:48 2013 -0800
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 20:26:38 2013 -0800
1.3 @@ -5427,24 +5427,54 @@
1.4  qed
1.5
1.6  lemma separate_compact_closed:
1.7 -  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
1.8 -    (* TODO: does this generalize to heine_borel? *)
1.9 +  fixes s t :: "'a::heine_borel set"
1.10    assumes "compact s" and "closed t" and "s \<inter> t = {}"
1.11    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
1.12 -proof-
1.13 -  have "0 \<notin> {x - y |x y. x \<in> s \<and> y \<in> t}" using assms(3) by auto
1.14 -  then obtain d where "d>0" and d:"\<forall>x\<in>{x - y |x y. x \<in> s \<and> y \<in> t}. d \<le> dist 0 x"
1.15 -    using separate_point_closed[OF compact_closed_differences[OF assms(1,2)], of 0] by auto
1.16 -  { fix x y assume "x\<in>s" "y\<in>t"
1.17 -    hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
1.18 -    hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
1.19 -      by (auto  simp add: dist_commute)
1.20 -    hence "d \<le> dist x y" unfolding dist_norm by auto  }
1.21 -  thus ?thesis using `d>0` by auto
1.22 +proof - (* FIXME: long proof *)
1.23 +  let ?T = "\<Union>x\<in>s. { ball x (d / 2) | d. 0 < d \<and> (\<forall>y\<in>t. d \<le> dist x y) }"
1.24 +  note `compact s`
1.25 +  moreover have "\<forall>t\<in>?T. open t" by auto
1.26 +  moreover have "s \<subseteq> \<Union>?T"
1.27 +    apply auto
1.28 +    apply (rule rev_bexI, assumption)
1.29 +    apply (subgoal_tac "x \<notin> t")
1.30 +    apply (drule separate_point_closed [OF `closed t`])
1.31 +    apply clarify
1.32 +    apply (rule_tac x="ball x (d / 2)" in exI)
1.33 +    apply simp
1.34 +    apply fast
1.35 +    apply (cut_tac assms(3))
1.36 +    apply auto
1.37 +    done
1.38 +  ultimately obtain U where "U \<subseteq> ?T" and "finite U" and "s \<subseteq> \<Union>U"
1.39 +    by (rule compactE)
1.40 +  from `finite U` and `U \<subseteq> ?T` have "\<exists>d>0. \<forall>x\<in>\<Union>U. \<forall>y\<in>t. d \<le> dist x y"
1.41 +    apply (induct set: finite)
1.42 +    apply simp
1.43 +    apply (rule exI)
1.44 +    apply (rule zero_less_one)
1.45 +    apply clarsimp
1.46 +    apply (rename_tac y e)
1.47 +    apply (rule_tac x="min d (e / 2)" in exI)
1.48 +    apply simp
1.49 +    apply (subst ball_Un)
1.50 +    apply (rule conjI)
1.51 +    apply (intro ballI, rename_tac z)
1.52 +    apply (rule min_max.le_infI2)
1.53 +    apply (simp only: mem_ball)
1.54 +    apply (drule (1) bspec)
1.55 +    apply (cut_tac x=y and y=x and z=z in dist_triangle, arith)
1.56 +    apply simp
1.57 +    apply (intro ballI)
1.58 +    apply (rule min_max.le_infI1)
1.59 +    apply simp
1.60 +    done
1.61 +  with `s \<subseteq> \<Union>U` show ?thesis
1.62 +    by fast
1.63  qed
1.64
1.65  lemma separate_closed_compact:
1.66 -  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
1.67 +  fixes s t :: "'a::heine_borel set"
1.68    assumes "closed s" and "compact t" and "s \<inter> t = {}"
1.69    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
1.70  proof-
```