src/HOL/Analysis/Function_Topology.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69945 35ba13ac6e5c
child 69994 cf7150ab1075
permissions -rw-r--r--
more strict AFP properties;
lp15@69030
     1
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP
hoelzl@64289
     2
    License: BSD
hoelzl@64289
     3
*)
hoelzl@64289
     4
hoelzl@64289
     5
theory Function_Topology
lp15@69945
     6
imports Topology_Euclidean_Space Abstract_Limits
hoelzl@64289
     7
begin
hoelzl@64289
     8
hoelzl@64289
     9
lp15@69939
    10
section \<open>Function Topology\<close>
hoelzl@64289
    11
lp15@69922
    12
text \<open>We want to define the general product topology.
hoelzl@64289
    13
hoelzl@64289
    14
The product topology on a product of topological spaces is generated by
hoelzl@64289
    15
the sets which are products of open sets along finitely many coordinates, and the whole
hoelzl@64289
    16
space along the other coordinates. This is the coarsest topology for which the projection
hoelzl@64289
    17
to each factor is continuous.
hoelzl@64289
    18
hoelzl@64289
    19
To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
wenzelm@69597
    20
'a. The product is then \<^term>\<open>Pi\<^sub>E I X\<close>, the set of elements from \<open>'i\<close> to \<open>'a\<close> such that the \<open>i\<close>-th
wenzelm@69566
    21
coordinate belongs to \<open>X i\<close> for all \<open>i \<in> I\<close>.
hoelzl@64289
    22
hoelzl@64289
    23
Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
hoelzl@64289
    24
This means that type classes can not be used to define such a product if one wants to take the
hoelzl@64289
    25
product of different topological spaces (as the type 'a can only be given one structure of
hoelzl@64289
    26
topological space using type classes). On the other hand, one can define different topologies (as
wenzelm@69566
    27
introduced in \<open>thy\<close>) on one type, and these topologies do not need to
hoelzl@64289
    28
share the same maximal open set. Hence, one can form a product of topologies in this sense, and
hoelzl@64289
    29
this works well. The big caveat is that it does not interact well with the main body of
hoelzl@64289
    30
topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
hoelzl@64289
    31
is not defined in this setting.
hoelzl@64289
    32
hoelzl@64289
    33
As the product of different topological spaces is very important in several areas of
hoelzl@64289
    34
mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
hoelzl@64289
    35
and reformulate afterwards the consequences in terms of type classes (which are of course very
hoelzl@64289
    36
handy for applications).
hoelzl@64289
    37
hoelzl@64289
    38
Given this limitation, it looks to me that it would be very beneficial to revamp the theory
hoelzl@64289
    39
of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
hoelzl@64289
    40
type classes as consequences of more general statements in terms of topologies (but I am
hoelzl@64289
    41
probably too naive here).
hoelzl@64289
    42
hoelzl@64289
    43
Here is an example of a reformulation using topologies. Let
wenzelm@69566
    44
