src/HOL/Analysis/Product_Topology.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69945 35ba13ac6e5c child 69986 f2d327275065 permissions -rw-r--r--
more strict AFP properties;
```     1 section\<open>The binary product topology\<close>
```
```     2
```
```     3 theory Product_Topology
```
```     4 imports Function_Topology Abstract_Limits
```
```     5 begin
```
```     6
```
```     7 section \<open>Product Topology\<close>
```
```     8
```
```     9 subsection\<open>Definition\<close>
```
```    10
```
```    11 definition prod_topology :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<times> 'b) topology" where
```
```    12  "prod_topology X Y \<equiv> topology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
```
```    13
```
```    14 lemma open_product_open:
```
```    15   assumes "open A"
```
```    16   shows "\<exists>\<U>. \<U> \<subseteq> {S \<times> T |S T. open S \<and> open T} \<and> \<Union> \<U> = A"
```
```    17 proof -
```
```    18   obtain f g where *: "\<And>u. u \<in> A \<Longrightarrow> open (f u) \<and> open (g u) \<and> u \<in> (f u) \<times> (g u) \<and> (f u) \<times> (g u) \<subseteq> A"
```
```    19     using open_prod_def [of A] assms by metis
```
```    20   let ?\<U> = "(\<lambda>u. f u \<times> g u) ` A"
```
```    21   show ?thesis
```
```    22     by (rule_tac x="?\<U>" in exI) (auto simp: dest: *)
```
```    23 qed
```
```    24
```
```    25 lemma open_product_open_eq: "(arbitrary union_of (\<lambda>U. \<exists>S T. U = S \<times> T \<and> open S \<and> open T)) = open"
```
```    26   by (force simp: union_of_def arbitrary_def intro: open_product_open open_Times)
```
```    27
```
```    28 lemma openin_prod_topology:
```
```    29    "openin (prod_topology X Y) = arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T})"
```
```    30   unfolding prod_topology_def
```
```    31 proof (rule topology_inverse')
```
```    32   show "istopology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
```
```    33     apply (rule istopology_base, simp)
```
```    34     by (metis openin_Int Times_Int_Times)
```
```    35 qed
```
```    36
```
```    37 lemma topspace_prod_topology [simp]:
```
```    38    "topspace (prod_topology X Y) = topspace X \<times> topspace Y"
```
```    39 proof -
```
```    40   have "topspace(prod_topology X Y) = \<Union> (Collect (openin (prod_topology X Y)))" (is "_ = ?Z")
```
```    41     unfolding topspace_def ..
```
```    42   also have "\<dots> = topspace X \<times> topspace Y"
```
```    43   proof
```
```    44     show "?Z \<subseteq> topspace X \<times> topspace Y"
```
```    45       apply (auto simp: openin_prod_topology union_of_def arbitrary_def)
```
```    46       using openin_subset by force+
```
```    47   next
```
```    48     have *: "\<exists>A B. topspace X \<times> topspace Y = A \<times> B \<and> openin X A \<and> openin Y B"
```
```    49       by blast
```
```    50     show "topspace X \<times> topspace Y \<subseteq> ?Z"
```
```    51       apply (rule Union_upper)
```
```    52       using * by (simp add: openin_prod_topology arbitrary_union_of_inc)
```
```    53   qed
```
```    54   finally show ?thesis .
```
```    55 qed
```
```    56
```
```    57 lemma subtopology_Times:
```
```    58   shows "subtopology (prod_topology X Y) (S \<times> T) = prod_topology (subtopology X S) (subtopology Y T)"
```
```    59 proof -
```
```    60   have "((\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T) relative_to S \<times> T) =
```
```    61         (\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (openin Y relative_to T) T')"
```
```    62     by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis
```
```    63   then show ?thesis
```
```    64     by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to)
```
```    65 qed
```
```    66
```
```    67 lemma prod_topology_subtopology:
```
```    68     "prod_topology (subtopology X S) Y = subtopology (prod_topology X Y) (S \<times> topspace Y)"
```
```    69     "prod_topology X (subtopology Y T) = subtopology (prod_topology X Y) (topspace X \<times> T)"
```
```    70 by (auto simp: subtopology_Times)
```
```    71
```
```    72 lemma prod_topology_discrete_topology:
```
```    73      "discrete_topology (S \<times> T) = prod_topology (discrete_topology S) (discrete_topology T)"
```
```    74   by (auto simp: discrete_topology_unique openin_prod_topology intro: arbitrary_union_of_inc)
```
```    75
```
```    76 lemma prod_topology_euclidean [simp]: "prod_topology euclidean euclidean = euclidean"
```
```    77   by (simp add: prod_topology_def open_product_open_eq)
```
```    78
```
```    79 lemma prod_topology_subtopology_eu [simp]:
```
```    80   "prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
```
```    81   by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
```
```    82
```
```    83 lemma continuous_map_subtopology_eu [simp]:
```
```    84   "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
```
```    85   apply safe
```
```    86   apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
```
```    87   apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
```
```    88   by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
```
```    89
```
```    90 lemma openin_prod_topology_alt:
```
```    91      "openin (prod_topology X Y) S \<longleftrightarrow>
```
```    92       (\<forall>x y. (x,y) \<in> S \<longrightarrow> (\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> S))"
```
```    93   apply (auto simp: openin_prod_topology arbitrary_union_of_alt, fastforce)
```
```    94   by (metis mem_Sigma_iff)
```
```    95
```
```    96 lemma open_map_fst: "open_map (prod_topology X Y) X fst"
```
```    97   unfolding open_map_def openin_prod_topology_alt
```
```    98   by (force simp: openin_subopen [of X "fst ` _"] intro: subset_fst_imageI)
```
```    99
```
```   100 lemma open_map_snd: "open_map (prod_topology X Y) Y snd"
```
```   101   unfolding open_map_def openin_prod_topology_alt
```
```   102   by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI)
```
```   103
```
```   104 lemma openin_Times:
```
```   105      "openin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> openin X S \<and> openin Y T"
```
```   106 proof (cases "S = {} \<or> T = {}")
```
```   107   case False
```
```   108   then show ?thesis
```
```   109     apply (simp add: openin_prod_topology_alt openin_subopen [of X S] openin_subopen [of Y T] times_subset_iff, safe)
```
```   110       apply (meson|force)+
```
```   111     done
```
```   112 qed force
```
```   113
```
```   114
```
```   115 lemma closure_of_Times:
```
```   116    "(prod_topology X Y) closure_of (S \<times> T) = (X closure_of S) \<times> (Y closure_of T)"  (is "?lhs = ?rhs")
```
```   117 proof
```
```   118   show "?lhs \<subseteq> ?rhs"
```
```   119     by (clarsimp simp: closure_of_def openin_prod_topology_alt) blast
```
```   120   show "?rhs \<subseteq> ?lhs"
```
```   121     by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD)
```
```   122 qed
```
```   123
```
```   124 lemma closedin_Times:
```
```   125    "closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
```
```   126   by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
```
```   127
```
```   128 lemma interior_of_Times: "(prod_topology X Y) interior_of (S \<times> T) = (X interior_of S) \<times> (Y interior_of T)"
```
```   129 proof (rule interior_of_unique)
```
```   130   show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
```
```   131     by (simp add: Sigma_mono interior_of_subset)
```
```   132   show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
```
```   133     by (simp add: openin_Times)
```
```   134 next
```
```   135   show "T' \<subseteq> (X interior_of S) \<times> Y interior_of T" if "T' \<subseteq> S \<times> T" "openin (prod_topology X Y) T'" for T'
```
```   136   proof (clarsimp; intro conjI)
```
```   137     fix a :: "'a" and b :: "'b"
```
```   138     assume "(a, b) \<in> T'"
```
```   139     with that obtain U V where UV: "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> T'"
```
```   140       by (metis openin_prod_topology_alt)
```
```   141     then show "a \<in> X interior_of S"
```
```   142       using interior_of_maximal_eq that(1) by fastforce
```
```   143     show "b \<in> Y interior_of T"
```
```   144       using UV interior_of_maximal_eq that(1)
```
```   145       by (metis SigmaI mem_Sigma_iff subset_eq)
```
```   146   qed
```
```   147 qed
```
```   148
```
```   149 subsection \<open>Continuity\<close>
```
```   150
```
```   151 lemma continuous_map_pairwise:
```
```   152    "continuous_map Z (prod_topology X Y) f \<longleftrightarrow> continuous_map Z X (fst \<circ> f) \<and> continuous_map Z Y (snd \<circ> f)"
```
```   153    (is "?lhs = ?rhs")
```
```   154 proof -
```
```   155   let ?g = "fst \<circ> f" and ?h = "snd \<circ> f"
```
```   156   have f: "f x = (?g x, ?h x)" for x
```
```   157     by auto
```
```   158   show ?thesis
```
```   159   proof (cases "(\<forall>x \<in> topspace Z. ?g x \<in> topspace X) \<and> (\<forall>x \<in> topspace Z. ?h x \<in> topspace Y)")
```
```   160     case True
```
```   161     show ?thesis
```
```   162     proof safe
```
```   163       assume "continuous_map Z (prod_topology X Y) f"
```
```   164       then have "openin Z {x \<in> topspace Z. fst (f x) \<in> U}" if "openin X U" for U
```
```   165         unfolding continuous_map_def using True that
```
```   166         apply clarify
```
```   167         apply (drule_tac x="U \<times> topspace Y" in spec)
```
```   168         by (simp add: openin_Times mem_Times_iff cong: conj_cong)
```
```   169       with True show "continuous_map Z X (fst \<circ> f)"
```
```   170         by (auto simp: continuous_map_def)
```
```   171     next
```
```   172       assume "continuous_map Z (prod_topology X Y) f"
```
```   173       then have "openin Z {x \<in> topspace Z. snd (f x) \<in> V}" if "openin Y V" for V
```
```   174         unfolding continuous_map_def using True that
```
```   175         apply clarify
```
```   176         apply (drule_tac x="topspace X \<times> V" in spec)
```
```   177         by (simp add: openin_Times mem_Times_iff cong: conj_cong)
```
```   178       with True show "continuous_map Z Y (snd \<circ> f)"
```
```   179         by (auto simp: continuous_map_def)
```
```   180     next
```
```   181       assume Z: "continuous_map Z X (fst \<circ> f)" "continuous_map Z Y (snd \<circ> f)"
```
```   182       have *: "openin Z {x \<in> topspace Z. f x \<in> W}"
```
```   183         if "\<And>w. w \<in> W \<Longrightarrow> \<exists>U V. openin X U \<and> openin Y V \<and> w \<in> U \<times> V \<and> U \<times> V \<subseteq> W" for W
```
```   184       proof (subst openin_subopen, clarify)
```
```   185         fix x :: "'a"
```
```   186         assume "x \<in> topspace Z" and "f x \<in> W"
```
```   187         with that [OF \<open>f x \<in> W\<close>]
```
```   188         obtain U V where UV: "openin X U" "openin Y V" "f x \<in> U \<times> V" "U \<times> V \<subseteq> W"
```
```   189           by auto
```
```   190         with Z  UV show "\<exists>T. openin Z T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace Z. f x \<in> W}"
```
```   191           apply (rule_tac x="{x \<in> topspace Z. ?g x \<in> U} \<inter> {x \<in> topspace Z. ?h x \<in> V}" in exI)
```
```   192           apply (auto simp: \<open>x \<in> topspace Z\<close> continuous_map_def)
```
```   193           done
```
```   194       qed
```
```   195       show "continuous_map Z (prod_topology X Y) f"
```
```   196         using True by (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
```
```   197     qed
```
```   198   qed (auto simp: continuous_map_def)
```
```   199 qed
```
```   200
```
```   201 lemma continuous_map_paired:
```
```   202    "continuous_map Z (prod_topology X Y) (\<lambda>x. (f x,g x)) \<longleftrightarrow> continuous_map Z X f \<and> continuous_map Z Y g"
```
```   203   by (simp add: continuous_map_pairwise o_def)
```
```   204
```
```   205 lemma continuous_map_pairedI [continuous_intros]:
```
```   206    "\<lbrakk>continuous_map Z X f; continuous_map Z Y g\<rbrakk> \<Longrightarrow> continuous_map Z (prod_topology X Y) (\<lambda>x. (f x,g x))"
```
```   207   by (simp add: continuous_map_pairwise o_def)
```
```   208
```
```   209 lemma continuous_map_fst [continuous_intros]: "continuous_map (prod_topology X Y) X fst"
```
```   210   using continuous_map_pairwise [of "prod_topology X Y" X Y id]
```
```   211   by (simp add: continuous_map_pairwise)
```
```   212
```
```   213 lemma continuous_map_snd [continuous_intros]: "continuous_map (prod_topology X Y) Y snd"
```
```   214   using continuous_map_pairwise [of "prod_topology X Y" X Y id]
```
```   215   by (simp add: continuous_map_pairwise)
```
```   216
```
```   217 lemma continuous_map_fst_of [continuous_intros]:
```
```   218    "continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z X (fst \<circ> f)"
```
```   219   by (simp add: continuous_map_pairwise)
```
```   220
```
```   221 lemma continuous_map_snd_of [continuous_intros]:
```
```   222    "continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)"
```
```   223   by (simp add: continuous_map_pairwise)
```
```   224
```
```   225 lemma continuous_map_if_iff [simp]: "continuous_map X Y (\<lambda>x. if P then f x else g x) \<longleftrightarrow> continuous_map X Y (if P then f else g)"
```
```   226   by simp
```
```   227
```
```   228 lemma continuous_map_if [continuous_intros]: "\<lbrakk>P \<Longrightarrow> continuous_map X Y f; ~P \<Longrightarrow> continuous_map X Y g\<rbrakk>
```
```   229       \<Longrightarrow> continuous_map X Y (\<lambda>x. if P then f x else g x)"
```
```   230   by simp
```
```   231
```
```   232 lemma continuous_map_subtopology_fst [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) X fst"
```
```   233       using continuous_map_from_subtopology continuous_map_fst by force
```
```   234
```
```   235 lemma continuous_map_subtopology_snd [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) Y snd"
```
```   236       using continuous_map_from_subtopology continuous_map_snd by force
```
```   237
```
```   238 lemma quotient_map_fst [simp]:
```
```   239    "quotient_map(prod_topology X Y) X fst \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})"
```
```   240   by (auto simp: continuous_open_quotient_map open_map_fst continuous_map_fst)
```
```   241
```
```   242 lemma quotient_map_snd [simp]:
```
```   243    "quotient_map(prod_topology X Y) Y snd \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})"
```
```   244   by (auto simp: continuous_open_quotient_map open_map_snd continuous_map_snd)
```
```   245
```
```   246 lemma retraction_map_fst:
```
```   247    "retraction_map (prod_topology X Y) X fst \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})"
```
```   248 proof (cases "topspace Y = {}")
```
```   249   case True
```
```   250   then show ?thesis
```
```   251     using continuous_map_image_subset_topspace
```
```   252     by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty)
```
```   253 next
```
```   254   case False
```
```   255   have "\<exists>g. continuous_map X (prod_topology X Y) g \<and> (\<forall>x\<in>topspace X. fst (g x) = x)"
```
```   256     if y: "y \<in> topspace Y" for y
```
```   257     by (rule_tac x="\<lambda>x. (x,y)" in exI) (auto simp: y continuous_map_paired)
```
```   258   with False have "retraction_map (prod_topology X Y) X fst"
```
```   259     by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst)
```
```   260   with False show ?thesis
```
```   261     by simp
```
```   262 qed
```
```   263
```
```   264 lemma retraction_map_snd:
```
```   265    "retraction_map (prod_topology X Y) Y snd \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})"
```
```   266 proof (cases "topspace X = {}")
```
```   267   case True
```
```   268   then show ?thesis
```
```   269     using continuous_map_image_subset_topspace
```
```   270     by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty)
```
```   271 next
```
```   272   case False
```
```   273   have "\<exists>g. continuous_map Y (prod_topology X Y) g \<and> (\<forall>y\<in>topspace Y. snd (g y) = y)"
```
```   274     if x: "x \<in> topspace X" for x
```
```   275     by (rule_tac x="\<lambda>y. (x,y)" in exI) (auto simp: x continuous_map_paired)
```
```   276   with False have "retraction_map (prod_topology X Y) Y snd"
```
```   277     by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_snd)
```
```   278   with False show ?thesis
```
```   279     by simp
```
```   280 qed
```
```   281
```
```   282
```
```   283 lemma continuous_map_of_fst:
```
```   284    "continuous_map (prod_topology X Y) Z (f \<circ> fst) \<longleftrightarrow> topspace Y = {} \<or> continuous_map X Z f"
```
```   285 proof (cases "topspace Y = {}")
```
```   286   case True
```
```   287   then show ?thesis
```
```   288     by (simp add: continuous_map_on_empty)
```
```   289 next
```
```   290   case False
```
```   291   then show ?thesis
```
```   292     by (simp add: continuous_compose_quotient_map_eq quotient_map_fst)
```
```   293 qed
```
```   294
```
```   295 lemma continuous_map_of_snd:
```
```   296    "continuous_map (prod_topology X Y) Z (f \<circ> snd) \<longleftrightarrow> topspace X = {} \<or> continuous_map Y Z f"
```
```   297 proof (cases "topspace X = {}")
```
```   298   case True
```
```   299   then show ?thesis
```
```   300     by (simp add: continuous_map_on_empty)
```
```   301 next
```
```   302   case False
```
```   303   then show ?thesis
```
```   304     by (simp add: continuous_compose_quotient_map_eq quotient_map_snd)
```
```   305 qed
```
```   306
```
```   307 lemma continuous_map_prod_top:
```
```   308    "continuous_map (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) \<longleftrightarrow>
```
```   309     topspace (prod_topology X Y) = {} \<or> continuous_map X X' f \<and> continuous_map Y Y' g"
```
```   310 proof (cases "topspace (prod_topology X Y) = {}")
```
```   311   case True
```
```   312   then show ?thesis
```
```   313     by (simp add: continuous_map_on_empty)
```
```   314 next
```
```   315   case False
```
```   316   then show ?thesis
```
```   317     by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
```
```   318 qed
```
```   319
```
```   320 lemma in_prod_topology_closure_of:
```
```   321   assumes  "z \<in> (prod_topology X Y) closure_of S"
```
```   322   shows "fst z \<in> X closure_of (fst ` S)" "snd z \<in> Y closure_of (snd ` S)"
```
```   323   using assms continuous_map_eq_image_closure_subset continuous_map_fst apply fastforce
```
```   324   using assms continuous_map_eq_image_closure_subset continuous_map_snd apply fastforce
```
```   325   done
```
```   326
```
```   327
```
```   328 proposition compact_space_prod_topology:
```
```   329    "compact_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> compact_space X \<and> compact_space Y"
```
```   330 proof (cases "topspace(prod_topology X Y) = {}")
```
```   331   case True
```
```   332   then show ?thesis
```
```   333     using compact_space_topspace_empty by blast
```
```   334 next
```
```   335   case False
```
```   336   then have non_mt: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
```
```   337     by auto
```
```   338   have "compact_space X" "compact_space Y" if "compact_space(prod_topology X Y)"
```
```   339   proof -
```
```   340     have "compactin X (fst ` (topspace X \<times> topspace Y))"
```
```   341       by (metis compact_space_def continuous_map_fst image_compactin that topspace_prod_topology)
```
```   342     moreover
```
```   343     have "compactin Y (snd ` (topspace X \<times> topspace Y))"
```
```   344       by (metis compact_space_def continuous_map_snd image_compactin that topspace_prod_topology)
```
```   345     ultimately show "compact_space X" "compact_space Y"
```
```   346       by (simp_all add: non_mt compact_space_def)
```
```   347   qed
```
```   348   moreover
```
```   349   define \<X> where "\<X> \<equiv> (\<lambda>V. topspace X \<times> V) ` Collect (openin Y)"
```
```   350   define \<Y> where "\<Y> \<equiv> (\<lambda>U. U \<times> topspace Y) ` Collect (openin X)"
```
```   351   have "compact_space(prod_topology X Y)" if "compact_space X" "compact_space Y"
```
```   352   proof (rule Alexander_subbase_alt)
```
```   353     show toptop: "topspace X \<times> topspace Y \<subseteq> \<Union>(\<X> \<union> \<Y>)"
```
```   354       unfolding \<X>_def \<Y>_def by auto
```
```   355     fix \<C> :: "('a \<times> 'b) set set"
```
```   356     assume \<C>: "\<C> \<subseteq> \<X> \<union> \<Y>" "topspace X \<times> topspace Y \<subseteq> \<Union>\<C>"
```
```   357     then obtain \<X>' \<Y>' where XY: "\<X>' \<subseteq> \<X>" "\<Y>' \<subseteq> \<Y>" and \<C>eq: "\<C> = \<X>' \<union> \<Y>'"
```
```   358       using subset_UnE by metis
```
```   359     then have sub: "topspace X \<times> topspace Y \<subseteq> \<Union>(\<X>' \<union> \<Y>')"
```
```   360       using \<C> by simp
```
```   361     obtain \<U> \<V> where \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U" "\<Y>' = (\<lambda>U. U \<times> topspace Y) ` \<U>"
```
```   362       and \<V>: "\<And>V. V \<in> \<V> \<Longrightarrow> openin Y V" "\<X>' = (\<lambda>V. topspace X \<times> V) ` \<V>"
```
```   363       using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp add: subset_iff)
```
```   364     have "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<X>' \<union> \<Y>' \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>"
```
```   365     proof -
```
```   366       have "topspace X \<subseteq> \<Union>\<U> \<or> topspace Y \<subseteq> \<Union>\<V>"
```
```   367         using \<U> \<V> \<C> \<C>eq by auto
```
```   368       then have *: "\<exists>\<D>. finite \<D> \<and>
```
```   369                (\<forall>x \<in> \<D>. x \<in> (\<lambda>V. topspace X \<times> V) ` \<V> \<or> x \<in> (\<lambda>U. U \<times> topspace Y) ` \<U>) \<and>
```
```   370                (topspace X \<times> topspace Y \<subseteq> \<Union>\<D>)"
```
```   371       proof
```
```   372         assume "topspace X \<subseteq> \<Union>\<U>"
```
```   373         with \<open>compact_space X\<close> \<U> obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> \<Union>\<F>"
```
```   374           by (meson compact_space_alt)
```
```   375         with that show ?thesis
```
```   376           by (rule_tac x="(\<lambda>D. D \<times> topspace Y) ` \<F>" in exI) auto
```
```   377       next
```
```   378         assume "topspace Y \<subseteq> \<Union>\<V>"
```
```   379         with \<open>compact_space Y\<close> \<V> obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "topspace Y \<subseteq> \<Union>\<F>"
```
```   380           by (meson compact_space_alt)
```
```   381         with that show ?thesis
```
```   382           by (rule_tac x="(\<lambda>C. topspace X \<times> C) ` \<F>" in exI) auto
```
```   383       qed
```
```   384       then show ?thesis
```
```   385         using that \<U> \<V> by blast
```
```   386     qed
```
```   387     then show "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<C> \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>"
```
```   388       using \<C> \<C>eq by blast
```
```   389   next
```
```   390     have "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>) relative_to topspace X \<times> topspace Y)
```
```   391            = (\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T)"
```
```   392       (is "?lhs = ?rhs")
```
```   393     proof -
```
```   394       have "?rhs U" if "?lhs U" for U
```
```   395       proof -
```
```   396         have "topspace X \<times> topspace Y \<inter> \<Inter> T \<in> {A \<times> B |A B. A \<in> Collect (openin X) \<and> B \<in> Collect (openin Y)}"
```
```   397           if "finite T" "T \<subseteq> \<X> \<union> \<Y>" for T
```
```   398           using that
```
```   399         proof induction
```
```   400           case (insert B \<B>)
```
```   401           then show ?case
```
```   402             unfolding \<X>_def \<Y>_def
```
```   403             apply (simp add: Int_ac subset_eq image_def)
```
```   404             apply (metis (no_types) openin_Int openin_topspace Times_Int_Times)
```
```   405             done
```
```   406         qed auto
```
```   407         then show ?thesis
```
```   408           using that
```
```   409           by (auto simp: subset_eq  elim!: relative_toE intersection_ofE)
```
```   410       qed
```
```   411       moreover
```
```   412       have "?lhs Z" if Z: "?rhs Z" for Z
```
```   413       proof -
```
```   414         obtain U V where "Z = U \<times> V" "openin X U" "openin Y V"
```
```   415           using Z by blast
```
```   416         then have UV: "U \<times> V = (topspace X \<times> topspace Y) \<inter> (U \<times> V)"
```
```   417           by (simp add: Sigma_mono inf_absorb2 openin_subset)
```
```   418         moreover
```
```   419         have "?lhs ((topspace X \<times> topspace Y) \<inter> (U \<times> V))"
```
```   420         proof (rule relative_to_inc)
```
```   421           show "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>)) (U \<times> V)"
```
```   422             apply (simp add: intersection_of_def \<X>_def \<Y>_def)
```
```   423             apply (rule_tac x="{(U \<times> topspace Y),(topspace X \<times> V)}" in exI)
```
```   424             using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp add:)
```
```   425             done
```
```   426         qed
```
```   427         ultimately show ?thesis
```
```   428           using \<open>Z = U \<times> V\<close> by auto
```
```   429       qed
```
```   430       ultimately show ?thesis
```
```   431         by meson
```
```   432     qed
```
```   433     then show "topology (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<X> \<union> \<Y>)
```
```   434            relative_to (topspace X \<times> topspace Y))) =
```
```   435         prod_topology X Y"
```
```   436       by (simp add: prod_topology_def)
```
```   437   qed
```
```   438   ultimately show ?thesis
```
```   439     using False by blast
```
```   440 qed
```
```   441
```
```   442 lemma compactin_Times:
```
```   443    "compactin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> compactin X S \<and> compactin Y T"
```
```   444   by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology)
```
```   445
```
```   446 subsection\<open>Homeomorphic maps\<close>
```
```   447
```
```   448 lemma homeomorphic_maps_prod:
```
```   449    "homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
```
```   450         topspace(prod_topology X Y) = {} \<and>
```
```   451         topspace(prod_topology X' Y') = {} \<or>
```
```   452         homeomorphic_maps X X' f f' \<and>
```
```   453         homeomorphic_maps Y Y' g g'"
```
```   454   unfolding homeomorphic_maps_def continuous_map_prod_top
```
```   455   by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
```
```   456
```
```   457 lemma embedding_map_graph:
```
```   458    "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
```
```   459     (is "?lhs = ?rhs")
```
```   460 proof
```
```   461   assume L: ?lhs
```
```   462   have "snd \<circ> (\<lambda>x. (x, f x)) = f"
```
```   463     by force
```
```   464   moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
```
```   465     using L
```
```   466     unfolding embedding_map_def
```
```   467     by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
```
```   468   ultimately show ?rhs
```
```   469     by simp
```
```   470 next
```
```   471   assume R: ?rhs
```
```   472   then show ?lhs
```
```   473     unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
```
```   474     by (rule_tac x=fst in exI)
```
```   475        (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
```
```   476                    continuous_map_fst topspace_subtopology)
```
```   477 qed
```
```   478
```
```   479 lemma homeomorphic_space_prod_topology:
```
```   480    "\<lbrakk>X homeomorphic_space X''; Y homeomorphic_space Y'\<rbrakk>
```
```   481         \<Longrightarrow> prod_topology X Y homeomorphic_space prod_topology X'' Y'"
```
```   482 using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast
```
```   483
```
```   484 lemma prod_topology_homeomorphic_space_left:
```
```   485    "topspace Y = {b} \<Longrightarrow> prod_topology X Y homeomorphic_space X"
```
```   486   unfolding homeomorphic_space_def
```
```   487   by (rule_tac x=fst in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
```
```   488
```
```   489 lemma prod_topology_homeomorphic_space_right:
```
```   490    "topspace X = {a} \<Longrightarrow> prod_topology X Y homeomorphic_space Y"
```
```   491   unfolding homeomorphic_space_def
```
```   492   by (rule_tac x=snd in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
```
```   493
```
```   494
```
```   495 lemma homeomorphic_space_prod_topology_sing1:
```
```   496      "b \<in> topspace Y \<Longrightarrow> X homeomorphic_space (prod_topology X (subtopology Y {b}))"
```
```   497   by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_left topspace_subtopology)
```
```   498
```
```   499 lemma homeomorphic_space_prod_topology_sing2:
```
```   500      "a \<in> topspace X \<Longrightarrow> Y homeomorphic_space (prod_topology (subtopology X {a}) Y)"
```
```   501   by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_right topspace_subtopology)
```
```   502
```
```   503 lemma topological_property_of_prod_component:
```
```   504   assumes major: "P(prod_topology X Y)"
```
```   505     and X: "\<And>x. \<lbrakk>x \<in> topspace X; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) ({x} \<times> topspace Y))"
```
```   506     and Y: "\<And>y. \<lbrakk>y \<in> topspace Y; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) (topspace X \<times> {y}))"
```
```   507     and PQ:  "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
```
```   508     and PR: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> R X')"
```
```   509   shows "topspace(prod_topology X Y) = {} \<or> Q X \<and> R Y"
```
```   510 proof -
```
```   511   have "Q X \<and> R Y" if "topspace(prod_topology X Y) \<noteq> {}"
```
```   512   proof -
```
```   513     from that obtain a b where a: "a \<in> topspace X" and b: "b \<in> topspace Y"
```
```   514       by force
```
```   515     show ?thesis
```
```   516       using X [OF a major] and Y [OF b major] homeomorphic_space_prod_topology_sing1 [OF b, of X] homeomorphic_space_prod_topology_sing2 [OF a, of Y]
```
```   517       by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym)
```
```   518   qed
```
```   519   then show ?thesis by metis
```
```   520 qed
```
```   521
```
```   522 lemma limitin_pairwise:
```
```   523    "limitin (prod_topology X Y) f l F \<longleftrightarrow> limitin X (fst \<circ> f) (fst l) F \<and> limitin Y (snd \<circ> f) (snd l) F"
```
```   524     (is "?lhs = ?rhs")
```
```   525 proof
```
```   526   assume ?lhs
```
```   527   then obtain a b where ev: "\<And>U. \<lbrakk>(a,b) \<in> U; openin (prod_topology X Y) U\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in F. f x \<in> U"
```
```   528                         and a: "a \<in> topspace X" and b: "b \<in> topspace Y" and l: "l = (a,b)"
```
```   529     by (auto simp: limitin_def)
```
```   530   moreover have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" if "openin X U" "a \<in> U" for U
```
```   531   proof -
```
```   532     have "\<forall>\<^sub>F c in F. f c \<in> U \<times> topspace Y"
```
```   533       using b that ev [of "U \<times> topspace Y"] by (auto simp: openin_prod_topology_alt)
```
```   534     then show ?thesis
```
```   535       by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
```
```   536   qed
```
```   537   moreover have "\<forall>\<^sub>F x in F. snd (f x) \<in> U" if "openin Y U" "b \<in> U" for U
```
```   538   proof -
```
```   539     have "\<forall>\<^sub>F c in F. f c \<in> topspace X \<times> U"
```
```   540       using a that ev [of "topspace X \<times> U"] by (auto simp: openin_prod_topology_alt)
```
```   541     then show ?thesis
```
```   542       by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
```
```   543   qed
```
```   544   ultimately show ?rhs
```
```   545     by (simp add: limitin_def)
```
```   546 next
```
```   547   have "limitin (prod_topology X Y) f (a,b) F"
```
```   548     if "limitin X (fst \<circ> f) a F" "limitin Y (snd \<circ> f) b F" for a b
```
```   549     using that
```
```   550   proof (clarsimp simp: limitin_def)
```
```   551     fix Z :: "('a \<times> 'b) set"
```
```   552     assume a: "a \<in> topspace X" "\<forall>U. openin X U \<and> a \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. fst (f x) \<in> U)"
```
```   553       and b: "b \<in> topspace Y" "\<forall>U. openin Y U \<and> b \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. snd (f x) \<in> U)"
```
```   554       and Z: "openin (prod_topology X Y) Z" "(a, b) \<in> Z"
```
```   555     then obtain U V where "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> Z"
```
```   556       using Z by (force simp: openin_prod_topology_alt)
```
```   557     then have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" "\<forall>\<^sub>F x in F. snd (f x) \<in> V"
```
```   558       by (simp_all add: a b)
```
```   559     then show "\<forall>\<^sub>F x in F. f x \<in> Z"
```
```   560       by (rule eventually_elim2) (use \<open>U \<times> V \<subseteq> Z\<close> subsetD in auto)
```
```   561   qed
```
```   562   then show "?rhs \<Longrightarrow> ?lhs"
```
```   563     by (metis prod.collapse)
```
```   564 qed
```
```   565
```
```   566 end
```
```   567
```