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