author hoelzl Tue Mar 05 15:43:20 2013 +0100 (2013-03-05) changeset 51349 166170c5f8a2 parent 51348 011c97ba3b3d child 51350 490f34774a9a
generalized compact_Times to topological_space
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:19 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:20 2013 +0100
1.3 @@ -5031,11 +5031,43 @@
1.4  apply (simp add: o_def)
1.5  done
1.6
1.7 -text {* Generalize to @{class topological_space} *}
1.8  lemma compact_Times:
1.9 -  fixes s :: "'a::metric_space set" and t :: "'b::metric_space set"
1.10 -  shows "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
1.11 -  unfolding compact_eq_seq_compact_metric by (rule seq_compact_Times)
1.12 +  assumes "compact s" "compact t"
1.13 +  shows "compact (s \<times> t)"
1.14 +proof (rule compactI)
1.15 +  fix C assume C: "\<forall>t\<in>C. open t" "s \<times> t \<subseteq> \<Union>C"
1.16 +  have "\<forall>x\<in>s. \<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
1.17 +  proof
1.18 +    fix x assume "x \<in> s"
1.19 +    have "\<forall>y\<in>t. \<exists>a b c. c \<in> C \<and> open a \<and> open b \<and> x \<in> a \<and> y \<in> b \<and> a \<times> b \<subseteq> c" (is "\<forall>y\<in>t. ?P y")
1.20 +    proof
1.21 +      fix y assume "y \<in> t"
1.22 +      with `x \<in> s` C obtain c where "c \<in> C" "(x, y) \<in> c" "open c" by auto
1.23 +      then show "?P y" by (auto elim!: open_prod_elim)
1.24 +    qed
1.25 +    then obtain a b c where b: "\<And>y. y \<in> t \<Longrightarrow> open (b y)"
1.26 +      and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
1.27 +      by metis
1.28 +    then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
1.29 +    from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
1.30 +      by auto
1.31 +    moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
1.32 +      by (fastforce simp: subset_eq)
1.33 +    ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
1.34 +      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
1.35 +  qed
1.36 +  then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
1.37 +    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"
1.38 +    unfolding subset_eq UN_iff by metis
1.39 +  moreover from compactE_image[OF `compact s` a] obtain e where e: "e \<subseteq> s" "finite e"
1.40 +    and s: "s \<subseteq> (\<Union>x\<in>e. a x)" by auto
1.41 +  moreover
1.42 +  { from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)" by auto
1.43 +    also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)" using d `e \<subseteq> s` by (intro UN_mono) auto
1.44 +    finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" . }
1.45 +  ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
1.46 +    by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp add: subset_eq)
1.47 +qed
1.48
1.49  text{* Hence some useful properties follow quite easily. *}
1.50
```