move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 5147933db4b7189af
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
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     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 +