# HG changeset patch
# User hoelzl
# Date 1362494600 -3600
# Node ID 166170c5f8a2895a2bbc06ae030248d0bf399dd6
# Parent  011c97ba3b3df381093282a7d9f8a06e269e2db5
generalized compact_Times to topological_space

diff -r 011c97ba3b3d -r 166170c5f8a2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:19 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:20 2013 +0100
@@ -5031,11 +5031,43 @@
 apply (simp add: o_def)
 done
 
-text {* Generalize to @{class topological_space} *}
 lemma compact_Times: 
-  fixes s :: "'a::metric_space set" and t :: "'b::metric_space set"
-  shows "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
-  unfolding compact_eq_seq_compact_metric by (rule seq_compact_Times)
+  assumes "compact s" "compact t"
+  shows "compact (s \<times> t)"
+proof (rule compactI)
+  fix C assume C: "\<forall>t\<in>C. open t" "s \<times> t \<subseteq> \<Union>C"
+  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)"
+  proof
+    fix x assume "x \<in> s"
+    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")
+    proof 
+      fix y assume "y \<in> t"
+      with `x \<in> s` C obtain c where "c \<in> C" "(x, y) \<in> c" "open c" by auto
+      then show "?P y" by (auto elim!: open_prod_elim)
+    qed
+    then obtain a b c where b: "\<And>y. y \<in> t \<Longrightarrow> open (b y)"
+      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"
+      by metis
+    then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
+    from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
+      by auto
+    moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
+      by (fastforce simp: subset_eq)
+    ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
+      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
+  qed
+  then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
+    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"
+    unfolding subset_eq UN_iff by metis
+  moreover from compactE_image[OF `compact s` a] obtain e where e: "e \<subseteq> s" "finite e"
+    and s: "s \<subseteq> (\<Union>x\<in>e. a x)" by auto
+  moreover
+  { from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)" by auto
+    also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)" using d `e \<subseteq> s` by (intro UN_mono) auto
+    finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" . }
+  ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
+    by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp add: subset_eq)
+qed
 
 text{* Hence some useful properties follow quite easily. *}