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