@{text [display]
lp15@69939
    45
\<open>continuous_map T1 T2 f =
wenzelm@69566
    46
    ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
wenzelm@69566
    47
            \<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
wenzelm@69566
    48
be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
wenzelm@69566
    49
the current \<open>continuous_on\<close> (with type classes) can be redefined as
wenzelm@69566
    50
@{text [display] \<open>continuous_on s f =
lp15@69939
    51
    continuous_map (top_of_set s) (topology euclidean) f\<close>}
hoelzl@64289
    52
lp15@69939
    53
In fact, I need \<open>continuous_map\<close> to express the continuity of the projection on subfactors
wenzelm@69566
    54
for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
lp15@69939
    55
the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.
hoelzl@64289
    56
hoelzl@64289
    57
I only develop the basics of the product topology in this theory. The most important missing piece
hoelzl@64289
    58
is Tychonov theorem, stating that a product of compact spaces is always compact for the product
hoelzl@64289
    59
topology, even when the product is not finite (or even countable).
hoelzl@64289
    60
wenzelm@69566
    61
I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
wenzelm@64911
    62
\<close>
hoelzl@64289
    63
immler@69683
    64
subsection \<open>The product topology\<close>
hoelzl@64289
    65
wenzelm@64911
    66
text \<open>We can now define the product topology, as generated by
hoelzl@64289
    67
the sets which are products of open sets along finitely many coordinates, and the whole
hoelzl@64289
    68
space along the other coordinates. Equivalently, it is generated by sets which are one open
hoelzl@64289
    69
set along one single coordinate, and the whole space along other coordinates. In fact, this is only
hoelzl@64289
    70
equivalent for nonempty products, but for the empty product the first formulation is better
hoelzl@64289
    71
(the second one gives an empty product space, while an empty product should have exactly one
wenzelm@69566
    72
point, equal to \<open>undefined\<close> along all coordinates.
hoelzl@64289
    73
hoelzl@64289
    74
So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
wenzelm@64911
    75
\<close>
hoelzl@64289
    76
ak2110@68833
    77
definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
hoelzl@64289
    78
  where "product_topology T I =
hoelzl@64289
    79
    topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
hoelzl@64289
    80
wenzelm@64911
    81
text \<open>The total set of the product topology is the product of the total sets
wenzelm@64911
    82
along each coordinate.\<close>
hoelzl@64289
    83
lp15@69030
    84
proposition product_topology:
lp15@69030
    85
  "product_topology X I =
lp15@69030
    86
   topology
lp15@69030
    87
    (arbitrary union_of
lp15@69030
    88
       ((finite intersection_of
lp15@69030
    89
        (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
lp15@69030
    90
        relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
lp15@69030
    91
  (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
lp15@69030
    92
proof -
lp15@69030
    93
  let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"
lp15@69030
    94
  have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
lp15@69030
    95
  proof -
lp15@69030
    96
    have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
lp15@69030
    97
      if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
lp15@69030
    98
    proof -
lp15@69030
    99
      have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"
lp15@69030
   100
        using \<U> by auto
lp15@69030
   101
      then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"
lp15@69030
   102
        by metis
lp15@69030
   103
      obtain U where "U \<in> \<U>"
lp15@69030
   104
        using \<open>\<U> \<noteq> {}\<close> by blast
lp15@69030
   105
      let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
lp15@69030
   106
      show ?thesis
lp15@69030
   107
      proof (intro conjI exI)
lp15@69030
   108
        show "finite (\<Union>U\<in>\<U>. ?F U)"
lp15@69030
   109
          using Y \<open>finite' \<U>\<close> by auto
lp15@69030
   110
        show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
lp15@69030
   111
        proof
lp15@69030
   112
          have *: "f \<in> U"
lp15@69030
   113
            if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
lp15@69030
   114
              and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
lp15@69030
   115
          proof -
lp15@69030
   116
            have "Pi\<^sub>E I (Y U) = U"
lp15@69030
   117
              using Y \<open>U \<in> \<U>\<close> by blast
lp15@69030
   118
            then show "f \<in> U"
lp15@69030
   119
              using that unfolding PiE_def Pi_def by blast
lp15@69030
   120
          qed
lp15@69030
   121
          show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
lp15@69030
   122
            by (auto simp: PiE_iff *)
lp15@69030
   123
          show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
lp15@69030
   124
            using Y openin_subset \<open>finite' \<U>\<close> by fastforce
lp15@69030
   125
        qed
lp15@69030
   126
      qed (use Y openin_subset in \<open>blast+\<close>)
lp15@69030
   127
    qed
lp15@69030
   128
    have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   129
      if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
lp15@69030
   130
    proof (cases "\<U>={}")
lp15@69030
   131
      case True
lp15@69030
   132
      then show ?thesis
lp15@69030
   133
        apply (rule_tac x="{?TOP}" in exI, simp)
lp15@69030
   134
        apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
lp15@69030
   135
        apply force
lp15@69030
   136
        done
lp15@69030
   137
    next
lp15@69030
   138
      case False
lp15@69030
   139
      then obtain U where "U \<in> \<U>"
lp15@69030
   140
        by blast
lp15@69030
   141
      have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
lp15@69030
   142
        using \<U> by auto
lp15@69030
   143
      then obtain J Y where
lp15@69030
   144
        Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"
lp15@69030
   145
        by metis
lp15@69030
   146
      let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
lp15@69030
   147
      show ?thesis
lp15@69030
   148
      proof (intro conjI exI)
lp15@69030
   149
        show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
lp15@69030
   150
          using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
lp15@69030
   151
        have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
lp15@69030
   152
          using Y by force
lp15@69030
   153
        show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
lp15@69030
   154
          apply clarsimp
lp15@69030
   155
          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
lp15@69030
   156
          apply (auto simp: *)
lp15@69030
   157
          done
lp15@69030
   158
      next
lp15@69030
   159
        show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   160
        proof
lp15@69030
   161
          have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69030
   162
            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
lp15@69030
   163
            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
lp15@69030
   164
          then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
lp15@69030
   165
            using \<open>U \<in> \<U>\<close>
lp15@69030
   166
            by fastforce
lp15@69030
   167
          moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
lp15@69030
   168
            using PiE_mem Y by fastforce
lp15@69030
   169
          ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
lp15@69030
   170
            by auto
lp15@69030
   171
        qed (use Y in fastforce)
lp15@69030
   172
      qed
lp15@69030
   173
    qed
lp15@69030
   174
    show ?thesis
lp15@69030
   175
      unfolding relative_to_def intersection_of_def
lp15@69030
   176
      by (safe; blast dest!: 1 2)
lp15@69030
   177
  qed
lp15@69030
   178
  show ?thesis
lp15@69030
   179
    unfolding product_topology_def generate_topology_on_eq
lp15@69030
   180
    apply (rule arg_cong [where f = topology])
lp15@69030
   181
    apply (rule arg_cong [where f = "(union_of)arbitrary"])
lp15@69030
   182
    apply (force simp: *)
lp15@69030
   183
    done
lp15@69030
   184
qed
lp15@69030
   185
lp15@69874
   186
lemma topspace_product_topology [simp]:
hoelzl@64289
   187
  "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
immler@69681
   188
proof
hoelzl@64289
   189
  show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
lp15@69030
   190
    unfolding product_topology_def topology_generated_by_topspace
hoelzl@64289
   191
    unfolding topspace_def by auto
hoelzl@64289
   192
  have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
hoelzl@64289
   193
    using openin_topspace not_finite_existsD by auto
hoelzl@64289
   194
  then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
hoelzl@64289
   195
    unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
hoelzl@64289
   196
qed
hoelzl@64289
   197
immler@69681
   198
lemma product_topology_basis:
hoelzl@64289
   199
  assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
hoelzl@64289
   200
  shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
lp15@69030
   201
  unfolding product_topology_def
lp15@69030
   202
  by (rule topology_generated_by_Basis) (use assms in auto)
hoelzl@64289
   203
immler@69681
   204
proposition product_topology_open_contains_basis:
lp15@69030
   205
  assumes "openin (product_topology T I) U" "x \<in> U"
hoelzl@64289
   206
  shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
immler@69681
   207
proof -
hoelzl@64289
   208
  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
hoelzl@64289
   209
    using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
hoelzl@64289
   210
  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
hoelzl@64289
   211
  proof induction
hoelzl@64289
   212
    case (Int U V x)
hoelzl@64289
   213
    then obtain XU XV where H:
hoelzl@64289
   214
      "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
hoelzl@64289
   215
      "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
hoelzl@64289
   216
      by auto meson
hoelzl@64289
   217
    define X where "X = (\<lambda>i. XU i \<inter> XV i)"
hoelzl@64289
   218
    have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
hoelzl@64289
   219
      unfolding X_def by (auto simp add: PiE_iff)
hoelzl@64289
   220
    then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
hoelzl@64289
   221
    moreover have "\<forall>i. openin (T i) (X i)"
hoelzl@64289
   222
      unfolding X_def using H by auto
hoelzl@64289
   223
    moreover have "finite {i. X i \<noteq> topspace (T i)}"
hoelzl@64289
   224
      apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
hoelzl@64289
   225
      unfolding X_def using H by auto
hoelzl@64289
   226
    moreover have "x \<in> Pi\<^sub>E I X"
hoelzl@64289
   227
      unfolding X_def using H by auto
hoelzl@64289
   228
    ultimately show ?case
hoelzl@64289
   229
      by auto
hoelzl@64289
   230
  next
hoelzl@64289
   231
    case (UN K x)
hoelzl@64289
   232
    then obtain k where "k \<in> K" "x \<in> k" by auto
hoelzl@64289
   233
    with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
hoelzl@64289
   234
      by simp
hoelzl@64289
   235
    then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
hoelzl@64289
   236
      by blast
hoelzl@64289
   237
    then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
wenzelm@64911
   238
      using \<open>k \<in> K\<close> by auto
hoelzl@64289
   239
    then show ?case
hoelzl@64289
   240
      by auto
hoelzl@64289
   241
  qed auto
wenzelm@64911
   242
  then show ?thesis using \<open>x \<in> U\<close> by auto
hoelzl@64289
   243
qed
hoelzl@64289
   244
lp15@69922
   245
lemma product_topology_empty_discrete:
lp15@69922
   246
   "product_topology T {} = discrete_topology {(\<lambda>x. undefined)}"
lp15@69922
   247
  by (simp add: subtopology_eq_discrete_topology_sing)
hoelzl@64289
   248
lp15@69030
   249
lemma openin_product_topology:
lp15@69030
   250
   "openin (product_topology X I) =
lp15@69030
   251
    arbitrary union_of
lp15@69030
   252
          ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
lp15@69030
   253
           relative_to topspace (product_topology X I))"
lp15@69030
   254
  apply (subst product_topology)
lp15@69939
   255
  apply (simp add: topology_inverse' [OF istopology_subbase])
lp15@69030
   256
  done
lp15@69030
   257
lp15@69030
   258
lemma subtopology_PiE:
lp15@69030
   259
  "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
lp15@69030
   260
proof -
lp15@69030
   261
  let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
lp15@69030
   262
  let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
lp15@69030
   263
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
lp15@69030
   264
        finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   265
    by (rule finite_intersection_of_relative_to)
lp15@69030
   266
  also have "\<dots> = finite intersection_of
lp15@69030
   267
                      ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
lp15@69030
   268
                       relative_to ?X \<inter> Pi\<^sub>E I S)
lp15@69030
   269
                   relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   270
    apply (rule arg_cong2 [where f = "(relative_to)"])
lp15@69030
   271
     apply (rule arg_cong [where f = "(intersection_of)finite"])
lp15@69030
   272
     apply (rule ext)
lp15@69030
   273
     apply (auto simp: relative_to_def intersection_of_def)
lp15@69030
   274
    done
lp15@69030
   275
  finally
lp15@69030
   276
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
lp15@69030
   277
        finite intersection_of
lp15@69030
   278
          (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
lp15@69030
   279
          relative_to ?X \<inter> Pi\<^sub>E I S"
lp15@69030
   280
    by (metis finite_intersection_of_relative_to)
lp15@69030
   281
  then show ?thesis
lp15@69030
   282
  unfolding topology_eq
lp15@69030
   283
  apply clarify
lp15@69030
   284
  apply (simp add: openin_product_topology flip: openin_relative_to)
lp15@69030
   285
  apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
lp15@69030
   286
  done
lp15@69030
   287
qed
lp15@69030
   288
lp15@69030
   289
lemma product_topology_base_alt:
lp15@69030
   290
   "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
lp15@69939
   291
    relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
lp15@69030
   292
    (\<lambda>F. (\<exists>U. F =  Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
lp15@69030
   293
   (is "?lhs = ?rhs")
lp15@69030
   294
proof -
lp15@69030
   295
  have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
lp15@69030
   296
    unfolding all_relative_to all_intersection_of topspace_product_topology
lp15@69030
   297
  proof clarify
lp15@69030
   298
    fix \<F>
lp15@69030
   299
    assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
lp15@69030
   300
    then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
lp15@69030
   301
          finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
lp15@69030
   302
    proof (induction)
lp15@69030
   303
      case (insert F \<F>)
lp15@69030
   304
      then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
lp15@69030
   305
        and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
lp15@69030
   306
        and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
lp15@69030
   307
        by auto
lp15@69030
   308
      obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
lp15@69030
   309
        using insert by auto
lp15@69030
   310
      let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
lp15@69030
   311
      show ?case
lp15@69030
   312
      proof (intro exI conjI)
nipkow@69745
   313
        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
lp15@69030
   314
        using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
lp15@69030
   315
      next
lp15@69030
   316
        show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
lp15@69030
   317
          by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
lp15@69030
   318
      next
lp15@69030
   319
        show "\<forall>i\<in>I. openin (X i) (?U i)"
lp15@69030
   320
          by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
lp15@69030
   321
      qed
lp15@69030
   322
    qed (auto intro: dest: not_finite_existsD)
lp15@69030
   323
  qed
lp15@69030
   324
  moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
lp15@69030
   325
  proof clarify
lp15@69030
   326
    fix U :: "'a \<Rightarrow> 'b set"
lp15@69030
   327
    assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
lp15@69030
   328
    let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
lp15@69030
   329
    show "?lhs (Pi\<^sub>E I U)"
lp15@69030
   330
      unfolding relative_to_def topspace_product_topology
lp15@69030
   331
    proof (intro exI conjI)
lp15@69030
   332
      show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"
lp15@69030
   333
        using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
lp15@69030
   334
      show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
lp15@69030
   335
        using ope openin_subset by fastforce
lp15@69030
   336
    qed
lp15@69030
   337
  qed
lp15@69030
   338
  ultimately show ?thesis
lp15@69030
   339
    by meson
lp15@69030
   340
qed
lp15@69030
   341
lp15@69939
   342
corollary openin_product_topology_alt:
lp15@69939
   343
  "openin (product_topology X I) S \<longleftrightarrow>
lp15@69939
   344
    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
lp15@69939
   345
                 (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
lp15@69939
   346
  unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
lp15@69939
   347
  apply safe
lp15@69939
   348
  apply (drule bspec; blast)+
lp15@69939
   349
  done
lp15@69939
   350
lp15@69874
   351
lemma closure_of_product_topology:
lp15@69874
   352
  "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
lp15@69874
   353
proof -
lp15@69874
   354
  have *: "(\<forall>T. f \<in> T \<and> openin (product_topology X I) T \<longrightarrow> (\<exists>y\<in>Pi\<^sub>E I S. y \<in> T))
lp15@69874
   355
       \<longleftrightarrow> (\<forall>i \<in> I. \<forall>T. f i \<in> T \<and> openin (X i) T \<longrightarrow> S i \<inter> T \<noteq> {})"
lp15@69874
   356
    (is "?lhs = ?rhs")
lp15@69874
   357
    if top: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)" and ext:  "f \<in> extensional I" for f
lp15@69874
   358
  proof
lp15@69874
   359
    assume L[rule_format]: ?lhs
lp15@69874
   360
    show ?rhs
lp15@69874
   361
    proof clarify
lp15@69874
   362
      fix i T
lp15@69874
   363
      assume "i \<in> I" "f i \<in> T" "openin (X i) T" "S i \<inter> T = {}"
lp15@69874
   364
      then have "openin (product_topology X I) ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> {x. x i \<in> T})"
lp15@69874
   365
        by (force simp: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)
lp15@69874
   366
      then show "False"
lp15@69874
   367
        using L [of "topspace (product_topology X I) \<inter> {f. f i \<in> T}"] \<open>S i \<inter> T = {}\<close> \<open>f i \<in> T\<close> \<open>i \<in> I\<close>
lp15@69874
   368
        by (auto simp: top ext PiE_iff)
lp15@69874
   369
    qed
lp15@69874
   370
  next
lp15@69874
   371
    assume R [rule_format]: ?rhs
lp15@69874
   372
    show ?lhs
lp15@69874
   373
    proof (clarsimp simp: openin_product_topology union_of_def arbitrary_def)
lp15@69874
   374
      fix \<U> U
lp15@69874
   375
      assume
lp15@69874
   376
        \<U>: "\<U> \<subseteq> Collect
lp15@69874
   377
           (finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
lp15@69874
   378
            (\<Pi>\<^sub>E i\<in>I. topspace (X i)))" and
lp15@69874
   379
        "f \<in> U" "U \<in> \<U>"
lp15@69874
   380
      then have "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U)
lp15@69874
   381
                 relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))) U"
lp15@69874
   382
        by blast
lp15@69874
   383
      with \<open>f \<in> U\<close> \<open>U \<in> \<U>\<close>
lp15@69874
   384
      obtain \<T> where "finite \<T>"
lp15@69874
   385
        and \<T>: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i \<in> I. \<exists>V. openin (X i) V \<and> C = {x. x i \<in> V}"
lp15@69874
   386
        and "topspace (product_topology X I) \<inter> \<Inter> \<T> \<subseteq> U" "f \<in> topspace (product_topology X I) \<inter> \<Inter> \<T>"
lp15@69874
   387
        apply (clarsimp simp add: relative_to_def intersection_of_def)
lp15@69874
   388
        apply (rule that, auto dest!: subsetD)
lp15@69874
   389
        done
lp15@69874
   390
      then have "f \<in> PiE I (topspace \<circ> X)" "f \<in> \<Inter>\<T>" and subU: "PiE I (topspace \<circ> X) \<inter> \<Inter>\<T> \<subseteq> U"
lp15@69874
   391
        by (auto simp: PiE_iff)
lp15@69874
   392
      have *: "f i \<in> topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}
lp15@69874
   393
             \<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
lp15@69874
   394
        if "i \<in> I" for i
lp15@69874
   395
      proof -
lp15@69874
   396
        have "finite ((\<lambda>U. {x. x i \<in> U}) -` \<T>)"
lp15@69874
   397
        proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
lp15@69874
   398
          show "inj (\<lambda>U. {x. x i \<in> U})"
lp15@69874
   399
            by (auto simp: inj_on_def)
lp15@69874
   400
        qed
lp15@69874
   401
        then have fin: "finite {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}"
lp15@69874
   402
          by (rule rev_finite_subset) auto
lp15@69874
   403
        have "openin (X i) (\<Inter> (insert (topspace (X i)) {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}))"
lp15@69874
   404
          by (rule openin_Inter) (auto simp: fin)
lp15@69874
   405
        then show ?thesis
lp15@69874
   406
          using \<open>f \<in> \<Inter> \<T>\<close> by (fastforce simp: that top)
lp15@69874
   407
      qed
lp15@69874
   408
      define \<Phi> where "\<Phi> \<equiv> \<lambda>i. topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {f. f i \<in> U} \<in> \<T>}"
lp15@69874
   409
      have "\<forall>i \<in> I. \<exists>x. x \<in> S i \<inter> \<Phi> i"
lp15@69874
   410
        using R [OF _ *] unfolding \<Phi>_def by blast
lp15@69874
   411
      then obtain \<theta> where \<theta> [rule_format]: "\<forall>i \<in> I. \<theta> i \<in> S i \<inter> \<Phi> i"
lp15@69874
   412
        by metis
lp15@69874
   413
      show "\<exists>y\<in>Pi\<^sub>E I S. \<exists>x\<in>\<U>. y \<in> x"
lp15@69874
   414
      proof
lp15@69874
   415
        show "\<exists>U \<in> \<U>. (\<lambda>i \<in> I. \<theta> i) \<in> U"
lp15@69874
   416
        proof
lp15@69874
   417
          have "restrict \<theta> I \<in> PiE I (topspace \<circ> X) \<inter> \<Inter>\<T>"
lp15@69874
   418
            using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
lp15@69874
   419
          then show "restrict \<theta> I \<in> U"
lp15@69874
   420
            using subU by blast
lp15@69874
   421
        qed (rule \<open>U \<in> \<U>\<close>)
lp15@69874
   422
      next
lp15@69874
   423
        show "(\<lambda>i \<in> I. \<theta> i) \<in> Pi\<^sub>E I S"
lp15@69874
   424
          using \<theta> by simp
lp15@69874
   425
      qed
lp15@69874
   426
    qed
lp15@69874
   427
  qed
lp15@69874
   428
  show ?thesis
lp15@69874
   429
    apply (simp add: * closure_of_def PiE_iff set_eq_iff cong: conj_cong)
lp15@69874
   430
    by metis
lp15@69874
   431
qed
lp15@69030
   432
lp15@69874
   433
corollary closedin_product_topology:
lp15@69874
   434
   "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
lp15@69874
   435
  apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
lp15@69874
   436
  apply (metis closure_of_empty)
lp15@69030
   437
  done
lp15@69030
   438
lp15@69874
   439
corollary closedin_product_topology_singleton:
lp15@69874
   440
   "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
lp15@69874
   441
  using PiE_singleton closedin_product_topology [of X I]
lp15@69874
   442
  by (metis (no_types, lifting) all_not_in_conv insertI1)
lp15@69030
   443
lp15@69922
   444
lemma product_topology_empty:
lp15@69922
   445
   "product_topology X {} = topology (\<lambda>S. S \<in> {{},{\<lambda>k. undefined}})"
lp15@69922
   446
  unfolding product_topology union_of_def intersection_of_def arbitrary_def relative_to_def
lp15@69922
   447
  by (auto intro: arg_cong [where f=topology])
lp15@69922
   448
lp15@69922
   449
lemma openin_product_topology_empty: "openin (product_topology X {}) S \<longleftrightarrow> S \<in> {{},{\<lambda>k. undefined}}"
lp15@69922
   450
  unfolding union_of_def intersection_of_def arbitrary_def relative_to_def openin_product_topology
lp15@69922
   451
  by auto
lp15@69922
   452
lp15@69874
   453
lp15@69874
   454
subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
hoelzl@64289
   455
lp15@69939
   456
lemma continuous_map_product_coordinates [simp]:
hoelzl@64289
   457
  assumes "i \<in> I"
lp15@69939
   458
  shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
hoelzl@64289
   459
proof -
hoelzl@64289
   460
  {
hoelzl@64289
   461
    fix U assume "openin (T i) U"
hoelzl@64289
   462
    define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
hoelzl@64289
   463
    then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
wenzelm@64911
   464
      unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
hoelzl@64289
   465
      by (auto simp add: PiE_iff, auto, metis subsetCE)
hoelzl@64289
   466
    have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
wenzelm@64911
   467
      unfolding X_def using \<open>openin (T i) U\<close> by auto
hoelzl@64289
   468
    have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
hoelzl@64289
   469
      unfolding product_topology_def
hoelzl@64289
   470
      apply (rule topology_generated_by_Basis)
hoelzl@64289
   471
      apply (subst *)
hoelzl@64289
   472
      using ** by auto
hoelzl@64289
   473
  }
lp15@69939
   474
  then show ?thesis unfolding continuous_map_alt
lp15@69939
   475
    by (auto simp add: assms PiE_iff)
hoelzl@64289
   476
qed
hoelzl@64289
   477
lp15@69939
   478
lemma continuous_map_coordinatewise_then_product [intro]:
lp15@69939
   479
  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   480
          "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
lp15@69939
   481
  shows "continuous_map T1 (product_topology T I) f"
hoelzl@64289
   482
unfolding product_topology_def
immler@69681
   483
proof (rule continuous_on_generated_topo)
hoelzl@64289
   484
  fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
hoelzl@64289
   485
  then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
hoelzl@64289
   486
    by blast
hoelzl@64289
   487
  define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
hoelzl@64289
   488
  have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
hoelzl@64289
   489
  have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
lp15@69939
   490
    using that assms(1) by (simp add: continuous_map_preimage_topspace)
hoelzl@64289
   491
  then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
hoelzl@64289
   492
    using that unfolding J_def by auto
hoelzl@64289
   493
  have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
hoelzl@64289
   494
    by (subst H(1), auto simp add: PiE_iff assms)
hoelzl@64289
   495
  also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
wenzelm@64911
   496
    using * \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   497
  also have "openin T1 (...)"
hoelzl@64289
   498
    apply (rule openin_INT)
wenzelm@64911
   499
    apply (simp add: \<open>finite J\<close>)
wenzelm@64911
   500
    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   501
  ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
hoelzl@64289
   502
next
hoelzl@64289
   503
  show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
hoelzl@64289
   504
    apply (subst topology_generated_by_topspace[symmetric])
hoelzl@64289
   505
    apply (subst product_topology_def[symmetric])
lp15@69030
   506
    apply (simp only: topspace_product_topology)
hoelzl@64289
   507
    apply (auto simp add: PiE_iff)
lp15@69939
   508
    using assms unfolding continuous_map_def by auto
hoelzl@64289
   509
qed
hoelzl@64289
   510
lp15@69939
   511
lemma continuous_map_product_then_coordinatewise [intro]:
lp15@69939
   512
  assumes "continuous_map T1 (product_topology T I) f"
lp15@69939
   513
  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   514
        "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
hoelzl@64289
   515
proof -
hoelzl@64289
   516
  fix i assume "i \<in> I"
hoelzl@64289
   517
  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
lp15@69939
   518
  also have "continuous_map T1 (T i) (...)"
lp15@69939
   519
    apply (rule continuous_map_compose[of _ "product_topology T I"])
wenzelm@64911
   520
    using assms \<open>i \<in> I\<close> by auto
lp15@69939
   521
  ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
hoelzl@64289
   522
    by simp
hoelzl@64289
   523
next
hoelzl@64289
   524
  fix i x assume "i \<notin> I" "x \<in> topspace T1"
hoelzl@64289
   525
  have "f x \<in> topspace (product_topology T I)"
lp15@69939
   526
    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
hoelzl@64289
   527
  then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
lp15@69030
   528
    using topspace_product_topology by metis
hoelzl@64289
   529
  then show "f x i = undefined"
wenzelm@64911
   530
    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
hoelzl@64289
   531
qed
hoelzl@64289
   532
immler@69681
   533
lemma continuous_on_restrict:
hoelzl@64289
   534
  assumes "J \<subseteq> I"
lp15@69939
   535
  shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
lp15@69939
   536
proof (rule continuous_map_coordinatewise_then_product)
hoelzl@64289
   537
  fix i assume "i \<in> J"
hoelzl@64289
   538
  then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
lp15@69939
   539
  then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
wenzelm@64911
   540
    using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
hoelzl@64289
   541
next
hoelzl@64289
   542
  fix i assume "i \<notin> J"
hoelzl@64289
   543
  then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
hoelzl@64289
   544
    unfolding restrict_def by auto
hoelzl@64289
   545
qed
hoelzl@64289
   546
hoelzl@64289
   547
ak2110@69722
   548
subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
hoelzl@64289
   549
hoelzl@64289
   550
instantiation "fun" :: (type, topological_space) topological_space
hoelzl@64289
   551
begin
hoelzl@64289
   552
ak2110@68833
   553
definition%important open_fun_def:
hoelzl@64289
   554
  "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
   555
immler@69681
   556
instance proof
hoelzl@64289
   557
  have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
lp15@69030
   558
    unfolding topspace_product_topology topspace_euclidean by auto
hoelzl@64289
   559
  then show "open (UNIV::('a \<Rightarrow> 'b) set)"
hoelzl@64289
   560
    unfolding open_fun_def by (metis openin_topspace)
hoelzl@64289
   561
qed (auto simp add: open_fun_def)
hoelzl@64289
   562
hoelzl@64289
   563
end
hoelzl@64289
   564
immler@69681
   565
lemma euclidean_product_topology:
hoelzl@64289
   566
  "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
hoelzl@64289
   567
by (metis open_openin topology_eq open_fun_def)
hoelzl@64289
   568
immler@69681
   569
proposition product_topology_basis':
hoelzl@64289
   570
  fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
hoelzl@64289
   571
  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
hoelzl@64289
   572
  shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
immler@69681
   573
proof -
hoelzl@64289
   574
  define J where "J = x`I"
hoelzl@64289
   575
  define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
hoelzl@64289
   576
  define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
hoelzl@64289
   577
  have *: "open (X i)" for i
hoelzl@64289
   578
    unfolding X_def V_def using assms by auto
hoelzl@64289
   579
  have **: "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
   580
    unfolding X_def V_def J_def using assms(1) by auto
hoelzl@64289
   581
  have "open (Pi\<^sub>E UNIV X)"
lp15@69939
   582
    unfolding open_fun_def
lp15@69710
   583
    by (simp_all add: * ** product_topology_basis)
hoelzl@64289
   584
  moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
hoelzl@64289
   585
    apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
hoelzl@64289
   586
    proof (auto)
hoelzl@64289
   587
      fix f :: "'a \<Rightarrow> 'b" and i :: 'i
hoelzl@64289
   588
      assume a1: "i \<in> I"
hoelzl@64289
   589
      assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
hoelzl@64289
   590
      have f3: "x i \<in> x`I"
hoelzl@64289
   591
        using a1 by blast
hoelzl@64289
   592
      have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
hoelzl@64289
   593
        using a1 by blast
hoelzl@64289
   594
      then show "f (x i) \<in> U i"
hoelzl@64289
   595
        using f3 a2 by (meson Inter_iff)
hoelzl@64289
   596
    qed
hoelzl@64289
   597
  ultimately show ?thesis by simp
hoelzl@64289
   598
qed
hoelzl@64289
   599
wenzelm@64911
   600
text \<open>The results proved in the general situation of products of possibly different
wenzelm@64911
   601
spaces have their counterparts in this simpler setting.\<close>
hoelzl@64289
   602
immler@69681
   603
lemma continuous_on_product_coordinates [simp]:
hoelzl@64289
   604
  "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
lp15@69939
   605
  using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
lp15@69939
   606
    by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
hoelzl@64289
   607
immler@69681
   608
lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
lp15@69922
   609
  fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
lp15@69918
   610
  assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
lp15@69918
   611
  shows "continuous_on S f"
lp15@69939
   612
  using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
lp15@69939
   613
  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
hoelzl@64289
   614
lp15@69918
   615
lemma continuous_on_product_then_coordinatewise_UNIV:
hoelzl@64289
   616
  assumes "continuous_on UNIV f"
hoelzl@64289
   617
  shows "continuous_on UNIV (\<lambda>x. f x i)"
lp15@69939
   618
  using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
lp15@69939
   619
  by fastforce
hoelzl@64289
   620
lp15@69918
   621
lemma continuous_on_product_then_coordinatewise:
lp15@69918
   622
  assumes "continuous_on S f"
lp15@69918
   623
  shows "continuous_on S (\<lambda>x. f x i)"
lp15@69918
   624
proof -
lp15@69918
   625
  have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
lp15@69939
   626
    by (metis assms continuous_on_compose continuous_on_id
lp15@69918
   627
        continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
lp15@69918
   628
  then show ?thesis
lp15@69918
   629
    by auto
lp15@69918
   630
qed
lp15@69918
   631
lp15@69918
   632
lemma continuous_on_coordinatewise_iff:
lp15@69918
   633
  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
lp15@69918
   634
  shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
lp15@69918
   635
  by (auto simp: continuous_on_product_then_coordinatewise)
hoelzl@64289
   636
ak2110@69722
   637
subsubsection%important \<open>Topological countability for product spaces\<close>
hoelzl@64289
   638
wenzelm@64911
   639
text \<open>The next two lemmas are useful to prove first or second countability
hoelzl@64289
   640
of product spaces, but they have more to do with countability and could
wenzelm@64911
   641
be put in the corresponding theory.\<close>
hoelzl@64289
   642
immler@69681
   643
lemma countable_nat_product_event_const:
hoelzl@64289
   644
  fixes F::"'a set" and a::'a
hoelzl@64289
   645
  assumes "a \<in> F" "countable F"
hoelzl@64289
   646
  shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
hoelzl@64289
   647
proof -
hoelzl@64289
   648
  have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
hoelzl@64289
   649
                  \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
hoelzl@64289
   650
    using infinite_nat_iff_unbounded_le by fastforce
hoelzl@64289
   651
  have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
hoelzl@64289
   652
  proof (induction N)
hoelzl@64289
   653
    case 0
hoelzl@64289
   654
    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
wenzelm@64911
   655
      using \<open>a \<in> F\<close> by auto
hoelzl@64289
   656
    then show ?case by auto
hoelzl@64289
   657
  next
hoelzl@64289
   658
    case (Suc N)
hoelzl@64289
   659
    define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
hoelzl@64289
   660
      where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
hoelzl@64289
   661
    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
hoelzl@64289
   662
    proof (auto)
hoelzl@64289
   663
      fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
hoelzl@64289
   664
      define y where "y = (\<lambda>i. if i = N then a else x i)"
hoelzl@64289
   665
      have "f (y, x N) = x"
hoelzl@64289
   666
        unfolding f_def y_def by auto
hoelzl@64289
   667
      moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
wenzelm@64911
   668
        unfolding y_def using H \<open>a \<in> F\<close> by auto
hoelzl@64289
   669
      ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
hoelzl@64289
   670
        by (metis (no_types, lifting) image_eqI)
hoelzl@64289
   671
    qed
hoelzl@64289
   672
    moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
hoelzl@64289
   673
      using Suc.IH assms(2) by auto
hoelzl@64289
   674
    ultimately show ?case
hoelzl@64289
   675
      by (meson countable_image countable_subset)
hoelzl@64289
   676
  qed
hoelzl@64289
   677
  then show ?thesis using countable_subset[OF *] by auto
hoelzl@64289
   678
qed
hoelzl@64289
   679
immler@69681
   680
lemma countable_product_event_const:
hoelzl@64289
   681
  fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
hoelzl@64289
   682
  assumes "\<And>i. countable (F i)"
hoelzl@64289
   683
  shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
hoelzl@64289
   684
proof -
hoelzl@64289
   685
  define G where "G = (\<Union>i. F i) \<union> {b}"
hoelzl@64289
   686
  have "countable G" unfolding G_def using assms by auto
hoelzl@64289
   687
  have "b \<in> G" unfolding G_def by auto
hoelzl@64289
   688
  define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
hoelzl@64289
   689
  have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
hoelzl@64289
   690
        \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
hoelzl@64289
   691
  proof (auto)
hoelzl@64289
   692
    fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
hoelzl@64289
   693
    define I where "I = {i. f i \<noteq> b}"
hoelzl@64289
   694
    define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
hoelzl@64289
   695
    have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
hoelzl@64289
   696
    then have "finite {j. g j \<noteq> b}"
hoelzl@64289
   697
      unfolding I_def using H(2) using finite_surj by blast
hoelzl@64289
   698
    moreover have "g j \<in> G" for j
hoelzl@64289
   699
      unfolding g_def G_def using H by auto
hoelzl@64289
   700
    ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
hoelzl@64289
   701
      by auto
hoelzl@64289
   702
    moreover have "f = pi g"
hoelzl@64289
   703
      unfolding pi_def g_def I_def using H by fastforce
hoelzl@64289
   704
    ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
hoelzl@64289
   705
      by auto
hoelzl@64289
   706
  qed
hoelzl@64289
   707
  then show ?thesis
wenzelm@64911
   708
    using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
hoelzl@64289
   709
    by (meson countable_image countable_subset)
hoelzl@64289
   710
qed
hoelzl@64289
   711
hoelzl@64289
   712
instance "fun" :: (countable, first_countable_topology) first_countable_topology
immler@69681
   713
proof
hoelzl@64289
   714
  fix x::"'a \<Rightarrow> 'b"
hoelzl@64289
   715
  have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
hoelzl@64289
   716
    apply (rule choice) using first_countable_basis by auto
hoelzl@64289
   717
  then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
hoelzl@64289
   718
                                                  "\<And>x i. open (A x i)"
hoelzl@64289
   719
                                                  "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
hoelzl@64289
   720
    by metis
wenzelm@69566
   721
  text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
hoelzl@64289
   722
  define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
hoelzl@64289
   723
  have "countable (B i)" for i unfolding B_def by auto
hoelzl@64289
   724
hoelzl@64289
   725
  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
hoelzl@64289
   726
  have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
hoelzl@64289
   727
    unfolding K_def B_def by auto
hoelzl@64289
   728
  then have "K \<noteq> {}" by auto
hoelzl@64289
   729
  have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
wenzelm@64911
   730
    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
hoelzl@64289
   731
  moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
hoelzl@64289
   732
    unfolding K_def by auto
hoelzl@64289
   733
  ultimately have "countable K" by auto
hoelzl@64289
   734
  have "x \<in> k" if "k \<in> K" for k
hoelzl@64289
   735
    using that unfolding K_def B_def apply auto using A(1) by auto
hoelzl@64289
   736
  have "open k" if "k \<in> K" for k
hoelzl@64289
   737
    using that unfolding open_fun_def K_def B_def apply (auto)
hoelzl@64289
   738
    apply (rule product_topology_basis)
hoelzl@64289
   739
    unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
hoelzl@64289
   740
hoelzl@64289
   741
  have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
hoelzl@64289
   742
  proof -
hoelzl@64289
   743
    have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
wenzelm@64911
   744
      using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
hoelzl@64289
   745
    with product_topology_open_contains_basis[OF this]
hoelzl@64289
   746
    have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
lp15@69710
   747
      by simp
hoelzl@64289
   748
    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
hoelzl@64289
   749
                           "\<And>i. open (X i)"
hoelzl@64289
   750
                           "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
   751
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
hoelzl@64289
   752
      by auto
hoelzl@64289
   753
    define I where "I = {i. X i \<noteq> UNIV}"
hoelzl@64289
   754
    define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
hoelzl@64289
   755
    have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
hoelzl@64289
   756
      unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
hoelzl@64289
   757
    have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
hoelzl@64289
   758
      apply (cases "i \<in> I")
hoelzl@64289
   759
      unfolding Y_def using * that apply (auto)
hoelzl@64289
   760
      apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
hoelzl@64289
   761
      unfolding B_def apply simp
hoelzl@64289
   762
      unfolding I_def apply auto
hoelzl@64289
   763
      done
hoelzl@64289
   764
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
hoelzl@64289
   765
      unfolding Y_def by auto
hoelzl@64289
   766
    then have ***: "finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
   767
      unfolding I_def using H(3) rev_finite_subset by blast
hoelzl@64289
   768
    have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
   769
      using ** *** by auto
hoelzl@64289
   770
    then have "Pi\<^sub>E UNIV Y \<in> K"
hoelzl@64289
   771
      unfolding K_def by auto
hoelzl@64289
   772
hoelzl@64289
   773
    have "Y i \<subseteq> X i" for i
hoelzl@64289
   774
      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
hoelzl@64289
   775
    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
hoelzl@64289
   776
    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
wenzelm@64911
   777
    then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
hoelzl@64289
   778
  qed
hoelzl@64289
   779
hoelzl@64289
   780
  show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
hoelzl@64289
   781
    apply (rule first_countableI[of K])
wenzelm@64911
   782
    using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
hoelzl@64289
   783
qed
hoelzl@64289
   784
immler@69681
   785
proposition product_topology_countable_basis:
hoelzl@64289
   786
  shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
hoelzl@64289
   787
          topological_basis K \<and> countable K \<and>
wenzelm@64910
   788
          (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
immler@69681
   789
proof -
hoelzl@64289
   790
  obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
hoelzl@64289
   791
    using ex_countable_basis by auto
hoelzl@64289
   792
  then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
hoelzl@64289
   793
  define B2 where "B2 = B \<union> {UNIV}"
hoelzl@64289
   794
  have "countable B2"
hoelzl@64289
   795
    unfolding B2_def using B by auto
hoelzl@64289
   796
  have "open U" if "U \<in> B2" for U
hoelzl@64289
   797
    using that unfolding B2_def using B topological_basis_open by auto
hoelzl@64289
   798
hoelzl@64289
   799
  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
wenzelm@64910
   800
  have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
wenzelm@64911
   801
    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
hoelzl@64289
   802
hoelzl@64289
   803
  have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
wenzelm@64911
   804
    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
hoelzl@64289
   805
  moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
hoelzl@64289
   806
    unfolding K_def by auto
hoelzl@64289
   807
  ultimately have ii: "countable K" by auto
hoelzl@64289
   808
hoelzl@64289
   809
  have iii: "topological_basis K"
hoelzl@64289
   810
  proof (rule topological_basisI)
hoelzl@64289
   811
    fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
hoelzl@64289
   812
    then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
   813
      unfolding open_fun_def by auto
wenzelm@64911
   814
    with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
hoelzl@64289
   815
    have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
lp15@69710
   816
      by simp
hoelzl@64289
   817
    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
hoelzl@64289
   818
                           "\<And>i. open (X i)"
hoelzl@64289
   819
                           "finite {i. X i \<noteq> UNIV}"
hoelzl@64289
   820
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
hoelzl@64289
   821
      by auto
hoelzl@64289
   822
    then have "x i \<in> X i" for i by auto
hoelzl@64289
   823
    define I where "I = {i. X i \<noteq> UNIV}"
hoelzl@64289
   824
    define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
hoelzl@64289
   825
    have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
wenzelm@64911
   826
      unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
hoelzl@64289
   827
    have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
hoelzl@64289
   828
      using someI_ex[OF *]
hoelzl@64289
   829
      apply (cases "i \<in> I")
hoelzl@64289
   830
      unfolding Y_def using * apply (auto)
hoelzl@64289
   831
      unfolding B2_def I_def by auto
hoelzl@64289
   832
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
hoelzl@64289
   833
      unfolding Y_def by auto
hoelzl@64289
   834
    then have ***: "finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
   835
      unfolding I_def using H(3) rev_finite_subset by blast
hoelzl@64289
   836
    have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
hoelzl@64289
   837
      using ** *** by auto
hoelzl@64289
   838
    then have "Pi\<^sub>E UNIV Y \<in> K"
hoelzl@64289
   839
      unfolding K_def by auto
hoelzl@64289
   840
hoelzl@64289
   841
    have "Y i \<subseteq> X i" for i
hoelzl@64289
   842
      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
hoelzl@64289
   843
    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
hoelzl@64289
   844
    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
hoelzl@64289
   845
hoelzl@64289
   846
    have "x \<in> Pi\<^sub>E UNIV Y"
hoelzl@64289
   847
      using ** by auto
hoelzl@64289
   848
hoelzl@64289
   849
    show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
wenzelm@64911
   850
      using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
hoelzl@64289
   851
  next
hoelzl@64289
   852
    fix U assume "U \<in> K"
hoelzl@64289
   853
    show "open U"
wenzelm@64911
   854
      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
hoelzl@64289
   855
      apply (rule product_topology_basis)
lp15@69710
   856
      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV by auto
hoelzl@64289
   857
  qed
hoelzl@64289
   858
hoelzl@64289
   859
  show ?thesis using i ii iii by auto
hoelzl@64289
   860
qed
hoelzl@64289
   861
hoelzl@64289
   862
instance "fun" :: (countable, second_countable_topology) second_countable_topology
hoelzl@64289
   863
  apply standard
hoelzl@64289
   864
  using product_topology_countable_basis topological_basis_imp_subbasis by auto
hoelzl@64289
   865
hoelzl@64289
   866
immler@69683
   867
subsection \<open>Metrics on product spaces\<close>
hoelzl@64289
   868
hoelzl@64289
   869
wenzelm@64911
   870
text \<open>In general, the product topology is not metrizable, unless the index set is countable.
hoelzl@64289
   871
When the index set is countable, essentially any (convergent) combination of the metrics on the
wenzelm@69566
   872
factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
hoelzl@64289
   873
for instance.
hoelzl@64289
   874
hoelzl@64289
   875
What is not completely trivial is that the distance thus defined induces the same topology
hoelzl@64289
   876
as the product topology. This is what we have to prove to show that we have an instance
wenzelm@69566
   877
of \<^class>\<open>metric_space\<close>.
hoelzl@64289
   878
hoelzl@64289
   879
The proofs below would work verbatim for general countable products of metric spaces. However,
hoelzl@64289
   880
since distances are only implemented in terms of type classes, we only develop the theory
wenzelm@64911
   881
for countable products of the same space.\<close>
hoelzl@64289
   882
hoelzl@64289
   883
instantiation "fun" :: (countable, metric_space) metric_space
hoelzl@64289
   884
begin
hoelzl@64289
   885
ak2110@68833
   886
definition%important dist_fun_def:
hoelzl@64289
   887
  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
   888
ak2110@68833
   889
definition%important uniformity_fun_def:
haftmann@69260
   890
  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
hoelzl@64289
   891
wenzelm@64911
   892
text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
hoelzl@64289
   893
instance: once it is proved, they become trivial consequences of the general theory of metric
hoelzl@64289
   894
spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
wenzelm@64911
   895
to do this.\<close>
hoelzl@64289
   896
immler@69681
   897
lemma dist_fun_le_dist_first_terms:
hoelzl@64289
   898
  "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
immler@69681
   899
proof -
hoelzl@64289
   900
  have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
hoelzl@64289
   901
          = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
hoelzl@64289
   902
    by (rule suminf_cong, simp add: power_add)
hoelzl@64289
   903
  also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
hoelzl@64289
   904
    apply (rule suminf_mult)
hoelzl@64289
   905
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
   906
  also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
hoelzl@64289
   907
    apply (simp, rule suminf_le, simp)
hoelzl@64289
   908
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
   909
  also have "... = (1/2)^(Suc N) * 2"
hoelzl@64289
   910
    using suminf_geometric[of "1/2"] by auto
hoelzl@64289
   911
  also have "... = (1/2)^N"
hoelzl@64289
   912
    by auto
hoelzl@64289
   913
  finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"
hoelzl@64289
   914
    by simp
hoelzl@64289
   915
hoelzl@64289
   916
  define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
hoelzl@64289
   917
  have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
hoelzl@64289
   918
    unfolding M_def by (rule Max_ge, auto)
hoelzl@64289
   919
  then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
hoelzl@64289
   920
  have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
hoelzl@64289
   921
    unfolding M_def apply (rule Max_ge) using that by auto
hoelzl@64289
   922
  then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
hoelzl@64289
   923
    using that by force
hoelzl@64289
   924
  have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
hoelzl@64289
   925
      (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
hoelzl@64289
   926
    by (rule sum_mono, simp add: i)
hoelzl@64289
   927
  also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
hoelzl@64289
   928
    by (rule sum_distrib_left[symmetric])
hoelzl@64289
   929
  also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
hoelzl@64289
   930
    by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
hoelzl@64289
   931
  also have "... = M * 2"
hoelzl@64289
   932
    using suminf_geometric[of "1/2"] by auto
hoelzl@64289
   933
  finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
hoelzl@64289
   934
    by simp
hoelzl@64289
   935
hoelzl@64289
   936
  have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
   937
    unfolding dist_fun_def by simp
hoelzl@64289
   938
  also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
hoelzl@64289
   939
                  + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
   940
    apply (rule suminf_split_initial_segment)
hoelzl@64289
   941
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
   942
  also have "... \<le> 2 * M + (1/2)^N"
hoelzl@64289
   943
    using * ** by auto
hoelzl@64289
   944
  finally show ?thesis unfolding M_def by simp
hoelzl@64289
   945
qed
hoelzl@64289
   946
immler@69681
   947
lemma open_fun_contains_ball_aux:
hoelzl@64289
   948
  assumes "open (U::(('a \<Rightarrow> 'b) set))"
hoelzl@64289
   949
          "x \<in> U"
hoelzl@64289
   950
  shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
hoelzl@64289
   951
proof -
hoelzl@64289
   952
  have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
hoelzl@64289
   953
    using open_fun_def assms by auto
hoelzl@64289
   954
  obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
hoelzl@64289
   955
                    "\<And>i. openin euclidean (X i)"
hoelzl@64289
   956
                    "finite {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
   957
                    "x \<in> Pi\<^sub>E UNIV X"
wenzelm@64911
   958
    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
hoelzl@64289
   959
  define I where "I = {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
   960
  have "finite I" unfolding I_def using H(3) by auto
hoelzl@64289
   961
  {
hoelzl@64289
   962
    fix i
wenzelm@64911
   963
    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
hoelzl@64289
   964
    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
wenzelm@64911
   965
      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
hoelzl@64289
   966
    then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
hoelzl@64289
   967
    define f where "f = min e (1/2)"
wenzelm@64911
   968
    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
wenzelm@64911
   969
    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
hoelzl@64289
   970
    ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
hoelzl@64289
   971
  } note * = this
hoelzl@64289
   972
  have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
hoelzl@64289
   973
    by (rule choice, auto simp add: *)
hoelzl@64289
   974
  then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
hoelzl@64289
   975
    by blast
hoelzl@64289
   976
  define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
hoelzl@64289
   977
  have "m > 0" if "I\<noteq>{}"
lp15@65036
   978
    unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
hoelzl@64289
   979
  moreover have "{y. dist x y < m} \<subseteq> U"
hoelzl@64289
   980
  proof (auto)
hoelzl@64289
   981
    fix y assume "dist x y < m"
hoelzl@64289
   982
    have "y i \<in> X i" if "i \<in> I" for i
hoelzl@64289
   983
    proof -
hoelzl@64289
   984
      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
   985
        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
   986
      define n where "n = to_nat i"
hoelzl@64289
   987
      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
wenzelm@64911
   988
        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
hoelzl@64289
   989
      then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
wenzelm@64911
   990
        using \<open>n = to_nat i\<close> by auto
hoelzl@64289
   991
      also have "... \<le> (1/2)^(to_nat i) * e i"
wenzelm@64911
   992
        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
hoelzl@64289
   993
      ultimately have "min (dist (x i) (y i)) 1 < e i"
hoelzl@64289
   994
        by (auto simp add: divide_simps)
hoelzl@64289
   995
      then have "dist (x i) (y i) < e i"
wenzelm@64911
   996
        using \<open>e i < 1\<close> by auto
wenzelm@64911
   997
      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
hoelzl@64289
   998
    qed
hoelzl@64289
   999
    then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
wenzelm@64911
  1000
    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
hoelzl@64289
  1001
  qed
hoelzl@64289
  1002
  ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
hoelzl@64289
  1003
hoelzl@64289
  1004
  have "U = UNIV" if "I = {}"
hoelzl@64289
  1005
    using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
hoelzl@64289
  1006
  then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
hoelzl@64289
  1007
  then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
hoelzl@64289
  1008
qed
hoelzl@64289
  1009
immler@69681
  1010
lemma ball_fun_contains_open_aux:
hoelzl@64289
  1011
  fixes x::"('a \<Rightarrow> 'b)" and e::real
hoelzl@64289
  1012
  assumes "e>0"
hoelzl@64289
  1013
  shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
hoelzl@64289
  1014
proof -
hoelzl@64289
  1015
  have "\<exists>N::nat. 2^N > 8/e"
hoelzl@64289
  1016
    by (simp add: real_arch_pow)
hoelzl@64289
  1017
  then obtain N::nat where "2^N > 8/e" by auto
hoelzl@64289
  1018
  define f where "f = e/4"
hoelzl@64289
  1019
  have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
hoelzl@64289
  1020
  define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"
hoelzl@64289
  1021
  have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
hoelzl@64289
  1022
    unfolding X_def by auto
hoelzl@64289
  1023
  then have "finite {i. X i \<noteq> topspace euclidean}"
hoelzl@64289
  1024
    unfolding topspace_euclidean using finite_surj by blast
hoelzl@64289
  1025
  have "\<And>i. open (X i)"
hoelzl@64289
  1026
    unfolding X_def using metric_space_class.open_ball open_UNIV by auto
hoelzl@64289
  1027
  then have "\<And>i. openin euclidean (X i)"
hoelzl@64289
  1028
    using open_openin by auto
hoelzl@64289
  1029
  define U where "U = Pi\<^sub>E UNIV X"
hoelzl@64289
  1030
  have "open U"
hoelzl@64289
  1031
    unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
wenzelm@64911
  1032
    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
hoelzl@64289
  1033
    by auto
hoelzl@64289
  1034
  moreover have "x \<in> U"
hoelzl@64289
  1035
    unfolding U_def X_def by (auto simp add: PiE_iff)
hoelzl@64289
  1036
  moreover have "dist x y < e" if "y \<in> U" for y
hoelzl@64289
  1037
  proof -
hoelzl@64289
  1038
    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
wenzelm@64911
  1039
      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
hoelzl@64289
  1040
      unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
hoelzl@64289
  1041
    have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
hoelzl@64289
  1042
      apply (rule Max.boundedI) using * by auto
hoelzl@64289
  1043
hoelzl@64289
  1044
    have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
hoelzl@64289
  1045
      by (rule dist_fun_le_dist_first_terms)
hoelzl@64289
  1046
    also have "... \<le> 2 * f + e / 8"
wenzelm@64911
  1047
      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1048
    also have "... \<le> e/2 + e/8"
hoelzl@64289
  1049
      unfolding f_def by auto
hoelzl@64289
  1050
    also have "... < e"
hoelzl@64289
  1051
      by auto
hoelzl@64289
  1052
    finally show "dist x y < e" by simp
hoelzl@64289
  1053
  qed
hoelzl@64289
  1054
  ultimately show ?thesis by auto
hoelzl@64289
  1055
qed
hoelzl@64289
  1056
immler@69681
  1057
lemma fun_open_ball_aux:
hoelzl@64289
  1058
  fixes U::"('a \<Rightarrow> 'b) set"
hoelzl@64289
  1059
  shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
hoelzl@64289
  1060
proof (auto)
hoelzl@64289
  1061
  assume "open U"
hoelzl@64289
  1062
  fix x assume "x \<in> U"
hoelzl@64289
  1063
  then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
wenzelm@64911
  1064
    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
hoelzl@64289
  1065
next
hoelzl@64289
  1066
  assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
hoelzl@64289
  1067
  define K where "K = {V. open V \<and> V \<subseteq> U}"
hoelzl@64289
  1068
  {
hoelzl@64289
  1069
    fix x assume "x \<in> U"
hoelzl@64289
  1070
    then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
hoelzl@64289
  1071
    then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
wenzelm@64911
  1072
      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
hoelzl@64289
  1073
    have "V \<in> K"
hoelzl@64289
  1074
      unfolding K_def using e(2) V(1) V(3) by auto
wenzelm@64911
  1075
    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
hoelzl@64289
  1076
  }
hoelzl@64289
  1077
  then have "(\<Union>K) = U"
hoelzl@64289
  1078
    unfolding K_def by auto
hoelzl@64289
  1079
  moreover have "open (\<Union>K)"
hoelzl@64289
  1080
    unfolding K_def by auto
hoelzl@64289
  1081
  ultimately show "open U" by simp
hoelzl@64289
  1082
qed
hoelzl@64289
  1083
hoelzl@64289
  1084
instance proof
hoelzl@64289
  1085
  fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
hoelzl@64289
  1086
  proof
hoelzl@64289
  1087
    assume "x = y"
wenzelm@64911
  1088
    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
hoelzl@64289
  1089
  next
hoelzl@64289
  1090
    assume "dist x y = 0"
hoelzl@64289
  1091
    have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1092
      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1093
    have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
wenzelm@64911
  1094
      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
hoelzl@64289
  1095
    then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
hoelzl@64289
  1096
      by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
hoelzl@64289
  1097
                zero_eq_1_divide_iff zero_neq_numeral)
hoelzl@64289
  1098
    then have "x (from_nat n) = y (from_nat n)" for n
hoelzl@64289
  1099
      by auto
hoelzl@64289
  1100
    then have "x i = y i" for i
hoelzl@64289
  1101
      by (metis from_nat_to_nat)
hoelzl@64289
  1102
    then show "x = y"
hoelzl@64289
  1103
      by auto
hoelzl@64289
  1104
  qed
hoelzl@64289
  1105
next
wenzelm@64911
  1106
  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
hoelzl@64289
  1107
        with infinite series, hence we should justify the convergence at each step. In this
wenzelm@64911
  1108
        respect, the following simplification rule is extremely handy.\<close>
hoelzl@64289
  1109
  have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
hoelzl@64289
  1110
    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1111
  fix x y z::"'a \<Rightarrow> 'b"
hoelzl@64289
  1112
  {
hoelzl@64289
  1113
    fix n
hoelzl@64289
  1114
    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
hoelzl@64289
  1115
            dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  1116
      by (simp add: dist_triangle2)
hoelzl@64289
  1117
    have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  1118
      using zero_le_dist by blast
hoelzl@64289
  1119
    moreover
hoelzl@64289
  1120
    {
hoelzl@64289
  1121
      assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
hoelzl@64289
  1122
      then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
hoelzl@64289
  1123
        by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
hoelzl@64289
  1124
    }
hoelzl@64289
  1125
    ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
hoelzl@64289
  1126
            min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
hoelzl@64289
  1127
      using * by linarith
hoelzl@64289
  1128
  } note ineq = this
hoelzl@64289
  1129
  have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
hoelzl@64289
  1130
    unfolding dist_fun_def by simp
hoelzl@64289
  1131
  also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
hoelzl@64289
  1132
                        + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
hoelzl@64289
  1133
    apply (rule suminf_le)
hoelzl@64289
  1134
    using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
hoelzl@64289
  1135
      le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
hoelzl@64289
  1136
    by (auto simp add: summable_add)
hoelzl@64289
  1137
  also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
hoelzl@64289
  1138
                  + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
hoelzl@64289
  1139
    by (rule suminf_add[symmetric], auto)
hoelzl@64289
  1140
  also have "... = dist x z + dist y z"
hoelzl@64289
  1141
    unfolding dist_fun_def by simp
hoelzl@64289
  1142
  finally show "dist x y \<le> dist x z + dist y z"
hoelzl@64289
  1143
    by simp
hoelzl@64289
  1144
next
wenzelm@64911
  1145
  text\<open>Finally, we show that the topology generated by the distance and the product
wenzelm@69566
  1146
        topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
hoelzl@64289
  1147
        except that the condition to prove is expressed with filters. To deal with this,
wenzelm@69566
  1148
        we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
wenzelm@69566
  1149
        \<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<close>
hoelzl@64289
  1150
  fix U::"('a \<Rightarrow> 'b) set"
hoelzl@64289
  1151
  have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
hoelzl@64289
  1152
  unfolding uniformity_fun_def apply (subst eventually_INF_base)
hoelzl@64289
  1153
    by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
hoelzl@64289
  1154
  then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
hoelzl@64289
  1155
    unfolding fun_open_ball_aux by simp
hoelzl@64289
  1156
qed (simp add: uniformity_fun_def)
hoelzl@64289
  1157
hoelzl@64289
  1158
end
hoelzl@64289
  1159
wenzelm@64911
  1160
text \<open>Nice properties of spaces are preserved under countable products. In addition
hoelzl@64289
  1161
to first countability, second countability and metrizability, as we have seen above,
wenzelm@64911
  1162
completeness is also preserved, and therefore being Polish.\<close>
hoelzl@64289
  1163
hoelzl@64289
  1164
instance "fun" :: (countable, complete_space) complete_space
hoelzl@64289
  1165
proof
hoelzl@64289
  1166
  fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
hoelzl@64289
  1167
  have "Cauchy (\<lambda>n. u n i)" for i
hoelzl@64289
  1168
  unfolding cauchy_def proof (intro impI allI)
hoelzl@64289
  1169
    fix e assume "e>(0::real)"
hoelzl@64289
  1170
    obtain k where "i = from_nat k"
hoelzl@64289
  1171
      using from_nat_to_nat[of i] by metis
wenzelm@64911
  1172
    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
hoelzl@64289
  1173
    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
wenzelm@64911
  1174
      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
hoelzl@64289
  1175
    then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
hoelzl@64289
  1176
      by blast
hoelzl@64289
  1177
    have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
hoelzl@64289
  1178
    proof (auto)
hoelzl@64289
  1179
      fix m n::nat assume "m \<ge> N" "n \<ge> N"
hoelzl@64289
  1180
      have "(1/2)^k * min (dist (u m i) (u n i)) 1
hoelzl@64289
  1181
              = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
wenzelm@64911
  1182
        using \<open>i = from_nat k\<close> by auto
hoelzl@64289
  1183
      also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
hoelzl@64289
  1184
        apply (rule sum_le_suminf)
hoelzl@64289
  1185
        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
hoelzl@64289
  1186
      also have "... = dist (u m) (u n)"
hoelzl@64289
  1187
        unfolding dist_fun_def by auto
hoelzl@64289
  1188
      also have "... < (1/2)^k * min e 1"
wenzelm@64911
  1189
        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
hoelzl@64289
  1190
      finally have "min (dist (u m i) (u n i)) 1 < min e 1"
hoelzl@64289
  1191
        by (auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1192
      then show "dist (u m i) (u n i) < e" by auto
hoelzl@64289
  1193
    qed
hoelzl@64289
  1194
    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
hoelzl@64289
  1195
      by blast
hoelzl@64289
  1196
  qed
hoelzl@64289
  1197
  then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
hoelzl@64289
  1198
    using Cauchy_convergent convergent_def by auto
hoelzl@64289
  1199
  then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
hoelzl@64289
  1200
    using choice by force
hoelzl@64289
  1201
  then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
hoelzl@64289
  1202
  have "u \<longlonglongrightarrow> x"
hoelzl@64289
  1203
  proof (rule metric_LIMSEQ_I)
hoelzl@64289
  1204
    fix e assume [simp]: "e>(0::real)"
hoelzl@64289
  1205
    have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
hoelzl@64289
  1206
      by (rule metric_LIMSEQ_D, auto simp add: *)
hoelzl@64289
  1207
    have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
hoelzl@64289
  1208
      apply (rule choice) using i by auto
hoelzl@64289
  1209
    then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
hoelzl@64289
  1210
      by blast
hoelzl@64289
  1211
hoelzl@64289
  1212
    have "\<exists>N::nat. 2^N > 4/e"
hoelzl@64289
  1213
      by (simp add: real_arch_pow)
hoelzl@64289
  1214
    then obtain N::nat where "2^N > 4/e" by auto
hoelzl@64289
  1215
    define L where "L = Max {K (from_nat n)|n. n \<le> N}"
hoelzl@64289
  1216
    have "dist (u k) x < e" if "k \<ge> L" for k
hoelzl@64289
  1217
    proof -
hoelzl@64289
  1218
      have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
hoelzl@64289
  1219
      proof -
hoelzl@64289
  1220
        have "K (from_nat n) \<le> L"
wenzelm@64911
  1221
          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
wenzelm@64911
  1222
        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
hoelzl@64289
  1223
        then show ?thesis using K less_imp_le by auto
hoelzl@64289
  1224
      qed
hoelzl@64289
  1225
      have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
hoelzl@64289
  1226
        apply (rule Max.boundedI) using * by auto
hoelzl@64289
  1227
      have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
hoelzl@64289
  1228
        using dist_fun_le_dist_first_terms by auto
hoelzl@64289
  1229
      also have "... \<le> 2 * e/4 + e/4"
hoelzl@64289
  1230
        apply (rule add_mono)
wenzelm@64911
  1231
        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
hoelzl@64289
  1232
      also have "... < e" by auto
hoelzl@64289
  1233
      finally show ?thesis by simp
hoelzl@64289
  1234
    qed
hoelzl@64289
  1235
    then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
hoelzl@64289
  1236
  qed
hoelzl@64289
  1237
  then show "convergent u" using convergent_def by blast
hoelzl@64289
  1238
qed
hoelzl@64289
  1239
hoelzl@64289
  1240
instance "fun" :: (countable, polish_space) polish_space
hoelzl@64289
  1241
by standard
hoelzl@64289
  1242
lp15@69922
  1243
lp15@69922
  1244
subsection\<open>The Alexander subbase theorem\<close>
lp15@69922
  1245
lp15@69922
  1246
theorem Alexander_subbase:
lp15@69922
  1247
  assumes X: "topology (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) = X"
lp15@69922
  1248
    and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; \<Union>C = topspace X\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> \<Union>C' = topspace X"
lp15@69922
  1249
  shows "compact_space X"
lp15@69922
  1250
proof -
lp15@69922
  1251
  have U\<B>: "\<Union>\<B> = topspace X"
lp15@69922
  1252
    by (simp flip: X)
lp15@69922
  1253
  have False if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub: "topspace X \<subseteq> \<Union>\<U>"
lp15@69922
  1254
    and neg: "\<And>\<F>. \<lbrakk>\<F> \<subseteq> \<U>; finite \<F>\<rbrakk> \<Longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>" for \<U>
lp15@69922
  1255
  proof -
lp15@69922
  1256
    define \<A> where "\<A> \<equiv> {\<C>. (\<forall>U \<in> \<C>. openin X U) \<and> topspace X \<subseteq> \<Union>\<C> \<and> (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> ~(topspace X \<subseteq> \<Union>\<F>))}"
lp15@69922
  1257
    have 1: "\<A> \<noteq> {}"
lp15@69922
  1258
      unfolding \<A>_def using sub \<U> neg by force
lp15@69922
  1259
    have 2: "\<Union>\<C> \<in> \<A>" if "\<C>\<noteq>{}" and \<C>: "subset.chain \<A> \<C>" for \<C>
lp15@69922
  1260
      unfolding \<A>_def
lp15@69922
  1261
    proof (intro CollectI conjI ballI allI impI notI)
lp15@69922
  1262
      show "openin X U" if U: "U \<in> \<Union>\<C>" for U
lp15@69922
  1263
        using U \<C> unfolding \<A>_def subset_chain_def by force
lp15@69922
  1264
      have "\<C> \<subseteq> \<A>"
lp15@69922
  1265
        using subset_chain_def \<C> by blast
lp15@69922
  1266
      with that \<A>_def show UUC: "topspace X \<subseteq> \<Union>(\<Union>\<C>)"
lp15@69922
  1267
        by blast
lp15@69922
  1268
      show "False" if "finite \<F>" and "\<F> \<subseteq> \<Union>\<C>" and "topspace X \<subseteq> \<Union>\<F>" for \<F>
lp15@69922
  1269
      proof -
lp15@69922
  1270
        obtain \<B> where "\<B> \<in> \<C>" "\<F> \<subseteq> \<B>"
lp15@69922
  1271
          by (metis Sup_empty \<C> \<open>\<F> \<subseteq> \<Union>\<C>\<close> \<open>finite \<F>\<close> UUC empty_subsetI finite.emptyI finite_subset_Union_chain neg)
lp15@69922
  1272
        then show False
lp15@69922
  1273
          using \<A>_def \<open>\<C> \<subseteq> \<A>\<close> \<open>finite \<F>\<close> \<open>topspace X \<subseteq> \<Union>\<F>\<close> by blast
lp15@69922
  1274
      qed
lp15@69922
  1275
    qed
lp15@69922
  1276
    obtain \<K> where "\<K> \<in> \<A>" and "\<And>X. \<lbrakk>X\<in>\<A>; \<K> \<subseteq> X\<rbrakk> \<Longrightarrow> X = \<K>"
lp15@69922
  1277
      using subset_Zorn_nonempty [OF 1 2] by metis
lp15@69922
  1278
    then have *: "\<And>\<W>. \<lbrakk>\<And>W. W\<in>\<W> \<Longrightarrow> openin X W; topspace X \<subseteq> \<Union>\<W>; \<K> \<subseteq> \<W>;
lp15@69922
  1279
                        \<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<W>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False\<rbrakk>
lp15@69922
  1280
           \<Longrightarrow> \<W> = \<K>"
lp15@69922
  1281
      and ope: "\<forall>U\<in>\<K>. openin X U" and top: "topspace X \<subseteq> \<Union>\<K>"
lp15@69922
  1282
      and non: "\<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<K>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False"
lp15@69922
  1283
      unfolding \<A>_def by simp_all metis+
lp15@69922
  1284
    then obtain x where "x \<in> topspace X" "x \<notin> \<Union>(\<B> \<inter> \<K>)"
lp15@69922
  1285
    proof -
lp15@69922
  1286
      have "\<Union>(\<B> \<inter> \<K>) \<noteq> \<Union>\<B>"
lp15@69922
  1287
        by (metis \<open>\<Union>\<B> = topspace X\<close> fin inf.bounded_iff non order_refl)
lp15@69922
  1288
      then have "\<exists>a. a \<notin> \<Union>(\<B> \<inter> \<K>) \<and> a \<in> \<Union>\<B>"
lp15@69922
  1289
        by blast
lp15@69922
  1290
      then show ?thesis
lp15@69922
  1291
        using that by (metis U\<B>)
lp15@69922
  1292
    qed
lp15@69922
  1293
    obtain C where C: "openin X C" "C \<in> \<K>" "x \<in> C"
lp15@69922
  1294
      using \<open>x \<in> topspace X\<close> ope top by auto
lp15@69922
  1295
    then have "C \<subseteq> topspace X"
lp15@69922
  1296
      by (metis openin_subset)
lp15@69922
  1297
    then have "(arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) C"
lp15@69922
  1298
      using openin_subbase C unfolding X [symmetric] by blast
lp15@69922
  1299
    moreover have "C \<noteq> topspace X"
lp15@69922
  1300
      using \<open>\<K> \<in> \<A>\<close> \<open>C \<in> \<K>\<close> unfolding \<A>_def by blast
lp15@69922
  1301
    ultimately obtain \<V> W where W: "(finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to topspace X) W"
lp15@69922
  1302
      and "x \<in> W" "W \<in> \<V>" "\<Union>\<V> \<noteq> topspace X" "C = \<Union>\<V>"
lp15@69922
  1303
      using C  by (auto simp: union_of_def U\<B>)
lp15@69922
  1304
    then have "\<Union>\<V> \<subseteq> topspace X"
lp15@69922
  1305
      by (metis \<open>C \<subseteq> topspace X\<close>)
lp15@69922
  1306
    then have "topspace X \<notin> \<V>"
lp15@69922
  1307
      using \<open>\<Union>\<V> \<noteq> topspace X\<close> by blast
lp15@69922
  1308
    then obtain \<B>' where \<B>': "finite \<B>'" "\<B>' \<subseteq> \<B>" "x \<in> \<Inter>\<B>'" "W = topspace X \<inter> \<Inter>\<B>'"
lp15@69922
  1309
      using W \<open>x \<in> W\<close> unfolding relative_to_def intersection_of_def by auto
lp15@69922
  1310
    then have "\<Inter>\<B>' \<subseteq> \<Union>\<B>"
lp15@69922
  1311
      using \<open>W \<in> \<V>\<close> \<open>\<Union>\<V> \<noteq> topspace X\<close> \<open>\<Union>\<V> \<subseteq> topspace X\<close> by blast
lp15@69922
  1312
    then have "\<Inter>\<B>' \<subseteq> C"
lp15@69922
  1313
      using U\<B> \<open>C = \<Union>\<V>\<close> \<open>W = topspace X \<inter> \<Inter>\<B>'\<close> \<open>W \<in> \<V>\<close> by auto
lp15@69922
  1314
    have "\<forall>b \<in> \<B>'. \<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
lp15@69922
  1315
    proof
lp15@69922
  1316
      fix b
lp15@69922
  1317
      assume "b \<in> \<B>'"
lp15@69922
  1318
      have "insert b \<K> = \<K>" if neg: "\<not> (\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C'))"
lp15@69922
  1319
      proof (rule *)
lp15@69922
  1320
        show "openin X W" if "W \<in> insert b \<K>" for W
lp15@69922
  1321
          using that
lp15@69922
  1322
        proof
lp15@69922
  1323
          have "b \<in> \<B>"
lp15@69922
  1324
            using \<open>b \<in> \<B>'\<close> \<open>\<B>' \<subseteq> \<B>\<close> by blast
lp15@69922
  1325
          then have "\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> \<B> \<and> \<Inter>\<U> = b"
lp15@69922
  1326
            by (rule_tac x="{b}" in exI) auto
lp15@69922
  1327
          moreover have "\<Union>\<B> \<inter> b = b"
lp15@69922
  1328
            using \<B>'(2) \<open>b \<in> \<B>'\<close> by auto
lp15@69922
  1329
          ultimately show "openin X W" if "W = b"
lp15@69922
  1330
            using  that \<open>b \<in> \<B>'\<close>
lp15@69922
  1331
            apply (simp add: openin_subbase flip: X)
lp15@69922
  1332
            apply (auto simp: arbitrary_def intersection_of_def relative_to_def intro!: union_of_inc)
lp15@69922
  1333
            done
lp15@69922
  1334
          show "openin X W" if "W \<in> \<K>"
lp15@69922
  1335
            by (simp add: \<open>W \<in> \<K>\<close> ope)
lp15@69922
  1336
        qed
lp15@69922
  1337
      next
lp15@69922
  1338
        show "topspace X \<subseteq> \<Union> (insert b \<K>)"
lp15@69922
  1339
          using top by auto
lp15@69922
  1340
      next
lp15@69922
  1341
        show False if "finite \<F>" and "\<F> \<subseteq> insert b \<K>" "topspace X \<subseteq> \<Union>\<F>" for \<F>
lp15@69922
  1342
        proof -
lp15@69922
  1343
          have "insert b (\<F> \<inter> \<K>) = \<F>"
lp15@69922
  1344
            using non that by blast
lp15@69922
  1345
          then show False
lp15@69922
  1346
            by (metis Int_lower2 finite_insert neg that(1) that(3))
lp15@69922
  1347
        qed
lp15@69922
  1348
      qed auto
lp15@69922
  1349
      then show "\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
lp15@69922
  1350
        using \<open>b \<in> \<B>'\<close> \<open>x \<notin> \<Union>(\<B> \<inter> \<K>)\<close> \<B>'
lp15@69922
  1351
        by (metis IntI InterE Union_iff subsetD insertI1)
lp15@69922
  1352
    qed
lp15@69922
  1353
    then obtain F where F: "\<forall>b \<in> \<B>'. finite (F b) \<and> F b \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b (F b))"
lp15@69922
  1354
      by metis
lp15@69922
  1355
    let ?\<D> = "insert C (\<Union>(F ` \<B>'))"
lp15@69922
  1356
    show False
lp15@69922
  1357
    proof (rule non)
lp15@69922
  1358
      have "topspace X \<subseteq> (\<Inter>b \<in> \<B>'. \<Union>(insert b (F b)))"
lp15@69922
  1359
        using F by (simp add: INT_greatest)
lp15@69922
  1360
      also have "\<dots> \<subseteq> \<Union>?\<D>"
lp15@69922
  1361
        using \<open>\<Inter>\<B>' \<subseteq> C\<close> by force
lp15@69922
  1362
      finally show "topspace X \<subseteq> \<Union>?\<D>" .
lp15@69922
  1363
      show "?\<D> \<subseteq> \<K>"
lp15@69922
  1364
        using \<open>C \<in> \<K>\<close> F by auto
lp15@69922
  1365
      show "finite ?\<D>"
lp15@69922
  1366
        using \<open>finite \<B>'\<close> F by auto
lp15@69922
  1367
    qed
lp15@69922
  1368
  qed
lp15@69922
  1369
  then show ?thesis
lp15@69922
  1370
    by (force simp: compact_space_def compactin_def)
lp15@69922
  1371
qed
lp15@69922
  1372
lp15@69922
  1373
lp15@69922
  1374
corollary Alexander_subbase_alt:
lp15@69922
  1375
  assumes "U \<subseteq> \<Union>\<B>"
lp15@69922
  1376
  and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; U \<subseteq> \<Union>C\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> U \<subseteq> \<Union>C'"
lp15@69922
  1377
   and X: "topology
lp15@69922
  1378
              (arbitrary union_of
lp15@69922
  1379
                   (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to U)) = X"
lp15@69922
  1380
 shows "compact_space X"
lp15@69922
  1381
proof -
lp15@69922
  1382
  have "topspace X = U"
lp15@69922
  1383
    using X topspace_subbase by fastforce
lp15@69922
  1384
  have eq: "\<Union> (Collect ((\<lambda>x. x \<in> \<B>) relative_to U)) = U"
lp15@69922
  1385
    unfolding relative_to_def
lp15@69922
  1386
    using \<open>U \<subseteq> \<Union>\<B>\<close> by blast
lp15@69922
  1387
  have *: "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<and> \<Union>\<F> = topspace X"
lp15@69922
  1388
    if  "\<C> \<subseteq> Collect ((\<lambda>x. x \<in> \<B>) relative_to topspace X)" and UC: "\<Union>\<C> = topspace X" for \<C>
lp15@69922
  1389
  proof -
lp15@69922
  1390
    have "\<C> \<subseteq> (\<lambda>U. topspace X \<inter> U) ` \<B>"
lp15@69922
  1391
      using that by (auto simp: relative_to_def)
lp15@69922
  1392
    then obtain \<B>' where "\<B>' \<subseteq> \<B>" and \<B>': "\<C> = (\<inter>) (topspace X) ` \<B>'"
lp15@69922
  1393
      by (auto simp: subset_image_iff)
lp15@69922
  1394
    moreover have "U \<subseteq> \<Union>\<B>'"
lp15@69922
  1395
      using \<B>' \<open>topspace X = U\<close> UC by auto
lp15@69922
  1396
    ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
lp15@69922
  1397
      using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
lp15@69922
  1398
    then show ?thesis
lp15@69922
  1399
      unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
lp15@69922
  1400
  qed
lp15@69922
  1401
  show ?thesis
lp15@69922
  1402
    apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])
lp15@69922
  1403
     apply (simp flip: X)
lp15@69922
  1404
     apply (metis finite_intersection_of_relative_to eq)
lp15@69922
  1405
    apply (blast intro: *)
lp15@69922
  1406
    done
lp15@69922
  1407
qed
lp15@69922
  1408
lp15@69922
  1409
proposition continuous_map_componentwise:
lp15@69922
  1410
   "continuous_map X (product_topology Y I) f \<longleftrightarrow>
lp15@69922
  1411
    f ` (topspace X) \<subseteq> extensional I \<and> (\<forall>k \<in> I. continuous_map X (Y k) (\<lambda>x. f x k))"
lp15@69922
  1412
    (is "?lhs \<longleftrightarrow> _ \<and> ?rhs")
lp15@69922
  1413
proof (cases "\<forall>x \<in> topspace X. f x \<in> extensional I")
lp15@69922
  1414
  case True
lp15@69922
  1415
  then have "f ` (topspace X) \<subseteq> extensional I"
lp15@69922
  1416
    by force
lp15@69922
  1417
  moreover have ?rhs if L: ?lhs
lp15@69922
  1418
  proof -
lp15@69922
  1419
    have "openin X {x \<in> topspace X. f x k \<in> U}" if "k \<in> I" and "openin (Y k) U" for k U
lp15@69922
  1420
    proof -
lp15@69922
  1421
      have "openin (product_topology Y I) ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
lp15@69922
  1422
        apply (simp add: openin_product_topology flip: arbitrary_union_of_relative_to)
lp15@69922
  1423
        apply (simp add: relative_to_def)
lp15@69922
  1424
        using that apply (blast intro: arbitrary_union_of_inc finite_intersection_of_inc)
lp15@69922
  1425
        done
lp15@69922
  1426
      with that have "openin X {x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))}"
lp15@69922
  1427
        using L unfolding continuous_map_def by blast
lp15@69922
  1428
      moreover have "{x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))} = {x \<in> topspace X. f x k \<in> U}"
lp15@69922
  1429
        using L by (auto simp: continuous_map_def)
lp15@69922
  1430
      ultimately show ?thesis
lp15@69922
  1431
        by metis
lp15@69922
  1432
    qed
lp15@69922
  1433
    with that
lp15@69922
  1434
    show ?thesis
lp15@69922
  1435
      by (auto simp: continuous_map_def)
lp15@69922
  1436
  qed
lp15@69922
  1437
  moreover have ?lhs if ?rhs
lp15@69922
  1438
  proof -
lp15@69922
  1439
    have 1: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
lp15@69922
  1440
      using that True by (auto simp: continuous_map_def PiE_iff)
lp15@69922
  1441
    have 2: "{x \<in> S. \<exists>T\<in>\<T>. f x \<in> T} = (\<Union>T\<in>\<T>. {x \<in> S. f x \<in> T})" for S \<T>
lp15@69922
  1442
      by blast
lp15@69922
  1443
    have 3: "{x \<in> S. \<forall>U\<in>\<U>. f x \<in> U} = (\<Inter> (insert S ((\<lambda>U. {x \<in> S. f x \<in> U}) ` \<U>)))" for S \<U>
lp15@69922
  1444
      by blast
lp15@69922
  1445
    show ?thesis
lp15@69922
  1446
      unfolding continuous_map_def openin_product_topology arbitrary_def
lp15@69922
  1447
    proof (clarsimp simp: all_union_of 1 2)
lp15@69922
  1448
      fix \<T>
lp15@69922
  1449
      assume \<T>: "\<T> \<subseteq> Collect (finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U)
lp15@69922
  1450
                  relative_to (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
lp15@69922
  1451
      show "openin X (\<Union>T\<in>\<T>. {x \<in> topspace X. f x \<in> T})"
lp15@69922
  1452
      proof (rule openin_Union; clarify)
lp15@69922
  1453
        fix S T
lp15@69922
  1454
        assume "T \<in> \<T>"
lp15@69922
  1455
        obtain \<U> where "T = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<U>" and "finite \<U>"
lp15@69922
  1456
          "\<U> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
lp15@69922
  1457
          using subsetD [OF \<T> \<open>T \<in> \<T>\<close>] by (auto simp: intersection_of_def relative_to_def)
lp15@69922
  1458
        with that show "openin X {x \<in> topspace X. f x \<in> T}"
lp15@69922
  1459
          apply (simp add: continuous_map_def 1 cong: conj_cong)
lp15@69922
  1460
          unfolding 3
lp15@69922
  1461
          apply (rule openin_Inter; auto)
lp15@69922
  1462
          done
lp15@69922
  1463
      qed
lp15@69922
  1464
    qed
lp15@69922
  1465
  qed
lp15@69922
  1466
  ultimately show ?thesis
lp15@69922
  1467
    by metis
lp15@69922
  1468
next
lp15@69922
  1469
  case False
lp15@69922
  1470
  then show ?thesis
lp15@69922
  1471
    by (auto simp: continuous_map_def PiE_def)
lp15@69922
  1472
qed
lp15@69922
  1473
lp15@69922
  1474
lp15@69922
  1475
lemma continuous_map_componentwise_UNIV:
lp15@69922
  1476
   "continuous_map X (product_topology Y UNIV) f \<longleftrightarrow> (\<forall>k. continuous_map X (Y k) (\<lambda>x. f x k))"
lp15@69922
  1477
  by (simp add: continuous_map_componentwise)
lp15@69922
  1478
lp15@69922
  1479
lemma continuous_map_product_projection [continuous_intros]:
lp15@69922
  1480
   "k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
lp15@69922
  1481
  using continuous_map_componentwise [of "product_topology X I" X I id] by simp
lp15@69922
  1482
lp15@69945
  1483
declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]
lp15@69945
  1484
lp15@69922
  1485
proposition open_map_product_projection:
lp15@69922
  1486
  assumes "i \<in> I"
lp15@69922
  1487
  shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
lp15@69922
  1488
  unfolding openin_product_topology all_union_of arbitrary_def open_map_def image_Union
lp15@69922
  1489
proof clarify
lp15@69922
  1490
  fix \<V>
lp15@69922
  1491
  assume \<V>: "\<V> \<subseteq> Collect
lp15@69922
  1492
               (finite intersection_of
lp15@69922
  1493
                (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U) relative_to
lp15@69922
  1494
                           topspace (product_topology Y I))"
lp15@69922
  1495
  show "openin (Y i) (\<Union>x\<in>\<V>. (\<lambda>f. f i) ` x)"
lp15@69922
  1496
  proof (rule openin_Union, clarify)
lp15@69922
  1497
    fix S V
lp15@69922
  1498
    assume "V \<in> \<V>"
lp15@69922
  1499
    obtain \<F> where "finite \<F>"
lp15@69922
  1500
      and V: "V = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>"
lp15@69922
  1501
      and \<F>: "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
lp15@69922
  1502
      using subsetD [OF \<V> \<open>V \<in> \<V>\<close>]
lp15@69922
  1503
      by (auto simp: intersection_of_def relative_to_def)
lp15@69922
  1504
    show "openin (Y i) ((\<lambda>f. f i) ` V)"
lp15@69922
  1505
    proof (subst openin_subopen; clarify)
lp15@69922
  1506
      fix x f
lp15@69922
  1507
      assume "f \<in> V"
lp15@69922
  1508
      let ?T = "{a \<in> topspace(Y i).
lp15@69922
  1509
                   (\<lambda>j. if j = i then a
lp15@69922
  1510
                        else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
lp15@69922
  1511
      show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
lp15@69922
  1512
      proof (intro exI conjI)
lp15@69922
  1513
        show "openin (Y i) ?T"
lp15@69922
  1514
        proof (rule openin_continuous_map_preimage)
lp15@69922
  1515
          have "continuous_map (Y i) (Y k) (\<lambda>x. if k = i then x else f k)" if "k \<in> I" for k
lp15@69922
  1516
          proof (cases "k=i")
lp15@69922
  1517
            case True
lp15@69922
  1518
            then show ?thesis
lp15@69922
  1519
              by (metis (mono_tags) continuous_map_id eq_id_iff)
lp15@69922
  1520
          next
lp15@69922
  1521
            case False
lp15@69922
  1522
            then show ?thesis
lp15@69922
  1523
              by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
lp15@69922
  1524
          qed
lp15@69922
  1525
          then show "continuous_map (Y i) (product_topology Y I)
lp15@69922
  1526
                  (\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
lp15@69922
  1527
            by (auto simp: continuous_map_componentwise assms extensional_def)
lp15@69922
  1528
        next
lp15@69922
  1529
          have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
lp15@69922
  1530
            by (metis openin_topspace topspace_product_topology)
lp15@69922
  1531
          moreover have "openin (product_topology Y I) (\<Inter>B\<in>\<F>. (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> B)"
lp15@69922
  1532
                         if "\<F> \<noteq> {}"
lp15@69922
  1533
          proof -
lp15@69922
  1534
            show ?thesis
lp15@69922
  1535
            proof (rule openin_Inter)
lp15@69922
  1536
              show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
lp15@69922
  1537
                unfolding openin_product_topology relative_to_def
lp15@69922
  1538
                apply (clarify intro!: arbitrary_union_of_inc)
lp15@69922
  1539
                apply (rename_tac F)
lp15@69922
  1540
                apply (rule_tac x=F in exI)
lp15@69922
  1541
                using subsetD [OF \<F>]
lp15@69922
  1542
                apply (force intro: finite_intersection_of_inc)
lp15@69922
  1543
                done
lp15@69922
  1544
            qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
lp15@69922
  1545
          qed
lp15@69922
  1546
          ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
lp15@69922
  1547
            by (auto simp only: Int_Inter_eq split: if_split)
lp15@69922
  1548
        qed
lp15@69922
  1549
      next
lp15@69922
  1550
        have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
lp15@69922
  1551
          using PiE_arb V \<open>f \<in> V\<close> by force
lp15@69922
  1552
        show "f i \<in> ?T"
lp15@69922
  1553
          using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
lp15@69922
  1554
      next
lp15@69922
  1555
        show "?T \<subseteq> (\<lambda>f. f i) ` V"
lp15@69922
  1556
          unfolding V by (auto simp: intro!: rev_image_eqI)
lp15@69922
  1557
      qed
lp15@69922
  1558
    qed
lp15@69922
  1559
  qed
lp15@69922
  1560
qed
lp15@69922
  1561
lp15@69922
  1562
lemma retraction_map_product_projection:
lp15@69922
  1563
  assumes "i \<in> I"
lp15@69922
  1564
  shows "(retraction_map (product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
lp15@69922
  1565
         (topspace (product_topology X I) = {}) \<longrightarrow> topspace (X i) = {})"
lp15@69922
  1566
  (is "?lhs = ?rhs")
lp15@69922
  1567
proof
lp15@69922
  1568
  assume ?lhs
lp15@69922
  1569
  then show ?rhs
lp15@69922
  1570
    using retraction_imp_surjective_map by force
lp15@69922
  1571
next
lp15@69922
  1572
  assume R: ?rhs
lp15@69922
  1573
  show ?lhs
lp15@69922
  1574
  proof (cases "topspace (product_topology X I) = {}")
lp15@69922
  1575
    case True
lp15@69922
  1576
    then show ?thesis
lp15@69922
  1577
      using R by (auto simp: retraction_map_def retraction_maps_def continuous_map_on_empty)
lp15@69922
  1578
  next
lp15@69922
  1579
    case False
lp15@69922
  1580
    have *: "\<exists>g. continuous_map (X i) (product_topology X I) g \<and> (\<forall>x\<in>topspace (X i). g x i = x)"
lp15@69922
  1581
      if z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" for z
lp15@69922
  1582
    proof -
lp15@69922
  1583
      have cm: "continuous_map (X i) (X j) (\<lambda>x. if j = i then x else z j)" if "j \<in> I" for j
lp15@69922
  1584
        using \<open>j \<in> I\<close> z  by (case_tac "j = i") auto
lp15@69922
  1585
      show ?thesis
lp15@69922
  1586
        using \<open>i \<in> I\<close> that
lp15@69922
  1587
        by (rule_tac x="\<lambda>x j. if j = i then x else z j" in exI) (auto simp: continuous_map_componentwise PiE_iff extensional_def cm)
lp15@69922
  1588
    qed
lp15@69922
  1589
    show ?thesis
lp15@69922
  1590
      using \<open>i \<in> I\<close> False
lp15@69922
  1591
      by (auto simp: retraction_map_def retraction_maps_def assms continuous_map_product_projection *)
lp15@69922
  1592
  qed
lp15@69922
  1593
qed
lp15@69922
  1594
lp15@69939
  1595
subsection \<open>Open Pi-sets in the product topology\<close>
lp15@69939
  1596
lp15@69939
  1597
proposition openin_PiE_gen:
lp15@69939
  1598
  "openin (product_topology X I) (PiE I S) \<longleftrightarrow>
lp15@69939
  1599
        PiE I S = {} \<or>
lp15@69939
  1600
        finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
lp15@69939
  1601
  (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
lp15@69939
  1602
proof (cases "PiE I S = {}")
lp15@69939
  1603
  case False
lp15@69939
  1604
  moreover have "?lhs = ?rhs"
lp15@69939
  1605
  proof
lp15@69939
  1606
    assume L: ?lhs
lp15@69939
  1607
    moreover
lp15@69939
  1608
    obtain z where z: "z \<in> PiE I S"
lp15@69939
  1609
      using False by blast
lp15@69939
  1610
    ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
lp15@69939
  1611
      and "Pi\<^sub>E I U \<noteq> {}"
lp15@69939
  1612
      and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
lp15@69939
  1613
      by (fastforce simp add: openin_product_topology_alt)
lp15@69939
  1614
    then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
lp15@69939
  1615
      by (simp add: subset_PiE)
lp15@69939
  1616
    show ?rhs
lp15@69939
  1617
    proof (intro conjI ballI)
lp15@69939
  1618
      show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
lp15@69939
  1619
        apply (rule finite_subset [OF _ fin], clarify)
lp15@69939
  1620
        using *
lp15@69939
  1621
        by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
lp15@69939
  1622
    next
lp15@69939
  1623
      fix i :: "'a"
lp15@69939
  1624
      assume "i \<in> I"
lp15@69939
  1625
      then show "openin (X i) (S i)"
lp15@69939
  1626
        using open_map_product_projection [of i I X] L
lp15@69939
  1627
        apply (simp add: open_map_def)
lp15@69939
  1628
        apply (drule_tac x="PiE I S" in spec)
lp15@69939
  1629
        apply (simp add: False image_projection_PiE split: if_split_asm)
lp15@69939
  1630
        done
lp15@69939
  1631
    qed
lp15@69939
  1632
  next
lp15@69939
  1633
    assume ?rhs
lp15@69939
  1634
    then show ?lhs
lp15@69939
  1635
      apply (simp only: openin_product_topology)
lp15@69939
  1636
      apply (rule arbitrary_union_of_inc)
lp15@69939
  1637
      apply (auto simp: product_topology_base_alt)
lp15@69939
  1638
      done
lp15@69939
  1639
  qed
lp15@69939
  1640
  ultimately show ?thesis
lp15@69939
  1641
    by simp
lp15@69939
  1642
qed simp
lp15@69939
  1643
lp15@69939
  1644
lp15@69939
  1645
corollary openin_PiE:
lp15@69939
  1646
   "finite I \<Longrightarrow> openin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. openin (X i) (S i))"
lp15@69939
  1647
  by (simp add: openin_PiE_gen)
lp15@69939
  1648
lp15@69939
  1649
proposition compact_space_product_topology:
lp15@69939
  1650
   "compact_space(product_topology X I) \<longleftrightarrow>
lp15@69939
  1651
    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
lp15@69939
  1652
    (is "?lhs = ?rhs")
lp15@69939
  1653
proof (cases "topspace(product_topology X I) = {}")
lp15@69939
  1654
  case False
lp15@69939
  1655
  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
lp15@69939
  1656
    by auto
lp15@69939
  1657
  show ?thesis
lp15@69939
  1658
  proof
lp15@69939
  1659
    assume L: ?lhs
lp15@69939
  1660
    show ?rhs
lp15@69939
  1661
    proof (clarsimp simp add: False compact_space_def)
lp15@69939
  1662
      fix i
lp15@69939
  1663
      assume "i \<in> I"
lp15@69939
  1664
      with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
lp15@69939
  1665
        by (simp add: continuous_map_product_projection)
lp15@69939
  1666
      moreover
lp15@69939
  1667
      have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69939
  1668
        using \<open>i \<in> I\<close> z
lp15@69939
  1669
        apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
lp15@69939
  1670
        done
lp15@69939
  1671
      then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
lp15@69939
  1672
        using \<open>i \<in> I\<close> z by auto
lp15@69939
  1673
      ultimately show "compactin (X i) (topspace (X i))"
lp15@69939
  1674
        by (metis L compact_space_def image_compactin topspace_product_topology)
lp15@69939
  1675
    qed
lp15@69939
  1676
  next
lp15@69939
  1677
    assume R: ?rhs
lp15@69939
  1678
    show ?lhs
lp15@69939
  1679
    proof (cases "I = {}")
lp15@69939
  1680
      case True
lp15@69939
  1681
      with R show ?thesis
lp15@69939
  1682
        by (simp add: compact_space_def)
lp15@69939
  1683
    next
lp15@69939
  1684
      case False
lp15@69939
  1685
      then obtain i where "i \<in> I"
lp15@69939
  1686
        by blast
lp15@69939
  1687
      show ?thesis
lp15@69939
  1688
        using R
lp15@69939
  1689
      proof
lp15@69939
  1690
        assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
lp15@69939
  1691
        let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
lp15@69939
  1692
        show "compact_space (product_topology X I)"
lp15@69939
  1693
        proof (rule Alexander_subbase_alt)
lp15@69939
  1694
          show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
lp15@69939
  1695
            unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
lp15@69939
  1696
        next
lp15@69939
  1697
          fix C
lp15@69939
  1698
          assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
lp15@69939
  1699
          define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
lp15@69939
  1700
          show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
lp15@69939
  1701
          proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
lp15@69939
  1702
            case True
lp15@69939
  1703
            then obtain i where "i \<in> I"
lp15@69939
  1704
                   and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
lp15@69939
  1705
              unfolding \<D>_def by blast
lp15@69939
  1706
            then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
lp15@69939
  1707
                            \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
lp15@69939
  1708
              using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
lp15@69939
  1709
            have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
lp15@69939
  1710
              using i by auto
lp15@69939
  1711
            with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
lp15@69939
  1712
              unfolding \<D>_def by fastforce
lp15@69939
  1713
            with \<open>i \<in> I\<close> show ?thesis
lp15@69939
  1714
              unfolding \<D>_def
lp15@69939
  1715
              by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
lp15@69939
  1716
          next
lp15@69939
  1717
            case False
lp15@69939
  1718
            then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
lp15@69939
  1719
              by force
lp15@69939
  1720
            then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
lp15@69939
  1721
              by metis
lp15@69939
  1722
            then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
lp15@69939
  1723
              by (simp add: PiE_I)
lp15@69939
  1724
            moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
lp15@69939
  1725
              using Csub g unfolding \<D>_def by force
lp15@69939
  1726
            ultimately show ?thesis
lp15@69939
  1727
              using UC by blast
lp15@69939
  1728
          qed
lp15@69939
  1729
        qed (simp add: product_topology)
lp15@69939
  1730
      qed (simp add: compact_space_topspace_empty)
lp15@69939
  1731
    qed
lp15@69939
  1732
  qed
lp15@69939
  1733
qed (simp add: compact_space_topspace_empty)
lp15@69939
  1734
lp15@69939
  1735
corollary compactin_PiE:
lp15@69939
  1736
   "compactin (product_topology X I) (PiE I S) \<longleftrightarrow>
lp15@69939
  1737
        PiE I S = {} \<or> (\<forall>i \<in> I. compactin (X i) (S i))"
lp15@69939
  1738
  by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology
lp15@69939
  1739
       PiE_eq_empty_iff)
lp15@69939
  1740
lp15@69939
  1741
lemma in_product_topology_closure_of:
lp15@69939
  1742
   "z \<in> (product_topology X I) closure_of S
lp15@69939
  1743
        \<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
lp15@69939
  1744
  using continuous_map_product_projection
lp15@69939
  1745
  by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)
lp15@69939
  1746
lp15@69939
  1747
lemma homeomorphic_space_singleton_product:
lp15@69939
  1748
   "product_topology X {k} homeomorphic_space (X k)"
lp15@69939
  1749
  unfolding homeomorphic_space
lp15@69939
  1750
  apply (rule_tac x="\<lambda>x. x k" in exI)
lp15@69939
  1751
  apply (rule bijective_open_imp_homeomorphic_map)
lp15@69939
  1752
     apply (simp_all add: continuous_map_product_projection open_map_product_projection)
lp15@69939
  1753
  unfolding PiE_over_singleton_iff
lp15@69939
  1754
   apply (auto simp: image_iff inj_on_def)
lp15@69939
  1755
  done
lp15@69939
  1756
lp15@69945
  1757
subsection\<open>Relationship with connected spaces, paths, etc.\<close>
lp15@69945
  1758
lp15@69945
  1759
proposition connected_space_product_topology:
lp15@69945
  1760
   "connected_space(product_topology X I) \<longleftrightarrow>
lp15@69945
  1761
    (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
lp15@69945
  1762
  (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
lp15@69945
  1763
proof (cases ?eq)
lp15@69945
  1764
  case False
lp15@69945
  1765
  moreover have "?lhs = ?rhs"
lp15@69945
  1766
  proof
lp15@69945
  1767
    assume ?lhs
lp15@69945
  1768
    moreover
lp15@69945
  1769
    have "connectedin(X i) (topspace(X i))"
lp15@69945
  1770
      if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
lp15@69945
  1771
    proof -
lp15@69945
  1772
      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
lp15@69945
  1773
        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
lp15@69945
  1774
      show ?thesis
lp15@69945
  1775
        using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
lp15@69945
  1776
        by (simp add: False image_projection_PiE)
lp15@69945
  1777
    qed
lp15@69945
  1778
    ultimately show ?rhs
lp15@69945
  1779
      by (meson connectedin_topspace)
lp15@69945
  1780
  next
lp15@69945
  1781
    assume cs [rule_format]: ?rhs
lp15@69945
  1782
    have False
lp15@69945
  1783
      if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
lp15@69945
  1784
        and U: "openin (product_topology X I) U"
lp15@69945
  1785
        and V: "openin (product_topology X I) V"
lp15@69945
  1786
        and "U \<noteq> {}" "V \<noteq> {}"
lp15@69945
  1787
      for U V
lp15@69945
  1788
    proof -
lp15@69945
  1789
      obtain f where "f \<in> U"
lp15@69945
  1790
        using \<open>U \<noteq> {}\<close> by blast
lp15@69945
  1791
      then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69945
  1792
        using U openin_subset by fastforce
lp15@69945
  1793
      have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
lp15@69945
  1794
        using U V openin_subset by blast+
lp15@69945
  1795
      moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
lp15@69945
  1796
      proof -
lp15@69945
  1797
        obtain C where "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
lp15@69945
  1798
            (\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
lp15@69945
  1799
          using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
lp15@69945
  1800
        then obtain \<T> where "finite \<T>"
lp15@69945
  1801
          and t: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i u. (i \<in> I \<and> openin (X i) u) \<and> C = {x. x i \<in> u}"
lp15@69945
  1802
          and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
lp15@69945
  1803
          and ftop: "f \<in> topspace (product_topology X I)"
lp15@69945
  1804
          and fint: "f \<in> \<Inter> \<T>"
lp15@69945
  1805
          by (fastforce simp: relative_to_def intersection_of_def subset_iff)
lp15@69945
  1806
        let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
lp15@69945
  1807
        obtain L where "finite L"
lp15@69945
  1808
          and L: "\<And>i U. \<lbrakk>i \<in> I; openin (X i) U; U \<subset> topspace(X i); {x. x i \<in> U} \<in> \<T>\<rbrakk> \<Longrightarrow> i \<in> L"
lp15@69945
  1809
        proof
lp15@69945
  1810
          show "finite ?L"
lp15@69945
  1811
          proof (rule finite_Union)
lp15@69945
  1812
            fix M
lp15@69945
  1813
            assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
lp15@69945
  1814
            then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
lp15@69945
  1815
              by blast
lp15@69945
  1816
            then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
lp15@69945
  1817
              using t by meson
lp15@69945
  1818
            then have "f j \<in> V"
lp15@69945
  1819
              using \<open>C \<in> \<T>\<close> fint by force
lp15@69945
  1820
            then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
lp15@69945
  1821
              using that
lp15@69945
  1822
              apply (clarsimp simp add: set_eq_iff)
lp15@69945
  1823
              apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
lp15@69945
  1824
              done
lp15@69945
  1825
            then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
lp15@69945
  1826
              using Ceq by auto
lp15@69945
  1827
            then show "finite M"
lp15@69945
  1828
              using C finite_subset by fastforce
lp15@69945
  1829
          qed (use \<open>finite \<T>\<close> in blast)
lp15@69945
  1830
        next
lp15@69945
  1831
          fix i U
lp15@69945
  1832
          assume  "i \<in> I" and ope: "openin (X i) U" and psub: "U \<subset> topspace (X i)" and int: "{x. x i \<in> U} \<in> \<T>"
lp15@69945
  1833
          then show "i \<in> ?L"
lp15@69945
  1834
            by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
lp15@69945
  1835
        qed
lp15@69945
  1836
        show ?thesis
lp15@69945
  1837
        proof
lp15@69945
  1838
          fix h
lp15@69945
  1839
          assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69945
  1840
          define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
lp15@69945
  1841
          have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69945
  1842
            unfolding g_def using f h by auto
lp15@69945
  1843
          moreover have "g \<in> X" if "X \<in> \<T>" for X
lp15@69945
  1844
            using fint openin_subset t [OF that] L g_def h that by fastforce
lp15@69945
  1845
          ultimately have "g \<in> U"
lp15@69945
  1846
            using subU by auto
lp15@69945
  1847
          have "h \<in> U" if "finite M" "h \<in> PiE I (topspace \<circ> X)" "{i \<in> I. h i \<noteq> g i} \<subseteq> M" for M h
lp15@69945
  1848
            using that
lp15@69945
  1849
          proof (induction arbitrary: h)
lp15@69945
  1850
            case empty
lp15@69945
  1851
            then show ?case
lp15@69945
  1852
              using PiE_ext \<open>g \<in> U\<close> gin by force
lp15@69945
  1853
          next
lp15@69945
  1854
            case (insert i M)
lp15@69945
  1855
            define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
lp15@69945
  1856
            have fin: "f \<in> PiE I (topspace \<circ> X)"
lp15@69945
  1857
              unfolding f_def using gin insert.prems(1) by auto
lp15@69945
  1858
            have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
lp15@69945
  1859
              unfolding f_def using insert.prems(2) by auto
lp15@69945
  1860
            have "f \<in> U"
lp15@69945
  1861
              using insert.IH [OF fin subM] .
lp15@69945
  1862
            show ?case
lp15@69945
  1863
            proof (cases "h \<in> V")
lp15@69945
  1864
              case True
lp15@69945
  1865
              show ?thesis
lp15@69945
  1866
              proof (cases "i \<in> I")
lp15@69945
  1867
                case True
lp15@69945
  1868
                let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
lp15@69945
  1869
                let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
lp15@69945
  1870
                have False
lp15@69945
  1871
                proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
lp15@69945
  1872
                  have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
lp15@69945
  1873
                    using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
lp15@69945
  1874
                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
lp15@69945
  1875
                    using \<open>i \<in> I\<close> insert.prems(1)
lp15@69945
  1876
                    by (auto simp: continuous_map_componentwise extensional_def)
lp15@69945
  1877
                  show "openin (X i) ?U"
lp15@69945
  1878
                    by (rule openin_continuous_map_preimage [OF cm U])
lp15@69945
  1879
                  show "openin (X i) ?V"
lp15@69945
  1880
                    by (rule openin_continuous_map_preimage [OF cm V])
lp15@69945
  1881
                  show "topspace (X i) \<subseteq> ?U \<union> ?V"
lp15@69945
  1882
                  proof clarsimp
lp15@69945
  1883
                    fix x
lp15@69945
  1884
                    assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
lp15@69945
  1885
                    with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
lp15@69945
  1886
                    show "(\<lambda>j. if j = i then x else h j) \<in> U"
lp15@69945
  1887
                      by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
lp15@69945
  1888
                  qed
lp15@69945
  1889
                  show "?U \<inter> ?V = {}"
lp15@69945
  1890
                    using disj by blast
lp15@69945
  1891
                  show "?U \<noteq> {}"
lp15@69945
  1892
                    using \<open>U \<noteq> {}\<close> f_def
lp15@69945
  1893
                  proof -
lp15@69945
  1894
                    have "(\<lambda>j. if j = i then g i else h j) \<in> U"
lp15@69945
  1895
                      using \<open>f \<in> U\<close> f_def by blast
lp15@69945
  1896
                    moreover have "f i \<in> topspace (X i)"
lp15@69945
  1897
                      by (metis PiE_iff True comp_apply fin)
lp15@69945
  1898
                    ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
lp15@69945
  1899
                      using f_def by auto
lp15@69945
  1900
                    then show ?thesis
lp15@69945
  1901
                      by blast
lp15@69945
  1902
                  qed
lp15@69945
  1903
                  have "(\<lambda>j. if j = i then h i else h j) = h"
lp15@69945
  1904
                    by force
lp15@69945
  1905
                  moreover have "h i \<in> topspace (X i)"
lp15@69945
  1906
                    using True insert.prems(1) by auto
lp15@69945
  1907
                  ultimately show "?V \<noteq> {}"
lp15@69945
  1908
                    using \<open>h \<in> V\<close>  by force
lp15@69945
  1909
                qed
lp15@69945
  1910
                then show ?thesis ..
lp15@69945
  1911
              next
lp15@69945
  1912
                case False
lp15@69945
  1913
                show ?thesis
lp15@69945
  1914
                proof (cases "h = f")
lp15@69945
  1915
                  case True
lp15@69945
  1916
                  show ?thesis
lp15@69945
  1917
                    by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
lp15@69945
  1918
                next
lp15@69945
  1919
                  case False
lp15@69945
  1920
                  then show ?thesis
lp15@69945
  1921
                    using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
lp15@69945
  1922
                qed
lp15@69945
  1923
              qed
lp15@69945
  1924
            next
lp15@69945
  1925
              case False
lp15@69945
  1926
              then show ?thesis
lp15@69945
  1927
                using subUV insert.prems(1) by auto
lp15@69945
  1928
            qed
lp15@69945
  1929
          qed
lp15@69945
  1930
          then show "h \<in> U"
lp15@69945
  1931
            unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
lp15@69945
  1932
        qed
lp15@69945
  1933
      qed
lp15@69945
  1934
      ultimately show ?thesis
lp15@69945
  1935
        using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
lp15@69945
  1936
    qed
lp15@69945
  1937
    then show ?lhs
lp15@69945
  1938
      unfolding connected_space_def
lp15@69945
  1939
      by auto
lp15@69945
  1940
  qed
lp15@69945
  1941
  ultimately show ?thesis
lp15@69945
  1942
    by simp
lp15@69945
  1943
qed (simp add: connected_space_topspace_empty)
lp15@69945
  1944
lp15@69945
  1945
lp15@69945
  1946
lemma connectedin_PiE:
lp15@69945
  1947
   "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
lp15@69945
  1948
        PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
lp15@69945
  1949
  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
lp15@69945
  1950
      topspace_subtopology_subset)
lp15@69945
  1951
lp15@69945
  1952
lemma path_connected_space_product_topology:
lp15@69945
  1953
   "path_connected_space(product_topology X I) \<longleftrightarrow>
lp15@69945
  1954
    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
lp15@69945
  1955
 (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
lp15@69945
  1956
proof (cases ?eq)
lp15@69945
  1957
  case False
lp15@69945
  1958
  moreover have "?lhs = ?rhs"
lp15@69945
  1959
  proof
lp15@69945
  1960
    assume L: ?lhs
lp15@69945
  1961
    show ?rhs
lp15@69945
  1962
    proof (clarsimp simp flip: path_connectedin_topspace)
lp15@69945
  1963
      fix i :: "'a"
lp15@69945
  1964
      assume "i \<in> I"
lp15@69945
  1965
      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
lp15@69945
  1966
        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
lp15@69945
  1967
      show "path_connectedin (X i) (topspace (X i))"
lp15@69945
  1968
        using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
lp15@69945
  1969
        by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
lp15@69945
  1970
    qed
lp15@69945
  1971
  next
lp15@69945
  1972
    assume R [rule_format]: ?rhs
lp15@69945
  1973
    show ?lhs
lp15@69945
  1974
      unfolding path_connected_space_def topspace_product_topology
lp15@69945
  1975
    proof clarify
lp15@69945
  1976
      fix x y
lp15@69945
  1977
      assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and y: "y \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
lp15@69945
  1978
      have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
lp15@69945
  1979
        using PiE_mem R path_connected_space_def x y by force
lp15@69945
  1980
      then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> pathin (X i) (g i) \<and> g i 0 = x i \<and> g i 1 = y i"
lp15@69945
  1981
        by metis
lp15@69945
  1982
      with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
lp15@69945
  1983
        apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
lp15@69945
  1984
        apply (force simp: pathin_def continuous_map_componentwise)
lp15@69945
  1985
        done
lp15@69945
  1986
    qed
lp15@69945
  1987
  qed
lp15@69945
  1988
  ultimately show ?thesis
lp15@69945
  1989
    by simp
lp15@69945
  1990
qed (simp add: path_connected_space_topspace_empty)
lp15@69945
  1991
lp15@69945
  1992
lemma path_connectedin_PiE:
lp15@69945
  1993
   "path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
lp15@69945
  1994
    PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
lp15@69945
  1995
  by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
lp15@69945
  1996
lp15@69945
  1997
hoelzl@64289
  1998
end