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"