1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 13:58:02 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 14:38:12 2013 +0100
1.3 @@ -2325,7 +2325,8 @@
1.4 lemma Inf_insert:
1.5 fixes S :: "real set"
1.6 shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
1.7 -by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
1.8 +by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
1.9 +
1.10 lemma Inf_insert_finite:
1.11 fixes S :: "real set"
1.12 shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
1.13 @@ -2349,6 +2350,12 @@
1.14 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
1.15 using assms unfolding compact_eq_heine_borel by metis
1.16
1.17 +lemma compactE_image:
1.18 + assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
1.19 + obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
1.20 + using assms unfolding ball_simps[symmetric] SUP_def
1.21 + by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
1.22 +
1.23 subsubsection {* Bolzano-Weierstrass property *}
1.24
1.25 lemma heine_borel_imp_bolzano_weierstrass:
1.26 @@ -2572,6 +2579,29 @@
1.27 by (simp add: eventually_nhds subset_eq)
1.28 qed
1.29
1.30 +lemma compact_imp_bounded:
1.31 + assumes "compact U" shows "bounded U"
1.32 +proof -
1.33 + have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto
1.34 + then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
1.35 + by (elim compactE_image)
1.36 + def d \<equiv> "SOME d. d \<in> D"
1.37 + show "bounded U"
1.38 + unfolding bounded_def
1.39 + proof (intro exI, safe)
1.40 + fix x assume "x \<in> U"
1.41 + with D obtain d' where "d' \<in> D" "x \<in> ball d' 1" by auto
1.42 + moreover have "dist d x \<le> dist d d' + dist d' x"
1.43 + using dist_triangle[of d x d'] by (simp add: dist_commute)
1.44 + moreover
1.45 + from `x\<in>U` D have "d \<in> D"
1.46 + unfolding d_def by (rule_tac someI_ex) auto
1.47 + ultimately
1.48 + show "dist d x \<le> Max ((\<lambda>d'. dist d d' + 1) ` D)"
1.49 + using D by (subst Max_ge_iff) (auto intro!: bexI[of _ d'])
1.50 + qed
1.51 +qed
1.52 +
1.53 text{* In particular, some common special cases. *}
1.54
1.55 lemma compact_empty[simp]:
1.56 @@ -3105,8 +3135,6 @@
1.57
1.58 subsubsection{* Heine-Borel theorem *}
1.59
1.60 -text {* Following Burkill \& Burkill vol. 2. *}
1.61 -
1.62 lemma seq_compact_imp_heine_borel:
1.63 fixes s :: "'a :: metric_space set"
1.64 assumes "seq_compact s" shows "compact s"
1.65 @@ -3150,6 +3178,22 @@
1.66 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f o r) ----> l))"
1.67 unfolding compact_eq_seq_compact_metric seq_compact_def by auto
1.68
1.69 +subsubsection {* Complete the chain of compactness variants *}
1.70 +
1.71 +lemma compact_eq_bolzano_weierstrass:
1.72 + fixes s :: "'a::metric_space set"
1.73 + shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
1.74 +proof
1.75 + assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
1.76 +next
1.77 + assume ?rhs thus ?lhs
1.78 + unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
1.79 +qed
1.80 +
1.81 +lemma bolzano_weierstrass_imp_bounded:
1.82 + "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
1.83 + using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
1.84 +
1.85 text {*
1.86 A metric space (or topological vector space) is said to have the
1.87 Heine-Borel property if every closed and bounded subset is compact.
1.88 @@ -3174,6 +3218,17 @@
1.89 using `l \<in> s` r l by blast
1.90 qed
1.91
1.92 +lemma compact_eq_bounded_closed:
1.93 + fixes s :: "'a::heine_borel set"
1.94 + shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs")
1.95 +proof
1.96 + assume ?lhs thus ?rhs
1.97 + using compact_imp_closed compact_imp_bounded by blast
1.98 +next
1.99 + assume ?rhs thus ?lhs
1.100 + using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
1.101 +qed
1.102 +
1.103 lemma lim_subseq:
1.104 "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
1.105 unfolding tendsto_def eventually_sequentially o_def
1.106 @@ -3498,84 +3553,6 @@
1.107 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
1.108 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
1.109
1.110 -subsubsection {* Complete the chain of compactness variants *}
1.111 -
1.112 -primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
1.113 - "helper_2 beyond 0 = beyond 0" |
1.114 - "helper_2 beyond (Suc n) = beyond (dist undefined (helper_2 beyond n) + 1 )"
1.115 -
1.116 -lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
1.117 - assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
1.118 - shows "bounded s"
1.119 -proof(rule ccontr)
1.120 - assume "\<not> bounded s"
1.121 - then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist undefined (beyond a) \<le> a"
1.122 - unfolding bounded_any_center [where a=undefined]
1.123 - apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist undefined x \<le> a"] by auto
1.124 - hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist undefined (beyond a) > a"
1.125 - unfolding linorder_not_le by auto
1.126 - def x \<equiv> "helper_2 beyond"
1.127 -
1.128 - { fix m n ::nat assume "m<n"
1.129 - hence "dist undefined (x m) + 1 < dist undefined (x n)"
1.130 - proof(induct n)
1.131 - case 0 thus ?case by auto
1.132 - next
1.133 - case (Suc n)
1.134 - have *:"dist undefined (x n) + 1 < dist undefined (x (Suc n))"
1.135 - unfolding x_def and helper_2.simps
1.136 - using beyond(2)[of "dist undefined (helper_2 beyond n) + 1"] by auto
1.137 - thus ?case proof(cases "m < n")
1.138 - case True thus ?thesis using Suc and * by auto
1.139 - next
1.140 - case False hence "m = n" using Suc(2) by auto
1.141 - thus ?thesis using * by auto
1.142 - qed
1.143 - qed } note * = this
1.144 - { fix m n ::nat assume "m\<noteq>n"
1.145 - have "1 < dist (x m) (x n)"
1.146 - proof(cases "m<n")
1.147 - case True
1.148 - hence "1 < dist undefined (x n) - dist undefined (x m)" using *[of m n] by auto
1.149 - thus ?thesis using dist_triangle [of undefined "x n" "x m"] by arith
1.150 - next
1.151 - case False hence "n<m" using `m\<noteq>n` by auto
1.152 - hence "1 < dist undefined (x m) - dist undefined (x n)" using *[of n m] by auto
1.153 - thus ?thesis using dist_triangle2 [of undefined "x m" "x n"] by arith
1.154 - qed } note ** = this
1.155 - { fix a b assume "x a = x b" "a \<noteq> b"
1.156 - hence False using **[of a b] by auto }
1.157 - hence "inj x" unfolding inj_on_def by auto
1.158 - moreover
1.159 - { fix n::nat
1.160 - have "x n \<in> s"
1.161 - proof(cases "n = 0")
1.162 - case True thus ?thesis unfolding x_def using beyond by auto
1.163 - next
1.164 - case False then obtain z where "n = Suc z" using not0_implies_Suc by auto
1.165 - thus ?thesis unfolding x_def using beyond by auto
1.166 - qed }
1.167 - ultimately have "infinite (range x) \<and> range x \<subseteq> s" unfolding x_def using range_inj_infinite[of "helper_2 beyond"] using beyond(1) by auto
1.168 -
1.169 - then obtain l where "l\<in>s" and l:"l islimpt range x" using assms[THEN spec[where x="range x"]] by auto
1.170 - then obtain y where "x y \<noteq> l" and y:"dist (x y) l < 1/2" unfolding islimpt_approachable apply(erule_tac x="1/2" in allE) by auto
1.171 - then obtain z where "x z \<noteq> l" and z:"dist (x z) l < dist (x y) l" using l[unfolded islimpt_approachable, THEN spec[where x="dist (x y) l"]]
1.172 - unfolding dist_nz by auto
1.173 - show False using y and z and dist_triangle_half_l[of "x y" l 1 "x z"] and **[of y z] by auto
1.174 -qed
1.175 -
1.176 -text {* Hence express everything as an equivalence. *}
1.177 -
1.178 -lemma compact_eq_bolzano_weierstrass:
1.179 - fixes s :: "'a::metric_space set"
1.180 - shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
1.181 -proof
1.182 - assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
1.183 -next
1.184 - assume ?rhs thus ?lhs
1.185 - unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
1.186 -qed
1.187 -
1.188 lemma nat_approx_posE:
1.189 fixes e::real
1.190 assumes "0 < e"
1.191 @@ -3724,28 +3701,6 @@
1.192 qed
1.193 qed
1.194
1.195 -lemma compact_eq_bounded_closed:
1.196 - fixes s :: "'a::heine_borel set"
1.197 - shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs")
1.198 -proof
1.199 - assume ?lhs thus ?rhs
1.200 - unfolding compact_eq_bolzano_weierstrass using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed by auto
1.201 -next
1.202 - assume ?rhs thus ?lhs
1.203 - using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
1.204 -qed
1.205 -
1.206 -lemma compact_imp_bounded:
1.207 - fixes s :: "'a::metric_space set"
1.208 - shows "compact s \<Longrightarrow> bounded s"
1.209 -proof -
1.210 - assume "compact s"
1.211 - hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
1.212 - using heine_borel_imp_bolzano_weierstrass[of s] by auto
1.213 - thus "bounded s"
1.214 - by (rule bolzano_weierstrass_imp_bounded)
1.215 -qed
1.216 -
1.217 lemma compact_cball[simp]:
1.218 fixes x :: "'a::heine_borel"
1.219 shows "compact(cball x e)"
1.220 @@ -4938,8 +4893,8 @@
1.221 proof (cases, safe)
1.222 fix e :: real assume "0 < e" "s \<noteq> {}"
1.223 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.224 - let ?C = "(\<lambda>(y, d). ball y (d/2)) ` R"
1.225 - have "(\<forall>r\<in>?C. open r) \<and> s \<subseteq> \<Union>?C"
1.226 + let ?b = "(\<lambda>(y, d). ball y (d/2))"
1.227 + have "(\<forall>r\<in>R. open (?b r))" "s \<subseteq> (\<Union>r\<in>R. ?b r)"
1.228 proof safe
1.229 fix y assume "y \<in> s"
1.230 from continuous_open_in_preimage[OF f open_ball]
1.231 @@ -4947,11 +4902,11 @@
1.232 unfolding openin_subtopology open_openin by metis
1.233 then obtain d where "ball y d \<subseteq> T" "0 < d"
1.234 using `0 < e` `y \<in> s` by (auto elim!: openE)
1.235 - with T `y \<in> s` show "y \<in> \<Union>(\<lambda>(y, d). ball y (d/2)) ` R"
1.236 - by (intro UnionI[where X="ball y (d/2)"]) auto
1.237 + with T `y \<in> s` show "y \<in> (\<Union>r\<in>R. ?b r)"
1.238 + by (intro UN_I[of "(y, d)"]) auto
1.239 qed auto
1.240 - then obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
1.241 - by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s] s Union_image_eq)
1.242 + with s obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
1.243 + by (rule compactE_image)
1.244 with `s \<noteq> {}` have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)"
1.245 by (subst Min_gr_iff) auto
1.246 show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"