author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51479 33db4b7189af parent 51478 270b21f3ae0a child 51480 3793c3a11378
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
```     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -566,30 +566,65 @@
1.4  done
1.5
1.6
1.7 +lemma compact_Icc[simp, intro]: "compact {a .. b::real}"
1.8 +proof (cases "a \<le> b", rule compactI)
1.9 +  fix C assume C: "a \<le> b" "\<forall>t\<in>C. open t" "{a..b} \<subseteq> \<Union>C"
1.10 +  def T == "{a .. b}"
1.11 +  from C(1,3) show "\<exists>C'\<subseteq>C. finite C' \<and> {a..b} \<subseteq> \<Union>C'"
1.12 +  proof (induct rule: Bolzano)
1.13 +    case (trans a b c)
1.14 +    then have *: "{a .. c} = {a .. b} \<union> {b .. c}" by auto
1.15 +    from trans obtain C1 C2 where "C1\<subseteq>C \<and> finite C1 \<and> {a..b} \<subseteq> \<Union>C1" "C2\<subseteq>C \<and> finite C2 \<and> {b..c} \<subseteq> \<Union>C2"
1.16 +      by (auto simp: *)
1.17 +    with trans show ?case
1.18 +      unfolding * by (intro exI[of _ "C1 \<union> C2"]) auto
1.19 +  next
1.20 +    case (local x)
1.21 +    then have "x \<in> \<Union>C" using C by auto
1.22 +    with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
1.23 +    then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
1.24 +      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
1.25 +    with `c \<in> C` show ?case
1.26 +      by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
1.27 +  qed
1.28 +qed simp
1.29 +
1.30  subsection {* Boundedness of continuous functions *}
1.31
1.32  text{*By bisection, function continuous on closed interval is bounded above*}
1.33
1.34 +lemma isCont_eq_Ub:
1.35 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
1.36 +  shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
1.37 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
1.38 +  using continuous_attains_sup[of "{a .. b}" f]
1.39 +  apply (simp add: continuous_at_imp_continuous_on Ball_def)
1.40 +  apply safe
1.41 +  apply (rule_tac x="f x" in exI)
1.42 +  apply auto
1.43 +  done
1.44 +
1.45 +lemma isCont_eq_Lb:
1.46 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
1.47 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
1.48 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
1.49 +  using continuous_attains_inf[of "{a .. b}" f]
1.50 +  apply (simp add: continuous_at_imp_continuous_on Ball_def)
1.51 +  apply safe
1.52 +  apply (rule_tac x="f x" in exI)
1.53 +  apply auto
1.54 +  done
1.55 +
1.56  lemma isCont_bounded:
1.57 -     "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.58 -      ==> \<exists>M::real. \<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M"
1.59 -apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
1.60 -apply safe
1.61 -apply simp_all
1.62 -apply (rename_tac x xa ya M Ma)
1.63 -apply (metis linorder_not_less order_le_less order_trans)
1.64 -apply (case_tac "a \<le> x & x \<le> b")
1.65 - prefer 2
1.66 - apply (rule_tac x = 1 in exI, force)
1.67 -apply (simp add: LIM_eq isCont_iff)
1.68 -apply (drule_tac x = x in spec, auto)
1.69 -apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
1.70 -apply (drule_tac x = 1 in spec, auto)
1.71 -apply (rule_tac x = s in exI, clarify)
1.72 -apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
1.73 -apply (drule_tac x = "xa-x" in spec)
1.74 -apply (auto simp add: abs_ge_self)
1.75 -done
1.76 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
1.77 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> \<exists>M. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
1.78 +  using isCont_eq_Ub[of a b f] by auto
1.79 +
1.80 +lemma isCont_has_Ub:
1.81 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
1.82 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
1.83 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
1.84 +  using isCont_eq_Ub[of a b f] by auto
1.85
1.86  text{*Refine the above to existence of least upper bound*}
1.87
1.88 @@ -597,72 +632,6 @@
1.89        (\<exists>t. isLub UNIV S t)"
1.90  by (blast intro: reals_complete)
1.91
1.92 -lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.93 -         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M) &
1.94 -                   (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
1.95 -apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
1.96 -        in lemma_reals_complete)
1.97 -apply auto
1.98 -apply (drule isCont_bounded, assumption)
1.99 -apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
1.100 -apply (rule exI, auto)
1.101 -apply (auto dest!: spec simp add: linorder_not_less)
1.102 -done
1.103 -
1.104 -text{*Now show that it attains its upper bound*}
1.105 -
1.106 -lemma isCont_eq_Ub:
1.107 -  assumes le: "a \<le> b"
1.108 -      and con: "\<forall>x::real. a \<le> x & x \<le> b --> isCont f x"
1.109 -  shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
1.110 -             (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
1.111 -proof -
1.112 -  from isCont_has_Ub [OF le con]
1.113 -  obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
1.114 -             and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x"  by blast
1.115 -  show ?thesis
1.116 -  proof (intro exI, intro conjI)
1.117 -    show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
1.118 -    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M"
1.119 -    proof (rule ccontr)
1.120 -      assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
1.121 -      with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
1.122 -        by (fastforce simp add: linorder_not_le [symmetric])
1.123 -      hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
1.124 -        by (auto simp add: con)
1.125 -      from isCont_bounded [OF le this]
1.126 -      obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
1.127 -      have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
1.128 -        by (simp add: M3 algebra_simps)
1.129 -      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
1.130 -        by (auto intro: order_le_less_trans [of _ k])
1.131 -      with Minv
1.132 -      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))"
1.133 -        by (intro strip less_imp_inverse_less, simp_all)
1.134 -      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x"
1.135 -        by simp
1.136 -      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le
1.137 -        by (simp, arith)
1.138 -      from M2 [OF this]
1.139 -      obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
1.140 -      thus False using invlt [of x] by force
1.141 -    qed
1.142 -  qed
1.143 -qed
1.144 -
1.145 -
1.146 -text{*Same theorem for lower bound*}
1.147 -
1.148 -lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.149 -         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> M \<le> f(x)) &
1.150 -                   (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
1.151 -apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
1.152 -prefer 2 apply (blast intro: isCont_minus)
1.153 -apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub)
1.154 -apply safe
1.155 -apply auto
1.156 -done
1.157 -
1.158
1.159  text{*Another version.*}
1.160
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
2.3 @@ -2362,28 +2362,6 @@
2.4
2.5  subsection {* Compactness *}
2.6
2.7 -subsubsection{* Open-cover compactness *}
2.8 -
2.9 -definition compact :: "'a::topological_space set \<Rightarrow> bool" where
2.10 -  compact_eq_heine_borel: -- "This name is used for backwards compatibility"
2.11 -    "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
2.12 -
2.13 -lemma compactI:
2.14 -  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
2.15 -  shows "compact s"
2.16 -  unfolding compact_eq_heine_borel using assms by metis
2.17 -
2.18 -lemma compactE:
2.19 -  assumes "compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C"
2.20 -  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
2.21 -  using assms unfolding compact_eq_heine_borel by metis
2.22 -
2.23 -lemma compactE_image:
2.24 -  assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
2.25 -  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
2.26 -  using assms unfolding ball_simps[symmetric] SUP_def
2.27 -  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
2.28 -
2.29  subsubsection {* Bolzano-Weierstrass property *}
2.30
2.31  lemma heine_borel_imp_bolzano_weierstrass:
2.32 @@ -2621,11 +2599,6 @@
2.33
2.34  text{* In particular, some common special cases. *}
2.35
2.36 -lemma compact_empty[simp]:
2.37 - "compact {}"
2.38 -  unfolding compact_eq_heine_borel
2.39 -  by auto
2.40 -
2.41  lemma compact_union [intro]:
2.42    assumes "compact s" "compact t" shows " compact (s \<union> t)"
2.43  proof (rule compactI)
2.44 @@ -4523,40 +4496,6 @@
2.45    qed
2.46  qed
2.47
2.48 -lemma compact_continuous_image:
2.49 -  assumes "continuous_on s f" and "compact s"
2.50 -  shows "compact (f ` s)"
2.51 -using assms (* FIXME: long unstructured proof *)
2.52 -unfolding continuous_on_open
2.53 -unfolding compact_eq_openin_cover
2.54 -apply clarify
2.55 -apply (drule_tac x="image (\<lambda>t. {x \<in> s. f x \<in> t}) C" in spec)
2.56 -apply (drule mp)
2.57 -apply (rule conjI)
2.58 -apply simp
2.59 -apply clarsimp
2.60 -apply (drule subsetD)
2.61 -apply (erule imageI)
2.62 -apply fast
2.63 -apply (erule thin_rl)
2.64 -apply clarify
2.65 -apply (rule_tac x="image (inv_into C (\<lambda>t. {x \<in> s. f x \<in> t})) D" in exI)
2.66 -apply (intro conjI)
2.67 -apply clarify
2.68 -apply (rule inv_into_into)
2.69 -apply (erule (1) subsetD)
2.70 -apply (erule finite_imageI)
2.71 -apply (clarsimp, rename_tac x)
2.72 -apply (drule (1) subsetD, clarify)
2.73 -apply (drule (1) subsetD, clarify)
2.74 -apply (rule rev_bexI)
2.75 -apply assumption
2.76 -apply (subgoal_tac "{x \<in> s. f x \<in> t} \<in> (\<lambda>t. {x \<in> s. f x \<in> t}) ` C")
2.77 -apply (drule f_inv_into_f)
2.78 -apply fast
2.79 -apply (erule imageI)
2.80 -done
2.81 -
2.82  lemma connected_continuous_image:
2.83    assumes "continuous_on s f"  "connected s"
2.84    shows "connected(f ` s)"
2.85 @@ -4710,56 +4649,6 @@
2.86    shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
2.87    unfolding continuous_on_iff dist_norm by simp
2.88
2.89 -lemma compact_attains_sup:
2.90 -  fixes S :: "'a::linorder_topology set"
2.91 -  assumes "compact S" "S \<noteq> {}"
2.92 -  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
2.93 -proof (rule classical)
2.94 -  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
2.95 -  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
2.96 -    by (metis not_le)
2.97 -  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
2.98 -    by auto
2.99 -  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
2.100 -    by (erule compactE_image)
2.101 -  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
2.102 -    by (auto intro!: Max_in)
2.103 -  with C have "S \<subseteq> {..< Max (t`C)}"
2.104 -    by (auto intro: less_le_trans simp: subset_eq)
2.105 -  with t Max `C \<subseteq> S` show ?thesis
2.106 -    by fastforce
2.107 -qed
2.108 -
2.109 -lemma compact_attains_inf:
2.110 -  fixes S :: "'a::linorder_topology set"
2.111 -  assumes "compact S" "S \<noteq> {}"
2.112 -  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
2.113 -proof (rule classical)
2.114 -  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
2.115 -  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
2.116 -    by (metis not_le)
2.117 -  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
2.118 -    by auto
2.119 -  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
2.120 -    by (erule compactE_image)
2.121 -  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
2.122 -    by (auto intro!: Min_in)
2.123 -  with C have "S \<subseteq> {Min (t`C) <..}"
2.124 -    by (auto intro: le_less_trans simp: subset_eq)
2.125 -  with t Min `C \<subseteq> S` show ?thesis
2.126 -    by fastforce
2.127 -qed
2.128 -
2.129 -lemma continuous_attains_sup:
2.130 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
2.131 -  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
2.132 -  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
2.133 -
2.134 -lemma continuous_attains_inf:
2.135 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
2.136 -  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
2.137 -  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
2.138 -
2.139  text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
2.140
2.141  lemma distance_attains_sup:
```
```     3.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
3.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
3.3 @@ -1780,5 +1780,98 @@
3.4    "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
3.5    using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
3.6
3.7 +subsubsection{* Open-cover compactness *}
3.8 +
3.9 +context topological_space
3.10 +begin
3.11 +
3.12 +definition compact :: "'a set \<Rightarrow> bool" where
3.13 +  compact_eq_heine_borel: -- "This name is used for backwards compatibility"
3.14 +    "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
3.15 +
3.16 +lemma compactI:
3.17 +  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
3.18 +  shows "compact s"
3.19 +  unfolding compact_eq_heine_borel using assms by metis
3.20 +
3.21 +lemma compact_empty[simp]: "compact {}"
3.22 +  by (auto intro!: compactI)
3.23 +
3.24 +lemma compactE:
3.25 +  assumes "compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C"
3.26 +  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
3.27 +  using assms unfolding compact_eq_heine_borel by metis
3.28 +
3.29 +lemma compactE_image:
3.30 +  assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
3.31 +  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
3.32 +  using assms unfolding ball_simps[symmetric] SUP_def
3.33 +  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
3.34 +
3.35  end
3.36
3.37 +lemma (in linorder_topology) compact_attains_sup:
3.38 +  assumes "compact S" "S \<noteq> {}"
3.39 +  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
3.40 +proof (rule classical)
3.41 +  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
3.42 +  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
3.43 +    by (metis not_le)
3.44 +  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
3.45 +    by auto
3.46 +  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
3.47 +    by (erule compactE_image)
3.48 +  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
3.49 +    by (auto intro!: Max_in)
3.50 +  with C have "S \<subseteq> {..< Max (t`C)}"
3.51 +    by (auto intro: less_le_trans simp: subset_eq)
3.52 +  with t Max `C \<subseteq> S` show ?thesis
3.53 +    by fastforce
3.54 +qed
3.55 +
3.56 +lemma (in linorder_topology) compact_attains_inf:
3.57 +  assumes "compact S" "S \<noteq> {}"
3.58 +  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
3.59 +proof (rule classical)
3.60 +  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
3.61 +  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
3.62 +    by (metis not_le)
3.63 +  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
3.64 +    by auto
3.65 +  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
3.66 +    by (erule compactE_image)
3.67 +  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
3.68 +    by (auto intro!: Min_in)
3.69 +  with C have "S \<subseteq> {Min (t`C) <..}"
3.70 +    by (auto intro: le_less_trans simp: subset_eq)
3.71 +  with t Min `C \<subseteq> S` show ?thesis
3.72 +    by fastforce
3.73 +qed
3.74 +
3.75 +lemma compact_continuous_image:
3.76 +  assumes f: "continuous_on s f" and s: "compact s"
3.77 +  shows "compact (f ` s)"
3.78 +proof (rule compactI)
3.79 +  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
3.80 +  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
3.81 +    unfolding continuous_on_open_invariant by blast
3.82 +  then guess A unfolding bchoice_iff .. note A = this
3.83 +  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
3.84 +    by (fastforce simp add: subset_eq set_eq_iff)+
3.85 +  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
3.86 +  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
3.87 +    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
3.88 +qed
3.89 +
3.90 +lemma continuous_attains_sup:
3.91 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
3.92 +  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
3.93 +  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
3.94 +
3.95 +lemma continuous_attains_inf:
3.96 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
3.97 +  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
3.98 +  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
3.99 +
3.100 +end
3.101 +
```