src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 52141 eff000cab70f parent 51773 9328c6681f3c child 52624 8a7b59a81088
equal inserted replaced
52140:88a69da5d3fa 52141:eff000cab70f
`   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"`