1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 15:28:53 2013 -0800
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 18 20:00:59 2013 +0100
1.3 @@ -9,7 +9,6 @@
1.4 theory Topology_Euclidean_Space
1.5 imports
1.6 Complex_Main
1.7 - "~~/src/HOL/Library/Diagonal_Subsequence"
1.8 "~~/src/HOL/Library/Countable_Set"
1.9 "~~/src/HOL/Library/Glbs"
1.10 "~~/src/HOL/Library/FuncSet"
1.11 @@ -3417,10 +3416,120 @@
1.12
1.13 subsubsection{* Completeness *}
1.14
1.15 -definition
1.16 - complete :: "'a::metric_space set \<Rightarrow> bool" where
1.17 - "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
1.18 - --> (\<exists>l \<in> s. (f ---> l) sequentially))"
1.19 +definition complete :: "'a::metric_space set \<Rightarrow> bool" where
1.20 + "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
1.21 +
1.22 +lemma compact_imp_complete: assumes "compact s" shows "complete s"
1.23 +proof-
1.24 + { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
1.25 + from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) ----> l"
1.26 + using assms unfolding compact_def by blast
1.27 +
1.28 + note lr' = seq_suble [OF lr(2)]
1.29 +
1.30 + { fix e::real assume "e>0"
1.31 + from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
1.32 + from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
1.33 + { fix n::nat assume n:"n \<ge> max N M"
1.34 + have "dist ((f \<circ> r) n) l < e/2" using n M by auto
1.35 + moreover have "r n \<ge> N" using lr'[of n] n by auto
1.36 + hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
1.37 + ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) }
1.38 + hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast }
1.39 + hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto }
1.40 + thus ?thesis unfolding complete_def by auto
1.41 +qed
1.42 +
1.43 +lemma nat_approx_posE:
1.44 + fixes e::real
1.45 + assumes "0 < e"
1.46 + obtains n::nat where "1 / (Suc n) < e"
1.47 +proof atomize_elim
1.48 + have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
1.49 + by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
1.50 + also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
1.51 + by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
1.52 + also have "\<dots> = e" by simp
1.53 + finally show "\<exists>n. 1 / real (Suc n) < e" ..
1.54 +qed
1.55 +
1.56 +lemma compact_eq_totally_bounded:
1.57 + "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
1.58 + (is "_ \<longleftrightarrow> ?rhs")
1.59 +proof
1.60 + assume assms: "?rhs"
1.61 + then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
1.62 + by (auto simp: choice_iff')
1.63 +
1.64 + show "compact s"
1.65 + proof cases
1.66 + assume "s = {}" thus "compact s" by (simp add: compact_def)
1.67 + next
1.68 + assume "s \<noteq> {}"
1.69 + show ?thesis
1.70 + unfolding compact_def
1.71 + proof safe
1.72 + fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
1.73 +
1.74 + def e \<equiv> "\<lambda>n. 1 / (2 * Suc n)"
1.75 + then have [simp]: "\<And>n. 0 < e n" by auto
1.76 + def B \<equiv> "\<lambda>n U. SOME b. infinite {n. f n \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
1.77 + { fix n U assume "infinite {n. f n \<in> U}"
1.78 + then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
1.79 + using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
1.80 + then guess a ..
1.81 + then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
1.82 + by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
1.83 + from someI_ex[OF this]
1.84 + have "infinite {i. f i \<in> B n U}" "\<exists>x. B n U \<subseteq> ball x (e n) \<inter> U"
1.85 + unfolding B_def by auto }
1.86 + note B = this
1.87 +
1.88 + def F \<equiv> "nat_rec (B 0 UNIV) B"
1.89 + { fix n have "infinite {i. f i \<in> F n}"
1.90 + by (induct n) (auto simp: F_def B) }
1.91 + then have F: "\<And>n. \<exists>x. F (Suc n) \<subseteq> ball x (e n) \<inter> F n"
1.92 + using B by (simp add: F_def)
1.93 + then have F_dec: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
1.94 + using decseq_SucI[of F] by (auto simp: decseq_def)
1.95 +
1.96 + obtain sel where sel: "\<And>k i. i < sel k i" "\<And>k i. f (sel k i) \<in> F k"
1.97 + proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)
1.98 + fix k i
1.99 + have "infinite ({n. f n \<in> F k} - {.. i})"
1.100 + using `infinite {n. f n \<in> F k}` by auto
1.101 + from infinite_imp_nonempty[OF this]
1.102 + show "\<exists>x>i. f x \<in> F k"
1.103 + by (simp add: set_eq_iff not_le conj_commute)
1.104 + qed
1.105 +
1.106 + def t \<equiv> "nat_rec (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
1.107 + have "subseq t"
1.108 + unfolding subseq_Suc_iff by (simp add: t_def sel)
1.109 + moreover have "\<forall>i. (f \<circ> t) i \<in> s"
1.110 + using f by auto
1.111 + moreover
1.112 + { fix n have "(f \<circ> t) n \<in> F n"
1.113 + by (cases n) (simp_all add: t_def sel) }
1.114 + note t = this
1.115 +
1.116 + have "Cauchy (f \<circ> t)"
1.117 + proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
1.118 + fix r :: real and N n m assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
1.119 + then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
1.120 + using F_dec t by (auto simp: e_def field_simps real_of_nat_Suc)
1.121 + with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
1.122 + by (auto simp: subset_eq)
1.123 + with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] `2 * e N < r`
1.124 + show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
1.125 + by (simp add: dist_commute)
1.126 + qed
1.127 +
1.128 + ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.129 + using assms unfolding complete_def by blast
1.130 + qed
1.131 + qed
1.132 +qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
1.133
1.134 lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
1.135 proof-
1.136 @@ -3462,35 +3571,15 @@
1.137 apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
1.138 qed
1.139
1.140 -lemma seq_compact_imp_complete: assumes "seq_compact s" shows "complete s"
1.141 -proof-
1.142 - { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
1.143 - from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
1.144 -
1.145 - note lr' = seq_suble [OF lr(2)]
1.146 -
1.147 - { fix e::real assume "e>0"
1.148 - from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
1.149 - from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
1.150 - { fix n::nat assume n:"n \<ge> max N M"
1.151 - have "dist ((f \<circ> r) n) l < e/2" using n M by auto
1.152 - moreover have "r n \<ge> N" using lr'[of n] n by auto
1.153 - hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
1.154 - ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) }
1.155 - hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast }
1.156 - hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto }
1.157 - thus ?thesis unfolding complete_def by auto
1.158 -qed
1.159 -
1.160 instance heine_borel < complete_space
1.161 proof
1.162 fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
1.163 hence "bounded (range f)"
1.164 by (rule cauchy_imp_bounded)
1.165 - hence "seq_compact (closure (range f))"
1.166 - using bounded_closed_imp_seq_compact [of "closure (range f)"] by auto
1.167 + hence "compact (closure (range f))"
1.168 + unfolding compact_eq_bounded_closed by auto
1.169 hence "complete (closure (range f))"
1.170 - by (rule seq_compact_imp_complete)
1.171 + by (rule compact_imp_complete)
1.172 moreover have "\<forall>n. f n \<in> closure (range f)"
1.173 using closure_subset [of "range f"] by auto
1.174 ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
1.175 @@ -3543,154 +3632,6 @@
1.176 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
1.177 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
1.178
1.179 -lemma nat_approx_posE:
1.180 - fixes e::real
1.181 - assumes "0 < e"
1.182 - obtains n::nat where "1 / (Suc n) < e"
1.183 -proof atomize_elim
1.184 - have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
1.185 - by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
1.186 - also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
1.187 - by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
1.188 - also have "\<dots> = e" by simp
1.189 - finally show "\<exists>n. 1 / real (Suc n) < e" ..
1.190 -qed
1.191 -
1.192 -lemma compact_eq_totally_bounded:
1.193 - "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
1.194 -proof (safe intro!: seq_compact_imp_complete[unfolded compact_eq_seq_compact_metric[symmetric]])
1.195 - fix e::real
1.196 - def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
1.197 - assume "0 < e" "compact s"
1.198 - hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
1.199 - by (simp add: compact_eq_heine_borel)
1.200 - moreover
1.201 - have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
1.202 - hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
1.203 - ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
1.204 - then guess K .. note K = this
1.205 - have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
1.206 - then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
1.207 - thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
1.208 - by (intro exI[where x="k ` K"]) (auto simp: f_def)
1.209 -next
1.210 - assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
1.211 - show "compact s"
1.212 - proof cases
1.213 - assume "s = {}" thus "compact s" by (simp add: compact_def)
1.214 - next
1.215 - assume "s \<noteq> {}"
1.216 - show ?thesis
1.217 - unfolding compact_def
1.218 - proof safe
1.219 - fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
1.220 - from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
1.221 - then obtain K where
1.222 - K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.223 - unfolding choice_iff by blast
1.224 - {
1.225 - fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
1.226 - assume "e > 0"
1.227 - from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.228 - by simp_all
1.229 - have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
1.230 - proof (rule ccontr)
1.231 - from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.232 - using `s \<noteq> {}`
1.233 - by auto
1.234 - moreover
1.235 - assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
1.236 - hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
1.237 - ultimately
1.238 - show False using f'
1.239 - proof (induct arbitrary: s f f' rule: finite_ne_induct)
1.240 - case (singleton x)
1.241 - have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
1.242 - thus ?case using singleton by (auto simp: ball_def)
1.243 - next
1.244 - case (insert x A)
1.245 - show ?case
1.246 - proof cases
1.247 - have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
1.248 - have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
1.249 - using insert by (intro infinite_super[OF _ inf_ms]) auto
1.250 - also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
1.251 - {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
1.252 - finally have "infinite \<dots>" .
1.253 - moreover assume "finite {m. (f o f') m \<in> ball x e}"
1.254 - ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
1.255 - hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
1.256 - def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
1.257 - have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
1.258 - using enumerate_mono[OF _ inf] by (simp add: r_def)
1.259 - hence "subseq r" by (simp add: subseq_def)
1.260 - have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
1.261 - using enumerate_in_set[OF inf] by (simp add: r_def)
1.262 - show False
1.263 - proof (rule insert)
1.264 - show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
1.265 - fix k s assume "k \<in> A" "subseq s"
1.266 - thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
1.267 - by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
1.268 - next
1.269 - fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
1.270 - qed
1.271 - next
1.272 - assume inf: "infinite {m. (f o f') m \<in> ball x e}"
1.273 - def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
1.274 - have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
1.275 - using enumerate_mono[OF _ inf] by (simp add: r_def)
1.276 - hence "subseq r" by (simp add: subseq_def)
1.277 - from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
1.278 - moreover
1.279 - have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
1.280 - using enumerate_in_set[OF inf] by (simp add: r_def)
1.281 - hence "(f o f') (r i) \<in> ball x e" by simp
1.282 - ultimately show False by simp
1.283 - qed
1.284 - qed
1.285 - qed
1.286 - }
1.287 - hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
1.288 - let ?e = "\<lambda>n. 1 / real (Suc n)"
1.289 - let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
1.290 - interpret subseqs ?P using ex by unfold_locales force
1.291 - from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
1.292 - by (simp add: complete_def)
1.293 - have "\<exists>l\<in>s. (f o diagseq) ----> l"
1.294 - proof (intro limI metric_CauchyI)
1.295 - fix e::real assume "0 < e" hence "0 < e / 2" by auto
1.296 - from nat_approx_posE[OF this] guess n . note n = this
1.297 - show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
1.298 - proof (rule exI[where x="Suc n"], safe)
1.299 - fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
1.300 - let ?e = "1 / real (Suc n)"
1.301 - from reducer_reduces[of n] obtain k where
1.302 - "k\<in>K ?e" "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
1.303 - unfolding seqseq_reducer by auto
1.304 - moreover
1.305 - note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
1.306 - ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
1.307 - also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
1.308 - finally
1.309 - have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
1.310 - by (intro add_strict_mono) auto
1.311 - hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
1.312 - by (simp add: dist_commute)
1.313 - moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
1.314 - dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
1.315 - by (rule dist_triangle2)
1.316 - ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
1.317 - by simp
1.318 - qed
1.319 - next
1.320 - fix n show "(f o diagseq) n \<in> s" using f by simp
1.321 - qed
1.322 - thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
1.323 - qed
1.324 - qed
1.325 -qed
1.326 -
1.327 lemma compact_cball[simp]:
1.328 fixes x :: "'a::heine_borel"
1.329 shows "compact(cball x e)"
2.1 --- a/src/HOL/Probability/Projective_Limit.thy Thu Jan 17 15:28:53 2013 -0800
2.2 +++ b/src/HOL/Probability/Projective_Limit.thy Fri Jan 18 20:00:59 2013 +0100
2.3 @@ -11,7 +11,7 @@
2.4 Regularity
2.5 Projective_Family
2.6 Infinite_Product_Measure
2.7 - "~~/src/HOL/Library/Countable_Set"
2.8 + "~~/src/HOL/Library/Diagonal_Subsequence"
2.9 begin
2.10
2.11 subsection {* Sequences of Finite Maps in Compact Sets *}