218 proof (safe intro!: exI[where x=A]) |
218 proof (safe intro!: exI[where x=A]) |
219 show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite) |
219 show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite) |
220 fix a assume "a \<in> A" |
220 fix a assume "a \<in> A" |
221 thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
221 thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
222 next |
222 next |
223 let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N" |
223 let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" |
224 fix a b assume "a \<in> A" "b \<in> A" |
224 fix a b assume "a \<in> A" "b \<in> A" |
225 then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def) |
225 then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def) |
226 thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
226 thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
227 next |
227 next |
228 fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
228 fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
2615 (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})" |
2615 (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})" |
2616 (is "_ \<longleftrightarrow> ?R") |
2616 (is "_ \<longleftrightarrow> ?R") |
2617 proof (safe intro!: compact_eq_heine_borel[THEN iffD2]) |
2617 proof (safe intro!: compact_eq_heine_borel[THEN iffD2]) |
2618 fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}" |
2618 fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}" |
2619 and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" |
2619 and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" |
2620 from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>uminus`A" |
2620 from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)" |
2621 by auto |
2621 by auto |
2622 with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)" |
2622 with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)" |
2623 unfolding compact_eq_heine_borel by (metis subset_image_iff) |
2623 unfolding compact_eq_heine_borel by (metis subset_image_iff) |
2624 with fi[THEN spec, of B] show False |
2624 with fi[THEN spec, of B] show False |
2625 by (auto dest: finite_imageD intro: inj_setminus) |
2625 by (auto dest: finite_imageD intro: inj_setminus) |
2626 next |
2626 next |
2627 fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" |
2627 fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" |
2628 from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a" |
2628 from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a" |
2629 by auto |
2629 by auto |
2630 with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>uminus`B = {}" |
2630 with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}" |
2631 by (metis subset_image_iff) |
2631 by (metis subset_image_iff) |
2632 then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T" |
2632 then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T" |
2633 by (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD) |
2633 by (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD) |
2634 qed |
2634 qed |
2635 |
2635 |
3039 |
3039 |
3040 lemma seq_compact_imp_totally_bounded: |
3040 lemma seq_compact_imp_totally_bounded: |
3041 assumes "seq_compact s" |
3041 assumes "seq_compact s" |
3042 shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" |
3042 shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" |
3043 proof(rule, rule, rule ccontr) |
3043 proof(rule, rule, rule ccontr) |
3044 fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)" |
3044 fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))" |
3045 def x \<equiv> "helper_1 s e" |
3045 def x \<equiv> "helper_1 s e" |
3046 { fix n |
3046 { fix n |
3047 have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" |
3047 have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" |
3048 proof(induct_tac rule:nat_less_induct) |
3048 proof(induct_tac rule:nat_less_induct) |
3049 fix n def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))" |
3049 fix n def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))" |
4584 from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)" |
4584 from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)" |
4585 by auto |
4585 by auto |
4586 moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)" |
4586 moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)" |
4587 by (fastforce simp: subset_eq) |
4587 by (fastforce simp: subset_eq) |
4588 ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)" |
4588 ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)" |
4589 using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT) |
4589 using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT) |
4590 qed |
4590 qed |
4591 then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)" |
4591 then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)" |
4592 and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x" |
4592 and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x" |
4593 unfolding subset_eq UN_iff by metis |
4593 unfolding subset_eq UN_iff by metis |
4594 moreover from compactE_image[OF `compact s` a] obtain e where e: "e \<subseteq> s" "finite e" |
4594 moreover from compactE_image[OF `compact s` a] obtain e where e: "e \<subseteq> s" "finite e" |