diff -r b3d246c92dfb -r e7dd577cb053 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:15 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:16 2013 +0100 @@ -4915,59 +4915,63 @@ shows "continuous_on s f \ (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d --> abs(f x' - f x) < e))" unfolding continuous_on_iff dist_norm by simp +lemma compact_attains_sup: + fixes S :: "'a::linorder_topology set" + assumes "compact S" "S \ {}" + shows "\s\S. \t\S. t \ s" +proof (rule classical) + assume "\ (\s\S. \t\S. t \ s)" + then obtain t where t: "\s\S. t s \ S" and "\s\S. s < t s" + by (metis not_le) + then have "\s\S. open {..< t s}" "S \ (\s\S. {..< t s})" + by auto + with `compact S` obtain C where "C \ S" "finite C" and C: "S \ (\s\C. {..< t s})" + by (erule compactE_image) + with `S \ {}` have Max: "Max (t`C) \ t`C" and "\s\t`C. s \ Max (t`C)" + by (auto intro!: Max_in) + with C have "S \ {..< Max (t`C)}" + by (auto intro: less_le_trans simp: subset_eq) + with t Max `C \ S` show ?thesis + by fastforce +qed + +lemma compact_attains_inf: + fixes S :: "'a::linorder_topology set" + assumes "compact S" "S \ {}" + shows "\s\S. \t\S. s \ t" +proof (rule classical) + assume "\ (\s\S. \t\S. s \ t)" + then obtain t where t: "\s\S. t s \ S" and "\s\S. t s < s" + by (metis not_le) + then have "\s\S. open {t s <..}" "S \ (\s\S. {t s <..})" + by auto + with `compact S` obtain C where "C \ S" "finite C" and C: "S \ (\s\C. {t s <..})" + by (erule compactE_image) + with `S \ {}` have Min: "Min (t`C) \ t`C" and "\s\t`C. Min (t`C) \ s" + by (auto intro!: Min_in) + with C have "S \ {Min (t`C) <..}" + by (auto intro: le_less_trans simp: subset_eq) + with t Min `C \ S` show ?thesis + by fastforce +qed + +lemma continuous_attains_sup: + fixes f :: "'a::topological_space \ 'b::linorder_topology" + shows "compact s \ s \ {} \ continuous_on s f \ (\x\s. \y\s. f y \ f x)" + using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto + +lemma continuous_attains_inf: + fixes f :: "'a::topological_space \ 'b::linorder_topology" + shows "compact s \ s \ {} \ continuous_on s f \ (\x\s. \y\s. f x \ f y)" + using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto + text {* Hence some handy theorems on distance, diameter etc. of/from a set. *} -lemma compact_attains_sup: - fixes s :: "real set" - assumes "compact s" "s \ {}" - shows "\x \ s. \y \ s. y \ x" -proof- - from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ Sup s" "Sup s \ s" "0 < e" "\x'\s. x' = Sup s \ \ Sup s - x' < e" - have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto - moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto - ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto } - thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]] - apply(rule_tac x="Sup s" in bexI) by auto -qed lemma Inf: fixes S :: "real set" shows "S \ {} ==> (\b. b <=* S) ==> isGlb UNIV S (Inf S)" by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) - -lemma compact_attains_inf: - fixes s :: "real set" - assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. x \ y" -proof- - from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ Inf s" "Inf s \ s" "0 < e" - "\x'\s. x' = Inf s \ \ abs (x' - Inf s) < e" - have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto - moreover - { fix x assume "x \ s" - hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto - have "Inf s + e \ x" using as(4)[THEN bspec[where x=x]] using as(2) `x\s` unfolding * by auto } - hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto - ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto } - thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]] - apply(rule_tac x="Inf s" in bexI) by auto -qed - -lemma continuous_attains_sup: - fixes f :: "'a::topological_space \ real" - shows "compact s \ s \ {} \ continuous_on s f - ==> (\x \ s. \y \ s. f y \ f x)" - using compact_attains_sup[of "f ` s"] - using compact_continuous_image[of s f] by auto - -lemma continuous_attains_inf: - fixes f :: "'a::topological_space \ real" - shows "compact s \ s \ {} \ continuous_on s f - \ (\x \ s. \y \ s. f x \ f y)" - using compact_attains_inf[of "f ` s"] - using compact_continuous_image[of s f] by auto - lemma distance_attains_sup: assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. dist a y \ dist a x"