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