src/HOL/Topological_Spaces.thy
changeset 62367 d2bc8a7e5fec
parent 62343 24106dc44def
child 62369 acfc4ad7b76a
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Feb 18 17:53:09 2016 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Feb 08 17:18:13 2016 +0100
     1.3 @@ -2610,4 +2610,254 @@
     1.4    by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
     1.5             elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
     1.6  
     1.7 +section \<open>Product Topology\<close>
     1.8 +
     1.9 +
    1.10 +subsection \<open>Product is a topological space\<close>
    1.11 +
    1.12 +instantiation prod :: (topological_space, topological_space) topological_space
    1.13 +begin
    1.14 +
    1.15 +definition open_prod_def[code del]:
    1.16 +  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
    1.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)"
    1.18 +
    1.19 +lemma open_prod_elim:
    1.20 +  assumes "open S" and "x \<in> S"
    1.21 +  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
    1.22 +using assms unfolding open_prod_def by fast
    1.23 +
    1.24 +lemma open_prod_intro:
    1.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"
    1.26 +  shows "open S"
    1.27 +using assms unfolding open_prod_def by fast
    1.28 +
    1.29 +instance
    1.30 +proof
    1.31 +  show "open (UNIV :: ('a \<times> 'b) set)"
    1.32 +    unfolding open_prod_def by auto
    1.33 +next
    1.34 +  fix S T :: "('a \<times> 'b) set"
    1.35 +  assume "open S" "open T"
    1.36 +  show "open (S \<inter> T)"
    1.37 +  proof (rule open_prod_intro)
    1.38 +    fix x assume x: "x \<in> S \<inter> T"
    1.39 +    from x have "x \<in> S" by simp
    1.40 +    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
    1.41 +      using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
    1.42 +    from x have "x \<in> T" by simp
    1.43 +    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
    1.44 +      using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
    1.45 +    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
    1.46 +    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
    1.47 +      using A B by (auto simp add: open_Int)
    1.48 +    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
    1.49 +      by fast
    1.50 +  qed
    1.51 +next
    1.52 +  fix K :: "('a \<times> 'b) set set"
    1.53 +  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    1.54 +    unfolding open_prod_def by fast
    1.55 +qed
    1.56 +
    1.57  end
    1.58 +
    1.59 +declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
    1.60 +
    1.61 +lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
    1.62 +unfolding open_prod_def by auto
    1.63 +
    1.64 +lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
    1.65 +by auto
    1.66 +
    1.67 +lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
    1.68 +by auto
    1.69 +
    1.70 +lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
    1.71 +by (simp add: fst_vimage_eq_Times open_Times)
    1.72 +
    1.73 +lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
    1.74 +by (simp add: snd_vimage_eq_Times open_Times)
    1.75 +
    1.76 +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
    1.77 +unfolding closed_open vimage_Compl [symmetric]
    1.78 +by (rule open_vimage_fst)
    1.79 +
    1.80 +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
    1.81 +unfolding closed_open vimage_Compl [symmetric]
    1.82 +by (rule open_vimage_snd)
    1.83 +
    1.84 +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    1.85 +proof -
    1.86 +  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
    1.87 +  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    1.88 +    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
    1.89 +qed
    1.90 +
    1.91 +lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
    1.92 +  unfolding image_def subset_eq by force
    1.93 +
    1.94 +lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
    1.95 +  unfolding image_def subset_eq by force
    1.96 +
    1.97 +lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
    1.98 +proof (rule openI)
    1.99 +  fix x assume "x \<in> fst ` S"
   1.100 +  then obtain y where "(x, y) \<in> S" by auto
   1.101 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
   1.102 +    using \<open>open S\<close> unfolding open_prod_def by auto
   1.103 +  from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
   1.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
   1.105 +  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
   1.106 +qed
   1.107 +
   1.108 +lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
   1.109 +proof (rule openI)
   1.110 +  fix y assume "y \<in> snd ` S"
   1.111 +  then obtain x where "(x, y) \<in> S" by auto
   1.112 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
   1.113 +    using \<open>open S\<close> unfolding open_prod_def by auto
   1.114 +  from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
   1.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
   1.116 +  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
   1.117 +qed
   1.118 +
   1.119 +lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
   1.120 +  unfolding nhds_def
   1.121 +proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
   1.122 +  fix S T assume "open S" "a \<in> S" "open T" "b \<in> T"
   1.123 +  then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
   1.124 +    by (intro INF_lower) (auto intro!: open_Times)
   1.125 +next
   1.126 +  fix S' assume "open S'" "(a, b) \<in> S'"
   1.127 +  then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
   1.128 +    by (auto elim: open_prod_elim)
   1.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'"
   1.130 +    by (auto intro!: INF_lower2)
   1.131 +qed
   1.132 +
   1.133 +subsubsection \<open>Continuity of operations\<close>
   1.134 +
   1.135 +lemma tendsto_fst [tendsto_intros]:
   1.136 +  assumes "(f \<longlongrightarrow> a) F"
   1.137 +  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
   1.138 +proof (rule topological_tendstoI)
   1.139 +  fix S assume "open S" and "fst a \<in> S"
   1.140 +  then have "open (fst -` S)" and "a \<in> fst -` S"
   1.141 +    by (simp_all add: open_vimage_fst)
   1.142 +  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
   1.143 +    by (rule topological_tendstoD)
   1.144 +  then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
   1.145 +    by simp
   1.146 +qed
   1.147 +
   1.148 +lemma tendsto_snd [tendsto_intros]:
   1.149 +  assumes "(f \<longlongrightarrow> a) F"
   1.150 +  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
   1.151 +proof (rule topological_tendstoI)
   1.152 +  fix S assume "open S" and "snd a \<in> S"
   1.153 +  then have "open (snd -` S)" and "a \<in> snd -` S"
   1.154 +    by (simp_all add: open_vimage_snd)
   1.155 +  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
   1.156 +    by (rule topological_tendstoD)
   1.157 +  then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
   1.158 +    by simp
   1.159 +qed
   1.160 +
   1.161 +lemma tendsto_Pair [tendsto_intros]:
   1.162 +  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
   1.163 +  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
   1.164 +proof (rule topological_tendstoI)
   1.165 +  fix S assume "open S" and "(a, b) \<in> S"
   1.166 +  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   1.167 +    unfolding open_prod_def by fast
   1.168 +  have "eventually (\<lambda>x. f x \<in> A) F"
   1.169 +    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
   1.170 +    by (rule topological_tendstoD)
   1.171 +  moreover
   1.172 +  have "eventually (\<lambda>x. g x \<in> B) F"
   1.173 +    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
   1.174 +    by (rule topological_tendstoD)
   1.175 +  ultimately
   1.176 +  show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
   1.177 +    by (rule eventually_elim2)
   1.178 +       (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
   1.179 +qed
   1.180 +
   1.181 +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
   1.182 +  unfolding continuous_def by (rule tendsto_fst)
   1.183 +
   1.184 +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
   1.185 +  unfolding continuous_def by (rule tendsto_snd)
   1.186 +
   1.187 +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
   1.188 +  unfolding continuous_def by (rule tendsto_Pair)
   1.189 +
   1.190 +lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
   1.191 +  unfolding continuous_on_def by (auto intro: tendsto_fst)
   1.192 +
   1.193 +lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
   1.194 +  unfolding continuous_on_def by (auto intro: tendsto_snd)
   1.195 +
   1.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))"
   1.197 +  unfolding continuous_on_def by (auto intro: tendsto_Pair)
   1.198 +
   1.199 +lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
   1.200 +  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
   1.201 +
   1.202 +lemma continuous_on_swap_args:
   1.203 +  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
   1.204 +    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
   1.205 +proof -
   1.206 +  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
   1.207 +    by force
   1.208 +  then show ?thesis
   1.209 +    apply (rule ssubst)
   1.210 +    apply (rule continuous_on_compose)
   1.211 +     apply (force intro: continuous_on_subset [OF continuous_on_swap])
   1.212 +    apply (force intro: continuous_on_subset [OF assms])
   1.213 +    done
   1.214 +qed
   1.215 +
   1.216 +lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
   1.217 +  by (fact continuous_fst)
   1.218 +
   1.219 +lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
   1.220 +  by (fact continuous_snd)
   1.221 +
   1.222 +lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   1.223 +  by (fact continuous_Pair)
   1.224 +
   1.225 +subsubsection \<open>Separation axioms\<close>
   1.226 +
   1.227 +instance prod :: (t0_space, t0_space) t0_space
   1.228 +proof
   1.229 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   1.230 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   1.231 +    by (simp add: prod_eq_iff)
   1.232 +  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
   1.233 +    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
   1.234 +qed
   1.235 +
   1.236 +instance prod :: (t1_space, t1_space) t1_space
   1.237 +proof
   1.238 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   1.239 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   1.240 +    by (simp add: prod_eq_iff)
   1.241 +  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
   1.242 +    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
   1.243 +qed
   1.244 +
   1.245 +instance prod :: (t2_space, t2_space) t2_space
   1.246 +proof
   1.247 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
   1.248 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
   1.249 +    by (simp add: prod_eq_iff)
   1.250 +  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   1.251 +    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
   1.252 +qed
   1.253 +
   1.254 +lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
   1.255 +  using continuous_on_eq_continuous_within continuous_on_swap by blast
   1.256 +
   1.257 +end