generalized compact_Times to topological_space
authorhoelzl
Tue Mar 05 15:43:20 2013 +0100 (2013-03-05)
changeset 51349166170c5f8a2
parent 51348 011c97ba3b3d
child 51350 490f34774a9a
generalized compact_Times to topological_space
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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