--- a/src/HOL/Topological_Spaces.thy Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Feb 08 17:18:13 2016 +0100
@@ -2610,4 +2610,254 @@
by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
+section \<open>Product Topology\<close>
+
+
+subsection \<open>Product is a topological space\<close>
+
+instantiation prod :: (topological_space, topological_space) topological_space
+begin
+
+definition open_prod_def[code del]:
+ "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
+ (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
+
+lemma open_prod_elim:
+ assumes "open S" and "x \<in> S"
+ obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
+using assms unfolding open_prod_def by fast
+
+lemma open_prod_intro:
+ 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"
+ shows "open S"
+using assms unfolding open_prod_def by fast
+
+instance
+proof
+ show "open (UNIV :: ('a \<times> 'b) set)"
+ unfolding open_prod_def by auto
+next
+ fix S T :: "('a \<times> 'b) set"
+ assume "open S" "open T"
+ show "open (S \<inter> T)"
+ proof (rule open_prod_intro)
+ fix x assume x: "x \<in> S \<inter> T"
+ from x have "x \<in> S" by simp
+ obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
+ using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
+ from x have "x \<in> T" by simp
+ obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
+ using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
+ let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
+ have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
+ using A B by (auto simp add: open_Int)
+ thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
+ by fast
+ qed
+next
+ fix K :: "('a \<times> 'b) set set"
+ assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+ unfolding open_prod_def by fast
+qed
+
end
+
+declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
+
+lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
+unfolding open_prod_def by auto
+
+lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
+by auto
+
+lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
+by auto
+
+lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
+by (simp add: fst_vimage_eq_Times open_Times)
+
+lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
+by (simp add: snd_vimage_eq_Times open_Times)
+
+lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_fst)
+
+lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_snd)
+
+lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+proof -
+ have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
+ thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+ by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
+qed
+
+lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
+ unfolding image_def subset_eq by force
+
+lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
+ unfolding image_def subset_eq by force
+
+lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
+proof (rule openI)
+ fix x assume "x \<in> fst ` S"
+ then obtain y where "(x, y) \<in> S" by auto
+ then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+ using \<open>open S\<close> unfolding open_prod_def by auto
+ from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
+ with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
+ then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
+qed
+
+lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
+proof (rule openI)
+ fix y assume "y \<in> snd ` S"
+ then obtain x where "(x, y) \<in> S" by auto
+ then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+ using \<open>open S\<close> unfolding open_prod_def by auto
+ from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
+ with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
+ then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
+qed
+
+lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
+ unfolding nhds_def
+proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
+ fix S T assume "open S" "a \<in> S" "open T" "b \<in> T"
+ then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
+ by (intro INF_lower) (auto intro!: open_Times)
+next
+ fix S' assume "open S'" "(a, b) \<in> S'"
+ then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
+ by (auto elim: open_prod_elim)
+ 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'"
+ by (auto intro!: INF_lower2)
+qed
+
+subsubsection \<open>Continuity of operations\<close>
+
+lemma tendsto_fst [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "fst a \<in> S"
+ then have "open (fst -` S)" and "a \<in> fst -` S"
+ by (simp_all add: open_vimage_fst)
+ with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
+ by simp
+qed
+
+lemma tendsto_snd [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "snd a \<in> S"
+ then have "open (snd -` S)" and "a \<in> snd -` S"
+ by (simp_all add: open_vimage_snd)
+ with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
+ by simp
+qed
+
+lemma tendsto_Pair [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
+ shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "(a, b) \<in> S"
+ then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
+ unfolding open_prod_def by fast
+ have "eventually (\<lambda>x. f x \<in> A) F"
+ using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
+ by (rule topological_tendstoD)
+ moreover
+ have "eventually (\<lambda>x. g x \<in> B) F"
+ using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
+ by (rule topological_tendstoD)
+ ultimately
+ show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
+ by (rule eventually_elim2)
+ (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
+qed
+
+lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+ unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+ unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+ unfolding continuous_def by (rule tendsto_Pair)
+
+lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_fst)
+
+lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_snd)
+
+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))"
+ unfolding continuous_on_def by (auto intro: tendsto_Pair)
+
+lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
+ by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
+
+lemma continuous_on_swap_args:
+ assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
+ shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
+proof -
+ have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
+ by force
+ then show ?thesis
+ apply (rule ssubst)
+ apply (rule continuous_on_compose)
+ apply (force intro: continuous_on_subset [OF continuous_on_swap])
+ apply (force intro: continuous_on_subset [OF assms])
+ done
+qed
+
+lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
+ by (fact continuous_fst)
+
+lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
+ by (fact continuous_snd)
+
+lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+ by (fact continuous_Pair)
+
+subsubsection \<open>Separation axioms\<close>
+
+instance prod :: (t0_space, t0_space) t0_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
+ by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t1_space, t1_space) t1_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+ by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t2_space, t2_space) t2_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
+qed
+
+lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
+ using continuous_on_eq_continuous_within continuous_on_swap by blast
+
+end