use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 13:21:34 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 13:58:02 2013 +0100
1.3 @@ -17,6 +17,9 @@
1.4 Norm_Arith
1.5 begin
1.6
1.7 +lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
1.8 + using dist_triangle[of y z x] by (simp add: dist_commute)
1.9 +
1.10 (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
1.11 lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
1.12 apply (frule isGlb_isLb)
1.13 @@ -2373,25 +2376,23 @@
1.14 ultimately show False using g(2) using finite_subset by auto
1.15 qed
1.16
1.17 -lemma islimpt_range_imp_convergent_subsequence:
1.18 - fixes l :: "'a :: {t1_space, first_countable_topology}"
1.19 - assumes l: "l islimpt (range f)"
1.20 - shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
1.21 +lemma acc_point_range_imp_convergent_subsequence:
1.22 + fixes l :: "'a :: first_countable_topology"
1.23 + assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
1.24 + shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.25 proof -
1.26 - from first_countable_topology_class.countable_basis_at_decseq[of l] guess A . note A = this
1.27 + from countable_basis_at_decseq[of l] guess A . note A = this
1.28
1.29 def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
1.30 { fix n i
1.31 - have "\<exists>a. i < a \<and> f a \<in> A (Suc n) - (f ` {.. i} - {l})" (is "\<exists>a. _ \<and> _ \<in> ?A")
1.32 - apply (rule l[THEN islimptE, of "?A"])
1.33 - using A(2) apply fastforce
1.34 - using A(1)
1.35 - apply (intro open_Diff finite_imp_closed)
1.36 - apply auto
1.37 - apply (rule_tac x=x in exI)
1.38 - apply auto
1.39 - done
1.40 - then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)" by blast
1.41 + have "infinite (A (Suc n) \<inter> range f - f`{.. i})"
1.42 + using l A by auto
1.43 + then have "\<exists>x. x \<in> A (Suc n) \<inter> range f - f`{.. i}"
1.44 + unfolding ex_in_conv by (intro notI) simp
1.45 + then have "\<exists>j. f j \<in> A (Suc n) \<and> j \<notin> {.. i}"
1.46 + by auto
1.47 + then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
1.48 + by (auto simp: not_le)
1.49 then have "i < s n i" "f (s n i) \<in> A (Suc n)"
1.50 unfolding s_def by (auto intro: someI2_ex) }
1.51 note s = this
1.52 @@ -2475,6 +2476,31 @@
1.53 shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
1.54 by (simp add: islimpt_Un islimpt_finite)
1.55
1.56 +lemma islimpt_eq_acc_point:
1.57 + fixes l :: "'a :: t1_space"
1.58 + shows "l islimpt S \<longleftrightarrow> (\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S))"
1.59 +proof (safe intro!: islimptI)
1.60 + fix U assume "l islimpt S" "l \<in> U" "open U" "finite (U \<inter> S)"
1.61 + then have "l islimpt S" "l \<in> (U - (U \<inter> S - {l}))" "open (U - (U \<inter> S - {l}))"
1.62 + by (auto intro: finite_imp_closed)
1.63 + then show False
1.64 + by (rule islimptE) auto
1.65 +next
1.66 + fix T assume *: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S)" "l \<in> T" "open T"
1.67 + then have "infinite (T \<inter> S - {l})" by auto
1.68 + then have "\<exists>x. x \<in> (T \<inter> S - {l})"
1.69 + unfolding ex_in_conv by (intro notI) simp
1.70 + then show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> l"
1.71 + by auto
1.72 +qed
1.73 +
1.74 +lemma islimpt_range_imp_convergent_subsequence:
1.75 + fixes l :: "'a :: {t1_space, first_countable_topology}"
1.76 + assumes l: "l islimpt (range f)"
1.77 + shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.78 + using l unfolding islimpt_eq_acc_point
1.79 + by (rule acc_point_range_imp_convergent_subsequence)
1.80 +
1.81 lemma sequence_unique_limpt:
1.82 fixes f :: "nat \<Rightarrow> 'a::t2_space"
1.83 assumes "(f ---> l) sequentially" and "l' islimpt (range f)"
1.84 @@ -2837,6 +2863,10 @@
1.85 then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T" by auto
1.86 qed (insert countable_basis topological_basis_open[OF is_basis], auto)
1.87
1.88 +lemma countably_compact_eq_compact:
1.89 + "countably_compact U \<longleftrightarrow> compact (U :: 'a :: second_countable_topology set)"
1.90 + using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast
1.91 +
1.92 subsubsection{* Sequential compactness *}
1.93
1.94 definition
1.95 @@ -2937,12 +2967,6 @@
1.96 using `x \<in> U` by (auto simp: convergent_def comp_def)
1.97 qed
1.98
1.99 -lemma seq_compact_eq_compact:
1.100 - fixes U :: "'a :: second_countable_topology set"
1.101 - shows "seq_compact U \<longleftrightarrow> compact U"
1.102 - using compact_imp_seq_compact seq_compact_imp_countably_compact countably_compact_imp_compact_second_countable
1.103 - by blast
1.104 -
1.105 lemma seq_compactI:
1.106 assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially"
1.107 shows "seq_compact S"
1.108 @@ -2953,13 +2977,45 @@
1.109 obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
1.110 using assms unfolding seq_compact_def by fast
1.111
1.112 -lemma bolzano_weierstrass_imp_seq_compact:
1.113 - fixes s :: "'a::{t1_space, first_countable_topology} set"
1.114 - assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
1.115 +lemma countably_compact_imp_acc_point:
1.116 + assumes "countably_compact s" "countable t" "infinite t" "t \<subseteq> s"
1.117 + shows "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)"
1.118 +proof (rule ccontr)
1.119 + def C \<equiv> "(\<lambda>F. interior (F \<union> (- t))) ` {F. finite F \<and> F \<subseteq> t }"
1.120 + note `countably_compact s`
1.121 + moreover have "\<forall>t\<in>C. open t"
1.122 + by (auto simp: C_def)
1.123 + moreover
1.124 + assume "\<not> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
1.125 + then have s: "\<And>x. x \<in> s \<Longrightarrow> \<exists>U. x\<in>U \<and> open U \<and> finite (U \<inter> t)" by metis
1.126 + have "s \<subseteq> \<Union>C"
1.127 + using `t \<subseteq> s`
1.128 + unfolding C_def Union_image_eq
1.129 + apply (safe dest!: s)
1.130 + apply (rule_tac a="U \<inter> t" in UN_I)
1.131 + apply (auto intro!: interiorI simp add: finite_subset)
1.132 + done
1.133 + moreover
1.134 + from `countable t` have "countable C"
1.135 + unfolding C_def by (auto intro: countable_Collect_finite_subset)
1.136 + ultimately guess D by (rule countably_compactE)
1.137 + then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E" and
1.138 + s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
1.139 + by (metis (lifting) Union_image_eq finite_subset_image C_def)
1.140 + from s `t \<subseteq> s` have "t \<subseteq> \<Union>E"
1.141 + using interior_subset by blast
1.142 + moreover have "finite (\<Union>E)"
1.143 + using E by auto
1.144 + ultimately show False using `infinite t` by (auto simp: finite_subset)
1.145 +qed
1.146 +
1.147 +lemma countable_acc_point_imp_seq_compact:
1.148 + fixes s :: "'a::first_countable_topology set"
1.149 + assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
1.150 shows "seq_compact s"
1.151 proof -
1.152 { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
1.153 - have "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.154 + have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
1.155 proof (cases "finite (range f)")
1.156 case True
1.157 obtain l where "infinite {n. f n = f l}"
1.158 @@ -2972,17 +3028,44 @@
1.159 by auto
1.160 next
1.161 case False
1.162 - with f assms have "\<exists>x\<in>s. x islimpt (range f)" by auto
1.163 - then obtain l where "l \<in> s" "l islimpt (range f)" ..
1.164 - have "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.165 - using `l islimpt (range f)`
1.166 - by (rule islimpt_range_imp_convergent_subsequence)
1.167 - with `l \<in> s` show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" ..
1.168 + with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" by auto
1.169 + then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
1.170 + from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
1.171 + using acc_point_range_imp_convergent_subsequence[of l f] by auto
1.172 + with `l \<in> s` show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" ..
1.173 qed
1.174 }
1.175 thus ?thesis unfolding seq_compact_def by auto
1.176 qed
1.177
1.178 +lemma seq_compact_eq_countably_compact:
1.179 + fixes U :: "'a :: first_countable_topology set"
1.180 + shows "seq_compact U \<longleftrightarrow> countably_compact U"
1.181 + using
1.182 + countable_acc_point_imp_seq_compact
1.183 + countably_compact_imp_acc_point
1.184 + seq_compact_imp_countably_compact
1.185 + by metis
1.186 +
1.187 +lemma seq_compact_eq_acc_point:
1.188 + fixes s :: "'a :: first_countable_topology set"
1.189 + shows "seq_compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)))"
1.190 + using
1.191 + countable_acc_point_imp_seq_compact[of s]
1.192 + countably_compact_imp_acc_point[of s]
1.193 + seq_compact_imp_countably_compact[of s]
1.194 + by metis
1.195 +
1.196 +lemma seq_compact_eq_compact:
1.197 + fixes U :: "'a :: second_countable_topology set"
1.198 + shows "seq_compact U \<longleftrightarrow> compact U"
1.199 + using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
1.200 +
1.201 +lemma bolzano_weierstrass_imp_seq_compact:
1.202 + fixes s :: "'a::{t1_space, first_countable_topology} set"
1.203 + shows "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
1.204 + by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
1.205 +
1.206 subsubsection{* Total boundedness *}
1.207
1.208 lemma cauchy_def:
1.209 @@ -3024,69 +3107,38 @@
1.210
1.211 text {* Following Burkill \& Burkill vol. 2. *}
1.212
1.213 -lemma heine_borel_lemma: fixes s::"'a::metric_space set"
1.214 - assumes "seq_compact s" "s \<subseteq> (\<Union> t)" "\<forall>b \<in> t. open b"
1.215 - shows "\<exists>e>0. \<forall>x \<in> s. \<exists>b \<in> t. ball x e \<subseteq> b"
1.216 -proof(rule ccontr)
1.217 - assume "\<not> (\<exists>e>0. \<forall>x\<in>s. \<exists>b\<in>t. ball x e \<subseteq> b)"
1.218 - hence cont:"\<forall>e>0. \<exists>x\<in>s. \<forall>xa\<in>t. \<not> (ball x e \<subseteq> xa)" by auto
1.219 - { fix n::nat
1.220 - have "1 / real (n + 1) > 0" by auto
1.221 - hence "\<exists>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> (ball x (inverse (real (n+1))) \<subseteq> xa))" using cont unfolding Bex_def by auto }
1.222 - hence "\<forall>n::nat. \<exists>x. x \<in> s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)" by auto
1.223 - then obtain f where f:"\<forall>n::nat. f n \<in> s \<and> (\<forall>xa\<in>t. \<not> ball (f n) (inverse (real (n + 1))) \<subseteq> xa)"
1.224 - using choice[of "\<lambda>n::nat. \<lambda>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)"] by auto
1.225 -
1.226 - then obtain l r where l:"l\<in>s" and r:"subseq r" and lr:"((f \<circ> r) ---> l) sequentially"
1.227 - using assms(1)[unfolded seq_compact_def, THEN spec[where x=f]] by auto
1.228 -
1.229 - obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
1.230 - then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
1.231 - using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
1.232 -
1.233 - then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
1.234 - using lr[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
1.235 -
1.236 - obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
1.237 - have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
1.238 - apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
1.239 - using seq_suble[OF r, of "N1 + N2"] by auto
1.240 -
1.241 - def x \<equiv> "(f (r (N1 + N2)))"
1.242 - have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
1.243 - using f[THEN spec[where x="r (N1 + N2)"]] using `b\<in>t` by auto
1.244 - have "\<exists>y\<in>ball x (inverse (real (r (N1 + N2) + 1))). y\<notin>b" apply(rule ccontr) using x by auto
1.245 - then obtain y where y:"y \<in> ball x (inverse (real (r (N1 + N2) + 1)))" "y \<notin> b" by auto
1.246 -
1.247 - have "dist x l < e/2" using N1 unfolding x_def o_def by auto
1.248 - hence "dist y l < e" using y N2' using dist_triangle[of y l x]by (auto simp add:dist_commute)
1.249 -
1.250 - thus False using e and `y\<notin>b` by auto
1.251 -qed
1.252 -
1.253 lemma seq_compact_imp_heine_borel:
1.254 fixes s :: "'a :: metric_space set"
1.255 - shows "seq_compact s \<Longrightarrow> compact s"
1.256 - unfolding compact_eq_heine_borel
1.257 -proof clarify
1.258 - fix f assume "seq_compact s" " \<forall>t\<in>f. open t" "s \<subseteq> \<Union>f"
1.259 - then obtain e::real where "e>0" and "\<forall>x\<in>s. \<exists>b\<in>f. ball x e \<subseteq> b" using heine_borel_lemma[of s f] by auto
1.260 - hence "\<forall>x\<in>s. \<exists>b. b\<in>f \<and> ball x e \<subseteq> b" by auto
1.261 - hence "\<exists>bb. \<forall>x\<in>s. bb x \<in>f \<and> ball x e \<subseteq> bb x" using bchoice[of s "\<lambda>x b. b\<in>f \<and> ball x e \<subseteq> b"] by auto
1.262 - then obtain bb where bb:"\<forall>x\<in>s. (bb x) \<in> f \<and> ball x e \<subseteq> (bb x)" by blast
1.263 -
1.264 - from `seq_compact s` have "\<exists> k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
1.265 - using seq_compact_imp_totally_bounded[of s] `e>0` by auto
1.266 - then obtain k where k:"finite k" "k \<subseteq> s" "s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" by auto
1.267 -
1.268 - have "finite (bb ` k)" using k(1) by auto
1.269 - moreover
1.270 - { fix x assume "x\<in>s"
1.271 - hence "x\<in>\<Union>(\<lambda>x. ball x e) ` k" using k(3) unfolding subset_eq by auto
1.272 - hence "\<exists>X\<in>bb ` k. x \<in> X" using bb k(2) by blast
1.273 - hence "x \<in> \<Union>(bb ` k)" using Union_iff[of x "bb ` k"] by auto
1.274 - }
1.275 - ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
1.276 + assumes "seq_compact s" shows "compact s"
1.277 +proof -
1.278 + from seq_compact_imp_totally_bounded[OF `seq_compact s`]
1.279 + guess f unfolding choice_iff' .. note f = this
1.280 + def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
1.281 + have "countably_compact s"
1.282 + using `seq_compact s` by (rule seq_compact_imp_countably_compact)
1.283 + then show "compact s"
1.284 + proof (rule countably_compact_imp_compact)
1.285 + show "countable K"
1.286 + unfolding K_def using f
1.287 + by (auto intro: countable_finite countable_subset countable_rat
1.288 + intro!: countable_image countable_SIGMA countable_UN)
1.289 + show "\<forall>b\<in>K. open b" by (auto simp: K_def)
1.290 + next
1.291 + fix T x assume T: "open T" "x \<in> T" and x: "x \<in> s"
1.292 + from openE[OF T] obtain e where "0 < e" "ball x e \<subseteq> T" by auto
1.293 + then have "0 < e / 2" "ball x (e / 2) \<subseteq> T" by auto
1.294 + from Rats_dense_in_real[OF `0 < e / 2`] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2" by auto
1.295 + from f[rule_format, of r] `0 < r` `x \<in> s` obtain k where "k \<in> f r" "x \<in> ball k r"
1.296 + unfolding Union_image_eq by auto
1.297 + from `r \<in> \<rat>` `0 < r` `k \<in> f r` have "ball k r \<in> K" by (auto simp: K_def)
1.298 + then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"
1.299 + proof (rule bexI[rotated], safe)
1.300 + fix y assume "y \<in> ball k r"
1.301 + with `r < e / 2` `x \<in> ball k r` have "dist x y < e"
1.302 + by (intro dist_double[where x = k and d=e]) (auto simp: dist_commute)
1.303 + with `ball x e \<subseteq> T` show "y \<in> T" by auto
1.304 + qed (rule `x \<in> ball k r`)
1.305 + qed
1.306 qed
1.307
1.308 lemma compact_eq_seq_compact_metric:
1.309 @@ -3095,8 +3147,7 @@
1.310
1.311 lemma compact_def:
1.312 "compact (S :: 'a::metric_space set) \<longleftrightarrow>
1.313 - (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
1.314 - (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially)) "
1.315 + (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f o r) ----> l))"
1.316 unfolding compact_eq_seq_compact_metric seq_compact_def by auto
1.317
1.318 text {*
1.319 @@ -4879,41 +4930,42 @@
1.320 qed
1.321
1.322 text {* Continuity implies uniform continuity on a compact domain. *}
1.323 -
1.324 +
1.325 lemma compact_uniformly_continuous:
1.326 - assumes "continuous_on s f" "compact s"
1.327 + assumes f: "continuous_on s f" and s: "compact s"
1.328 shows "uniformly_continuous_on s f"
1.329 -proof-
1.330 - { fix x assume x:"x\<in>s"
1.331 - hence "\<forall>xa. \<exists>y. 0 < xa \<longrightarrow> (y > 0 \<and> (\<forall>x'\<in>s. dist x' x < y \<longrightarrow> dist (f x') (f x) < xa))" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=x]] by auto
1.332 - hence "\<exists>fa. \<forall>xa>0. \<forall>x'\<in>s. fa xa > 0 \<and> (dist x' x < fa xa \<longrightarrow> dist (f x') (f x) < xa)" using choice[of "\<lambda>e d. e>0 \<longrightarrow> d>0 \<and>(\<forall>x'\<in>s. (dist x' x < d \<longrightarrow> dist (f x') (f x) < e))"] by auto }
1.333 - then have "\<forall>x\<in>s. \<exists>y. \<forall>xa. 0 < xa \<longrightarrow> (\<forall>x'\<in>s. y xa > 0 \<and> (dist x' x < y xa \<longrightarrow> dist (f x') (f x) < xa))" by auto
1.334 - then obtain d where d:"\<forall>e>0. \<forall>x\<in>s. \<forall>x'\<in>s. d x e > 0 \<and> (dist x' x < d x e \<longrightarrow> dist (f x') (f x) < e)"
1.335 - using bchoice[of s "\<lambda>x fa. \<forall>xa>0. \<forall>x'\<in>s. fa xa > 0 \<and> (dist x' x < fa xa \<longrightarrow> dist (f x') (f x) < xa)"] by blast
1.336 -
1.337 - { fix e::real assume "e>0"
1.338 -
1.339 - { fix x assume "x\<in>s" hence "x \<in> ball x (d x (e / 2))" unfolding centre_in_ball using d[THEN spec[where x="e/2"]] using `e>0` by auto }
1.340 - hence "s \<subseteq> \<Union>{ball x (d x (e / 2)) |x. x \<in> s}" unfolding subset_eq by auto
1.341 - moreover
1.342 - { fix b assume "b\<in>{ball x (d x (e / 2)) |x. x \<in> s}" hence "open b" by auto }
1.343 - ultimately obtain ea where "ea>0" and ea:"\<forall>x\<in>s. \<exists>b\<in>{ball x (d x (e / 2)) |x. x \<in> s}. ball x ea \<subseteq> b"
1.344 - using heine_borel_lemma[OF assms(2)[unfolded compact_eq_seq_compact_metric], of "{ball x (d x (e / 2)) | x. x\<in>s }"] by auto
1.345 -
1.346 - { fix x y assume "x\<in>s" "y\<in>s" and as:"dist y x < ea"
1.347 - obtain z where "z\<in>s" and z:"ball x ea \<subseteq> ball z (d z (e / 2))" using ea[THEN bspec[where x=x]] and `x\<in>s` by auto
1.348 - hence "x\<in>ball z (d z (e / 2))" using `ea>0` unfolding subset_eq by auto
1.349 - hence "dist (f z) (f x) < e / 2" using d[THEN spec[where x="e/2"]] and `e>0` and `x\<in>s` and `z\<in>s`
1.350 - by (auto simp add: dist_commute)
1.351 - moreover have "y\<in>ball z (d z (e / 2))" using as and `ea>0` and z[unfolded subset_eq]
1.352 - by (auto simp add: dist_commute)
1.353 - hence "dist (f z) (f y) < e / 2" using d[THEN spec[where x="e/2"]] and `e>0` and `y\<in>s` and `z\<in>s`
1.354 - by (auto simp add: dist_commute)
1.355 - ultimately have "dist (f y) (f x) < e" using dist_triangle_half_r[of "f z" "f x" e "f y"]
1.356 - by (auto simp add: dist_commute) }
1.357 - then have "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `ea>0` by auto }
1.358 - thus ?thesis unfolding uniformly_continuous_on_def by auto
1.359 -qed
1.360 + unfolding uniformly_continuous_on_def
1.361 +proof (cases, safe)
1.362 + fix e :: real assume "0 < e" "s \<noteq> {}"
1.363 + def [simp]: R \<equiv> "{(y, d). y \<in> s \<and> 0 < d \<and> ball y d \<inter> s \<subseteq> {x \<in> s. f x \<in> ball (f y) (e/2) } }"
1.364 + let ?C = "(\<lambda>(y, d). ball y (d/2)) ` R"
1.365 + have "(\<forall>r\<in>?C. open r) \<and> s \<subseteq> \<Union>?C"
1.366 + proof safe
1.367 + fix y assume "y \<in> s"
1.368 + from continuous_open_in_preimage[OF f open_ball]
1.369 + obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
1.370 + unfolding openin_subtopology open_openin by metis
1.371 + then obtain d where "ball y d \<subseteq> T" "0 < d"
1.372 + using `0 < e` `y \<in> s` by (auto elim!: openE)
1.373 + with T `y \<in> s` show "y \<in> \<Union>(\<lambda>(y, d). ball y (d/2)) ` R"
1.374 + by (intro UnionI[where X="ball y (d/2)"]) auto
1.375 + qed auto
1.376 + then obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
1.377 + by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s] s Union_image_eq)
1.378 + with `s \<noteq> {}` have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)"
1.379 + by (subst Min_gr_iff) auto
1.380 + show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
1.381 + proof (rule, safe)
1.382 + fix x x' assume in_s: "x' \<in> s" "x \<in> s"
1.383 + with D obtain y d where x: "x \<in> ball y (d/2)" "(y, d) \<in> D"
1.384 + by blast
1.385 + moreover assume "dist x x' < Min (snd`D) / 2"
1.386 + ultimately have "dist y x' < d"
1.387 + by (intro dist_double[where x=x and d=d]) (auto simp: dist_commute)
1.388 + with D x in_s show "dist (f x) (f x') < e"
1.389 + by (intro dist_double[where x="f y" and d=e]) (auto simp: dist_commute subset_eq)
1.390 + qed (insert D, auto)
1.391 +qed auto
1.392
1.393 text{* Continuity of inverse function on compact domain. *}
1.394