move product topology to HOL-Complex_Main
authorhoelzl
Mon Feb 08 17:18:13 2016 +0100 (2016-02-08)
changeset 62367d2bc8a7e5fec
parent 62366 95c6cf433c91
child 62368 106569399cd6
move product topology to HOL-Complex_Main
src/HOL/Filter.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Thu Feb 18 17:53:09 2016 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Feb 08 17:18:13 2016 +0100
     1.3 @@ -479,6 +479,29 @@
     1.4      eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
     1.5    by (subst eventually_Inf_base) auto
     1.6  
     1.7 +lemma eventually_INF_mono:
     1.8 +  assumes *: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F i. P x"
     1.9 +  assumes T1: "\<And>Q R P. (\<And>x. Q x \<and> R x \<longrightarrow> P x) \<Longrightarrow> (\<And>x. T Q x \<Longrightarrow> T R x \<Longrightarrow> T P x)"
    1.10 +  assumes T2: "\<And>P. (\<And>x. P x) \<Longrightarrow> (\<And>x. T P x)"
    1.11 +  assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x"
    1.12 +  shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
    1.13 +proof -
    1.14 +  from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
    1.15 +    unfolding eventually_INF[of _ I] by auto
    1.16 +  moreover then have "eventually (T P) (INFIMUM X F')"
    1.17 +    apply (induction X arbitrary: P)
    1.18 +    apply (auto simp: eventually_inf T2)
    1.19 +    subgoal for x S P Q R
    1.20 +      apply (intro exI[of _ "T Q"])
    1.21 +      apply (auto intro!: **) []
    1.22 +      apply (intro exI[of _ "T R"])
    1.23 +      apply (auto intro: T1) []
    1.24 +      done
    1.25 +    done
    1.26 +  ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
    1.27 +    by (subst eventually_INF) auto
    1.28 +qed
    1.29 +
    1.30  
    1.31  subsubsection \<open>Map function for filters\<close>
    1.32  
    1.33 @@ -530,7 +553,6 @@
    1.34      by (subst (1 2) eventually_INF) auto
    1.35  qed
    1.36  
    1.37 -
    1.38  subsubsection \<open>Standard filters\<close>
    1.39  
    1.40  definition principal :: "'a set \<Rightarrow> 'a filter" where
    1.41 @@ -768,9 +790,116 @@
    1.42      by auto
    1.43  qed (auto simp: eventually_principal intro: eventually_True)
    1.44  
    1.45 +lemma eventually_prod1:
    1.46 +  assumes "B \<noteq> bot"
    1.47 +  shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
    1.48 +  unfolding eventually_prod_filter
    1.49 +proof safe
    1.50 +  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
    1.51 +  moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
    1.52 +  ultimately show "eventually P A"
    1.53 +    by (force elim: eventually_mono)
    1.54 +next
    1.55 +  assume "eventually P A"
    1.56 +  then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P x)"
    1.57 +    by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
    1.58 +qed
    1.59 +
    1.60 +lemma eventually_prod2:
    1.61 +  assumes "A \<noteq> bot"
    1.62 +  shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
    1.63 +  unfolding eventually_prod_filter
    1.64 +proof safe
    1.65 +  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
    1.66 +  moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
    1.67 +  ultimately show "eventually P B"
    1.68 +    by (force elim: eventually_mono)
    1.69 +next
    1.70 +  assume "eventually P B"
    1.71 +  then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P y)"
    1.72 +    by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
    1.73 +qed
    1.74 +
    1.75 +lemma INF_filter_bot_base:
    1.76 +  fixes F :: "'a \<Rightarrow> 'b filter"
    1.77 +  assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
    1.78 +  shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
    1.79 +proof cases
    1.80 +  assume "\<exists>i\<in>I. F i = bot"
    1.81 +  moreover then have "(INF i:I. F i) \<le> bot"
    1.82 +    by (auto intro: INF_lower2)
    1.83 +  ultimately show ?thesis
    1.84 +    by (auto simp: bot_unique)
    1.85 +next
    1.86 +  assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
    1.87 +  moreover have "(INF i:I. F i) \<noteq> bot"
    1.88 +  proof cases
    1.89 +    assume "I \<noteq> {}"
    1.90 +    show ?thesis
    1.91 +    proof (rule INF_filter_not_bot)
    1.92 +      fix J assume "finite J" "J \<subseteq> I"
    1.93 +      then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
    1.94 +      proof (induction J)
    1.95 +        case empty then show ?case
    1.96 +          using \<open>I \<noteq> {}\<close> by auto
    1.97 +      next
    1.98 +        case (insert i J)
    1.99 +        moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
   1.100 +        moreover note *[of i k]
   1.101 +        ultimately show ?case
   1.102 +          by auto
   1.103 +      qed
   1.104 +      with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
   1.105 +        by (auto simp: bot_unique)
   1.106 +    qed
   1.107 +  qed (auto simp add: filter_eq_iff)
   1.108 +  ultimately show ?thesis
   1.109 +    by auto
   1.110 +qed
   1.111 +
   1.112 +lemma Collect_empty_eq_bot: "Collect P = {} \<longleftrightarrow> P = \<bottom>"
   1.113 +  by auto
   1.114 +
   1.115 +lemma prod_filter_eq_bot: "A \<times>\<^sub>F B = bot \<longleftrightarrow> A = bot \<or> B = bot"
   1.116 +  unfolding prod_filter_def
   1.117 +proof (subst INF_filter_bot_base; clarsimp simp: principal_eq_bot_iff Collect_empty_eq_bot bot_fun_def simp del: Collect_empty_eq)
   1.118 +  fix A1 A2 B1 B2 assume "\<forall>\<^sub>F x in A. A1 x" "\<forall>\<^sub>F x in A. A2 x" "\<forall>\<^sub>F x in B. B1 x" "\<forall>\<^sub>F x in B. B2 x"
   1.119 +  then show "\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> Collect x \<times> Collect y \<subseteq> Collect A1 \<times> Collect B1 \<and> Collect x \<times> Collect y \<subseteq> Collect A2 \<times> Collect B2)"
   1.120 +    by (intro exI[of _ "\<lambda>x. A1 x \<and> A2 x"] exI[of _ "\<lambda>x. B1 x \<and> B2 x"] conjI)
   1.121 +       (auto simp: eventually_conj_iff)
   1.122 +next
   1.123 +  show "(\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> (x = (\<lambda>x. False) \<or> y = (\<lambda>x. False)))) = (A = \<bottom> \<or> B = \<bottom>)"
   1.124 +    by (auto simp: trivial_limit_def intro: eventually_True)
   1.125 +qed
   1.126 +
   1.127  lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
   1.128    by (auto simp: le_filter_def eventually_prod_filter)
   1.129  
   1.130 +lemma prod_filter_mono_iff:
   1.131 +  assumes nAB: "A \<noteq> bot" "B \<noteq> bot"
   1.132 +  shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
   1.133 +proof safe
   1.134 +  assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
   1.135 +  moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
   1.136 +    by (auto simp: bot_unique prod_filter_eq_bot)
   1.137 +  ultimately have "C \<times>\<^sub>F D \<noteq> bot"
   1.138 +    by (auto simp: bot_unique)
   1.139 +  then have nCD: "C \<noteq> bot" "D \<noteq> bot"
   1.140 +    by (auto simp: prod_filter_eq_bot)
   1.141 +
   1.142 +  show "A \<le> C"
   1.143 +  proof (rule filter_leI)
   1.144 +    fix P assume "eventually P C" with *[THEN filter_leD, of "\<lambda>(x, y). P x"] show "eventually P A"
   1.145 +      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
   1.146 +  qed
   1.147 +
   1.148 +  show "B \<le> D"
   1.149 +  proof (rule filter_leI)
   1.150 +    fix P assume "eventually P D" with *[THEN filter_leD, of "\<lambda>(x, y). P y"] show "eventually P B"
   1.151 +      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
   1.152 +  qed
   1.153 +qed (intro prod_filter_mono)
   1.154 +
   1.155  lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
   1.156      (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
   1.157    unfolding eventually_prod_filter
   1.158 @@ -791,6 +920,52 @@
   1.159    apply auto
   1.160    done
   1.161  
   1.162 +lemma prod_filter_INF:
   1.163 +  assumes "I \<noteq> {}" "J \<noteq> {}"
   1.164 +  shows "(INF i:I. A i) \<times>\<^sub>F (INF j:J. B j) = (INF i:I. INF j:J. A i \<times>\<^sub>F B j)"
   1.165 +proof (safe intro!: antisym INF_greatest)
   1.166 +  from \<open>I \<noteq> {}\<close> obtain i where "i \<in> I" by auto
   1.167 +  from \<open>J \<noteq> {}\<close> obtain j where "j \<in> J" by auto
   1.168 +
   1.169 +  show "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j) \<le> (\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j)"
   1.170 +    unfolding prod_filter_def
   1.171 +  proof (safe intro!: INF_greatest)
   1.172 +    fix P Q assume P: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. A i. P x" and Q: "\<forall>\<^sub>F x in \<Sqinter>j\<in>J. B j. Q x"
   1.173 +    let ?X = "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. \<Sqinter>(P, Q)\<in>{(P, Q). (\<forall>\<^sub>F x in A i. P x) \<and> (\<forall>\<^sub>F x in B j. Q x)}. principal {(x, y). P x \<and> Q y})"
   1.174 +    have "?X \<le> principal {x. P (fst x)} \<sqinter> principal {x. Q (snd x)}"
   1.175 +    proof (intro inf_greatest)
   1.176 +      have "?X \<le> (\<Sqinter>i\<in>I. \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)})"
   1.177 +        by (auto intro!: INF_greatest INF_lower2[of j] INF_lower2 \<open>j\<in>J\<close> INF_lower2[of "(_, \<lambda>x. True)"])
   1.178 +      also have "\<dots> \<le> principal {x. P (fst x)}"
   1.179 +        unfolding le_principal
   1.180 +      proof (rule eventually_INF_mono[OF P])
   1.181 +        fix i P assume "i \<in> I" "eventually P (A i)"
   1.182 +        then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)}. x \<in> {x. P (fst x)}"
   1.183 +          unfolding le_principal[symmetric] by (auto intro!: INF_lower)
   1.184 +      qed auto
   1.185 +      finally show "?X \<le> principal {x. P (fst x)}" .
   1.186 +
   1.187 +      have "?X \<le> (\<Sqinter>i\<in>J. \<Sqinter>P\<in>{P. eventually P (B i)}. principal {x. P (snd x)})"
   1.188 +        by (auto intro!: INF_greatest INF_lower2[of i] INF_lower2 \<open>i\<in>I\<close> INF_lower2[of "(\<lambda>x. True, _)"])
   1.189 +      also have "\<dots> \<le> principal {x. Q (snd x)}"
   1.190 +        unfolding le_principal
   1.191 +      proof (rule eventually_INF_mono[OF Q])
   1.192 +        fix j Q assume "j \<in> J" "eventually Q (B j)"
   1.193 +        then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (B j)}. principal {x. P (snd x)}. x \<in> {x. Q (snd x)}"
   1.194 +          unfolding le_principal[symmetric] by (auto intro!: INF_lower)
   1.195 +      qed auto
   1.196 +      finally show "?X \<le> principal {x. Q (snd x)}" .
   1.197 +    qed
   1.198 +    also have "\<dots> = principal {(x, y). P x \<and> Q y}"
   1.199 +      by auto
   1.200 +    finally show "?X \<le> principal {(x, y). P x \<and> Q y}" .
   1.201 +  qed
   1.202 +qed (intro prod_filter_mono INF_lower)
   1.203 +
   1.204 +lemma filtermap_Pair: "filtermap (\<lambda>x. (f x, g x)) F \<le> filtermap f F \<times>\<^sub>F filtermap g F"
   1.205 +  by (simp add: le_filter_def eventually_filtermap eventually_prod_filter)
   1.206 +     (auto elim: eventually_elim2)
   1.207 +
   1.208  subsection \<open>Limits\<close>
   1.209  
   1.210  definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.211 @@ -800,7 +975,7 @@
   1.212    "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   1.213  
   1.214  translations
   1.215 -  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
   1.216 +  "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
   1.217  
   1.218  lemma filterlim_iff:
   1.219    "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   1.220 @@ -907,6 +1082,11 @@
   1.221      LIM x F. if P x then f x else g x :> G"
   1.222    unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
   1.223  
   1.224 +lemma filterlim_Pair:
   1.225 +  "LIM x F. f x :> G \<Longrightarrow> LIM x F. g x :> H \<Longrightarrow> LIM x F. (f x, g x) :> G \<times>\<^sub>F H"
   1.226 +  unfolding filterlim_def
   1.227 +  by (rule order_trans[OF filtermap_Pair prod_filter_mono])
   1.228 +
   1.229  subsection \<open>Limits to @{const at_top} and @{const at_bot}\<close>
   1.230  
   1.231  lemma filterlim_at_top:
     2.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Feb 18 17:53:09 2016 +0100
     2.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Feb 08 17:18:13 2016 +0100
     2.3 @@ -40,239 +40,6 @@
     2.4  
     2.5  end
     2.6  
     2.7 -subsection \<open>Product is a topological space\<close>
     2.8 -
     2.9 -instantiation prod :: (topological_space, topological_space) topological_space
    2.10 -begin
    2.11 -
    2.12 -definition open_prod_def[code del]:
    2.13 -  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
    2.14 -    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
    2.15 -
    2.16 -lemma open_prod_elim:
    2.17 -  assumes "open S" and "x \<in> S"
    2.18 -  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
    2.19 -using assms unfolding open_prod_def by fast
    2.20 -
    2.21 -lemma open_prod_intro:
    2.22 -  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
    2.23 -  shows "open S"
    2.24 -using assms unfolding open_prod_def by fast
    2.25 -
    2.26 -instance
    2.27 -proof
    2.28 -  show "open (UNIV :: ('a \<times> 'b) set)"
    2.29 -    unfolding open_prod_def by auto
    2.30 -next
    2.31 -  fix S T :: "('a \<times> 'b) set"
    2.32 -  assume "open S" "open T"
    2.33 -  show "open (S \<inter> T)"
    2.34 -  proof (rule open_prod_intro)
    2.35 -    fix x assume x: "x \<in> S \<inter> T"
    2.36 -    from x have "x \<in> S" by simp
    2.37 -    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
    2.38 -      using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
    2.39 -    from x have "x \<in> T" by simp
    2.40 -    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
    2.41 -      using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
    2.42 -    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
    2.43 -    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
    2.44 -      using A B by (auto simp add: open_Int)
    2.45 -    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
    2.46 -      by fast
    2.47 -  qed
    2.48 -next
    2.49 -  fix K :: "('a \<times> 'b) set set"
    2.50 -  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    2.51 -    unfolding open_prod_def by fast
    2.52 -qed
    2.53 -
    2.54 -end
    2.55 -
    2.56 -declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
    2.57 -
    2.58 -lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
    2.59 -unfolding open_prod_def by auto
    2.60 -
    2.61 -lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
    2.62 -by auto
    2.63 -
    2.64 -lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
    2.65 -by auto
    2.66 -
    2.67 -lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
    2.68 -by (simp add: fst_vimage_eq_Times open_Times)
    2.69 -
    2.70 -lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
    2.71 -by (simp add: snd_vimage_eq_Times open_Times)
    2.72 -
    2.73 -lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
    2.74 -unfolding closed_open vimage_Compl [symmetric]
    2.75 -by (rule open_vimage_fst)
    2.76 -
    2.77 -lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
    2.78 -unfolding closed_open vimage_Compl [symmetric]
    2.79 -by (rule open_vimage_snd)
    2.80 -
    2.81 -lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    2.82 -proof -
    2.83 -  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
    2.84 -  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    2.85 -    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
    2.86 -qed
    2.87 -
    2.88 -lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
    2.89 -  unfolding image_def subset_eq by force
    2.90 -
    2.91 -lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
    2.92 -  unfolding image_def subset_eq by force
    2.93 -
    2.94 -lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
    2.95 -proof (rule openI)
    2.96 -  fix x assume "x \<in> fst ` S"
    2.97 -  then obtain y where "(x, y) \<in> S" by auto
    2.98 -  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
    2.99 -    using \<open>open S\<close> unfolding open_prod_def by auto
   2.100 -  from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
   2.101 -  with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
   2.102 -  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
   2.103 -qed
   2.104 -
   2.105 -lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
   2.106 -proof (rule openI)
   2.107 -  fix y assume "y \<in> snd ` S"
   2.108 -  then obtain x where "(x, y) \<in> S" by auto
   2.109 -  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
   2.110 -    using \<open>open S\<close> unfolding open_prod_def by auto
   2.111 -  from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
   2.112 -  with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
   2.113 -  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
   2.114 -qed
   2.115 -
   2.116 -subsubsection \<open>Continuity of operations\<close>
   2.117 -
   2.118 -lemma tendsto_fst [tendsto_intros]:
   2.119 -  assumes "(f \<longlongrightarrow> a) F"
   2.120 -  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
   2.121 -proof (rule topological_tendstoI)
   2.122 -  fix S assume "open S" and "fst a \<in> S"
   2.123 -  then have "open (fst -` S)" and "a \<in> fst -` S"
   2.124 -    by (simp_all add: open_vimage_fst)
   2.125 -  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
   2.126 -    by (rule topological_tendstoD)
   2.127 -  then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
   2.128 -    by simp
   2.129 -qed
   2.130 -
   2.131 -lemma tendsto_snd [tendsto_intros]:
   2.132 -  assumes "(f \<longlongrightarrow> a) F"
   2.133 -  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
   2.134 -proof (rule topological_tendstoI)
   2.135 -  fix S assume "open S" and "snd a \<in> S"
   2.136 -  then have "open (snd -` S)" and "a \<in> snd -` S"
   2.137 -    by (simp_all add: open_vimage_snd)
   2.138 -  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
   2.139 -    by (rule topological_tendstoD)
   2.140 -  then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
   2.141 -    by simp
   2.142 -qed
   2.143 -
   2.144 -lemma tendsto_Pair [tendsto_intros]:
   2.145 -  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
   2.146 -  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
   2.147 -proof (rule topological_tendstoI)
   2.148 -  fix S assume "open S" and "(a, b) \<in> S"
   2.149 -  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   2.150 -    unfolding open_prod_def by fast
   2.151 -  have "eventually (\<lambda>x. f x \<in> A) F"
   2.152 -    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
   2.153 -    by (rule topological_tendstoD)
   2.154 -  moreover
   2.155 -  have "eventually (\<lambda>x. g x \<in> B) F"
   2.156 -    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
   2.157 -    by (rule topological_tendstoD)
   2.158 -  ultimately
   2.159 -  show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
   2.160 -    by (rule eventually_elim2)
   2.161 -       (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
   2.162 -qed
   2.163 -
   2.164 -lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
   2.165 -  unfolding continuous_def by (rule tendsto_fst)
   2.166 -
   2.167 -lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
   2.168 -  unfolding continuous_def by (rule tendsto_snd)
   2.169 -
   2.170 -lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
   2.171 -  unfolding continuous_def by (rule tendsto_Pair)
   2.172 -
   2.173 -lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
   2.174 -  unfolding continuous_on_def by (auto intro: tendsto_fst)
   2.175 -
   2.176 -lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
   2.177 -  unfolding continuous_on_def by (auto intro: tendsto_snd)
   2.178 -
   2.179 -lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
   2.180 -  unfolding continuous_on_def by (auto intro: tendsto_Pair)
   2.181 -
   2.182 -lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
   2.183 -  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
   2.184 -
   2.185 -lemma continuous_on_swap_args:
   2.186 -  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)" 
   2.187 -    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
   2.188 -proof -
   2.189 -  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
   2.190 -    by force
   2.191 -  then show ?thesis
   2.192 -    apply (rule ssubst)
   2.193 -    apply (rule continuous_on_compose)
   2.194 -     apply (force intro: continuous_on_subset [OF continuous_on_swap])
   2.195 -    apply (force intro: continuous_on_subset [OF assms])
   2.196 -    done
   2.197 -qed
   2.198 -
   2.199 -lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
   2.200 -  by (fact continuous_fst)
   2.201 -
   2.202 -lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
   2.203 -  by (fact continuous_snd)
   2.204 -
   2.205 -lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   2.206 -  by (fact continuous_Pair)
   2.207 -
   2.208 -subsubsection \<open>Separation axioms\<close>
   2.209 -
   2.210 -instance prod :: (t0_space, t0_space) t0_space
   2.211 -proof
   2.212 -  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   2.213 -  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   2.214 -    by (simp add: prod_eq_iff)
   2.215 -  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
   2.216 -    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
   2.217 -qed
   2.218 -
   2.219 -instance prod :: (t1_space, t1_space) t1_space
   2.220 -proof
   2.221 -  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   2.222 -  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   2.223 -    by (simp add: prod_eq_iff)
   2.224 -  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
   2.225 -    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
   2.226 -qed
   2.227 -
   2.228 -instance prod :: (t2_space, t2_space) t2_space
   2.229 -proof
   2.230 -  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   2.231 -  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   2.232 -    by (simp add: prod_eq_iff)
   2.233 -  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   2.234 -    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
   2.235 -qed
   2.236 -
   2.237 -lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
   2.238 -  using continuous_on_eq_continuous_within continuous_on_swap by blast
   2.239 -
   2.240  subsection \<open>Product is a metric space\<close>
   2.241  
   2.242  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
     3.1 --- a/src/HOL/Topological_Spaces.thy	Thu Feb 18 17:53:09 2016 +0100
     3.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Feb 08 17:18:13 2016 +0100
     3.3 @@ -2610,4 +2610,254 @@
     3.4    by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
     3.5             elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
     3.6  
     3.7 +section \<open>Product Topology\<close>
     3.8 +
     3.9 +
    3.10 +subsection \<open>Product is a topological space\<close>
    3.11 +
    3.12 +instantiation prod :: (topological_space, topological_space) topological_space
    3.13 +begin
    3.14 +
    3.15 +definition open_prod_def[code del]:
    3.16 +  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
    3.17 +    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
    3.18 +
    3.19 +lemma open_prod_elim:
    3.20 +  assumes "open S" and "x \<in> S"
    3.21 +  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
    3.22 +using assms unfolding open_prod_def by fast
    3.23 +
    3.24 +lemma open_prod_intro:
    3.25 +  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
    3.26 +  shows "open S"
    3.27 +using assms unfolding open_prod_def by fast
    3.28 +
    3.29 +instance
    3.30 +proof
    3.31 +  show "open (UNIV :: ('a \<times> 'b) set)"
    3.32 +    unfolding open_prod_def by auto
    3.33 +next
    3.34 +  fix S T :: "('a \<times> 'b) set"
    3.35 +  assume "open S" "open T"
    3.36 +  show "open (S \<inter> T)"
    3.37 +  proof (rule open_prod_intro)
    3.38 +    fix x assume x: "x \<in> S \<inter> T"
    3.39 +    from x have "x \<in> S" by simp
    3.40 +    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
    3.41 +      using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
    3.42 +    from x have "x \<in> T" by simp
    3.43 +    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
    3.44 +      using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
    3.45 +    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
    3.46 +    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
    3.47 +      using A B by (auto simp add: open_Int)
    3.48 +    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
    3.49 +      by fast
    3.50 +  qed
    3.51 +next
    3.52 +  fix K :: "('a \<times> 'b) set set"
    3.53 +  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    3.54 +    unfolding open_prod_def by fast
    3.55 +qed
    3.56 +
    3.57  end
    3.58 +
    3.59 +declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
    3.60 +
    3.61 +lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
    3.62 +unfolding open_prod_def by auto
    3.63 +
    3.64 +lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
    3.65 +by auto
    3.66 +
    3.67 +lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
    3.68 +by auto
    3.69 +
    3.70 +lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
    3.71 +by (simp add: fst_vimage_eq_Times open_Times)
    3.72 +
    3.73 +lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
    3.74 +by (simp add: snd_vimage_eq_Times open_Times)
    3.75 +
    3.76 +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
    3.77 +unfolding closed_open vimage_Compl [symmetric]
    3.78 +by (rule open_vimage_fst)
    3.79 +
    3.80 +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
    3.81 +unfolding closed_open vimage_Compl [symmetric]
    3.82 +by (rule open_vimage_snd)
    3.83 +
    3.84 +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    3.85 +proof -
    3.86 +  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
    3.87 +  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    3.88 +    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
    3.89 +qed
    3.90 +
    3.91 +lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
    3.92 +  unfolding image_def subset_eq by force
    3.93 +
    3.94 +lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
    3.95 +  unfolding image_def subset_eq by force
    3.96 +
    3.97 +lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
    3.98 +proof (rule openI)
    3.99 +  fix x assume "x \<in> fst ` S"
   3.100 +  then obtain y where "(x, y) \<in> S" by auto
   3.101 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
   3.102 +    using \<open>open S\<close> unfolding open_prod_def by auto
   3.103 +  from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
   3.104 +  with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
   3.105 +  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
   3.106 +qed
   3.107 +
   3.108 +lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
   3.109 +proof (rule openI)
   3.110 +  fix y assume "y \<in> snd ` S"
   3.111 +  then obtain x where "(x, y) \<in> S" by auto
   3.112 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
   3.113 +    using \<open>open S\<close> unfolding open_prod_def by auto
   3.114 +  from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
   3.115 +  with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
   3.116 +  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
   3.117 +qed
   3.118 +
   3.119 +lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
   3.120 +  unfolding nhds_def
   3.121 +proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
   3.122 +  fix S T assume "open S" "a \<in> S" "open T" "b \<in> T"
   3.123 +  then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
   3.124 +    by (intro INF_lower) (auto intro!: open_Times)
   3.125 +next
   3.126 +  fix S' assume "open S'" "(a, b) \<in> S'"
   3.127 +  then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
   3.128 +    by (auto elim: open_prod_elim)
   3.129 +  then show "(INF x : {S. open S \<and> a \<in> S}. INF y : {S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'"
   3.130 +    by (auto intro!: INF_lower2)
   3.131 +qed
   3.132 +
   3.133 +subsubsection \<open>Continuity of operations\<close>
   3.134 +
   3.135 +lemma tendsto_fst [tendsto_intros]:
   3.136 +  assumes "(f \<longlongrightarrow> a) F"
   3.137 +  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
   3.138 +proof (rule topological_tendstoI)
   3.139 +  fix S assume "open S" and "fst a \<in> S"
   3.140 +  then have "open (fst -` S)" and "a \<in> fst -` S"
   3.141 +    by (simp_all add: open_vimage_fst)
   3.142 +  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
   3.143 +    by (rule topological_tendstoD)
   3.144 +  then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
   3.145 +    by simp
   3.146 +qed
   3.147 +
   3.148 +lemma tendsto_snd [tendsto_intros]:
   3.149 +  assumes "(f \<longlongrightarrow> a) F"
   3.150 +  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
   3.151 +proof (rule topological_tendstoI)
   3.152 +  fix S assume "open S" and "snd a \<in> S"
   3.153 +  then have "open (snd -` S)" and "a \<in> snd -` S"
   3.154 +    by (simp_all add: open_vimage_snd)
   3.155 +  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
   3.156 +    by (rule topological_tendstoD)
   3.157 +  then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
   3.158 +    by simp
   3.159 +qed
   3.160 +
   3.161 +lemma tendsto_Pair [tendsto_intros]:
   3.162 +  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
   3.163 +  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
   3.164 +proof (rule topological_tendstoI)
   3.165 +  fix S assume "open S" and "(a, b) \<in> S"
   3.166 +  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   3.167 +    unfolding open_prod_def by fast
   3.168 +  have "eventually (\<lambda>x. f x \<in> A) F"
   3.169 +    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
   3.170 +    by (rule topological_tendstoD)
   3.171 +  moreover
   3.172 +  have "eventually (\<lambda>x. g x \<in> B) F"
   3.173 +    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
   3.174 +    by (rule topological_tendstoD)
   3.175 +  ultimately
   3.176 +  show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
   3.177 +    by (rule eventually_elim2)
   3.178 +       (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
   3.179 +qed
   3.180 +
   3.181 +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
   3.182 +  unfolding continuous_def by (rule tendsto_fst)
   3.183 +
   3.184 +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
   3.185 +  unfolding continuous_def by (rule tendsto_snd)
   3.186 +
   3.187 +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
   3.188 +  unfolding continuous_def by (rule tendsto_Pair)
   3.189 +
   3.190 +lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
   3.191 +  unfolding continuous_on_def by (auto intro: tendsto_fst)
   3.192 +
   3.193 +lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
   3.194 +  unfolding continuous_on_def by (auto intro: tendsto_snd)
   3.195 +
   3.196 +lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
   3.197 +  unfolding continuous_on_def by (auto intro: tendsto_Pair)
   3.198 +
   3.199 +lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
   3.200 +  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
   3.201 +
   3.202 +lemma continuous_on_swap_args:
   3.203 +  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
   3.204 +    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
   3.205 +proof -
   3.206 +  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
   3.207 +    by force
   3.208 +  then show ?thesis
   3.209 +    apply (rule ssubst)
   3.210 +    apply (rule continuous_on_compose)
   3.211 +     apply (force intro: continuous_on_subset [OF continuous_on_swap])
   3.212 +    apply (force intro: continuous_on_subset [OF assms])
   3.213 +    done
   3.214 +qed
   3.215 +
   3.216 +lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
   3.217 +  by (fact continuous_fst)
   3.218 +
   3.219 +lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
   3.220 +  by (fact continuous_snd)
   3.221 +
   3.222 +lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   3.223 +  by (fact continuous_Pair)
   3.224 +
   3.225 +subsubsection \<open>Separation axioms\<close>
   3.226 +
   3.227 +instance prod :: (t0_space, t0_space) t0_space
   3.228 +proof
   3.229 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   3.230 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   3.231 +    by (simp add: prod_eq_iff)
   3.232 +  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
   3.233 +    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
   3.234 +qed
   3.235 +
   3.236 +instance prod :: (t1_space, t1_space) t1_space
   3.237 +proof
   3.238 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   3.239 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   3.240 +    by (simp add: prod_eq_iff)
   3.241 +  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
   3.242 +    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
   3.243 +qed
   3.244 +
   3.245 +instance prod :: (t2_space, t2_space) t2_space
   3.246 +proof
   3.247 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   3.248 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   3.249 +    by (simp add: prod_eq_iff)
   3.250 +  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   3.251 +    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
   3.252 +qed
   3.253 +
   3.254 +lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
   3.255 +  using continuous_on_eq_continuous_within continuous_on_swap by blast
   3.256 +
   3.257 +end