summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Tue, 05 Mar 2013 15:43:17 +0100 | |

changeset 51346 | d33de22432e2 |

parent 51345 | e7dd577cb053 |

child 51347 | f8a00792fbc1 |

tuned proofs (used continuity of infdist, dist and continuous_attains_sup)

src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:16 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:17 2013 +0100 @@ -4974,7 +4974,7 @@ by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) lemma distance_attains_sup: assumes "compact s" "s \<noteq> {}" - shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x" + shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x" proof (rule continuous_attains_sup [OF assms]) { fix x assume "x\<in>s" have "(dist a ---> dist a x) (at x within s)" @@ -4989,34 +4989,17 @@ lemma distance_attains_inf: fixes a :: "'a::heine_borel" assumes "closed s" "s \<noteq> {}" - shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a x \<le> dist a y" + shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a x \<le> dist a y" proof- - from assms(2) obtain b where "b\<in>s" by auto - let ?B = "cball a (dist b a) \<inter> s" - have "b \<in> ?B" using `b\<in>s` by (simp add: dist_commute) - hence "?B \<noteq> {}" by auto - moreover - { fix x assume "x\<in>?B" - fix e::real assume "e>0" - { fix x' assume "x'\<in>?B" and as:"dist x' x < e" - from as have "\<bar>dist a x' - dist a x\<bar> < e" - unfolding abs_less_iff minus_diff_eq - using dist_triangle2 [of a x' x] - using dist_triangle [of a x x'] - by arith - } - hence "\<exists>d>0. \<forall>x'\<in>?B. dist x' x < d \<longrightarrow> \<bar>dist a x' - dist a x\<bar> < e" - using `e>0` by auto - } - hence "continuous_on (cball a (dist b a) \<inter> s) (dist a)" - unfolding continuous_on Lim_within dist_norm real_norm_def - by fast + from assms(2) obtain b where "b \<in> s" by auto + let ?B = "s \<inter> cball a (dist b a)" + have "?B \<noteq> {}" using `b \<in> s` by (auto simp add: dist_commute) + moreover have "continuous_on ?B (dist a)" + by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const) moreover have "compact ?B" - using compact_cball[of a "dist b a"] - unfolding compact_eq_bounded_closed - using bounded_Int and closed_Int and assms(1) by auto - ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y" - using continuous_attains_inf[of ?B "dist a"] by fastforce + by (intro closed_inter_compact `closed s` compact_cball) + ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y" + by (metis continuous_attains_inf) thus ?thesis by fastforce qed @@ -5334,50 +5317,23 @@ lemma separate_compact_closed: fixes s t :: "'a::heine_borel set" - assumes "compact s" and "closed t" and "s \<inter> t = {}" + assumes "compact s" and t: "closed t" "s \<inter> t = {}" shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y" -proof - (* FIXME: long proof *) - let ?T = "\<Union>x\<in>s. { ball x (d / 2) | d. 0 < d \<and> (\<forall>y\<in>t. d \<le> dist x y) }" - note `compact s` - moreover have "\<forall>t\<in>?T. open t" by auto - moreover have "s \<subseteq> \<Union>?T" - apply auto - apply (rule rev_bexI, assumption) - apply (subgoal_tac "x \<notin> t") - apply (drule separate_point_closed [OF `closed t`]) - apply clarify - apply (rule_tac x="ball x (d / 2)" in exI) - apply simp - apply fast - apply (cut_tac assms(3)) - apply auto - done - ultimately obtain U where "U \<subseteq> ?T" and "finite U" and "s \<subseteq> \<Union>U" - by (rule compactE) - 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" - apply (induct set: finite) - apply simp - apply (rule exI) - apply (rule zero_less_one) - apply clarsimp - apply (rename_tac y e) - apply (rule_tac x="min d (e / 2)" in exI) - apply simp - apply (subst ball_Un) - apply (rule conjI) - apply (intro ballI, rename_tac z) - apply (rule min_max.le_infI2) - apply (simp only: mem_ball) - apply (drule (1) bspec) - apply (cut_tac x=y and y=x and z=z in dist_triangle, arith) - apply simp - apply (intro ballI) - apply (rule min_max.le_infI1) - apply simp - done - with `s \<subseteq> \<Union>U` show ?thesis - by fast -qed +proof cases + assume "s \<noteq> {} \<and> t \<noteq> {}" + then have "s \<noteq> {}" "t \<noteq> {}" by auto + let ?inf = "\<lambda>x. infdist x t" + have "continuous_on s ?inf" + by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id) + then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y" + using continuous_attains_inf[OF `compact s` `s \<noteq> {}`] by auto + then have "0 < ?inf x" + using t `t \<noteq> {}` in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg) + moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y" + using x by (auto intro: order_trans infdist_le) + ultimately show ?thesis + by auto +qed (auto intro!: exI[of _ 1]) lemma separate_closed_compact: fixes s t :: "'a::heine_borel set"