diff -r 4750673a96da -r 42f28160bad9 src/HOL/Analysis/Function_Topology.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Oct 18 17:29:28 2016 +0200
@@ -0,0 +1,1392 @@
+(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+    License: BSD
+*)
+
+theory Function_Topology
+imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
+begin
+
+
+section {*Product topology*}
+
+text {*We want to define the product topology.
+
+The product topology on a product of topological spaces is generated by
+the sets which are products of open sets along finitely many coordinates, and the whole
+space along the other coordinates. This is the coarsest topology for which the projection
+to each factor is continuous.
+
+To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
+'a. The product is then @{term "PiE I X"}, the set of elements from 'i to 'a such that the $i$-th
+coordinate belongs to $X\;i$ for all $i \in I$.
+
+Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
+This means that type classes can not be used to define such a product if one wants to take the
+product of different topological spaces (as the type 'a can only be given one structure of
+topological space using type classes). On the other hand, one can define different topologies (as
+introduced in \verb+Topology_Euclidean_Space.thy+) on one type, and these topologies do not need to
+share the same maximal open set. Hence, one can form a product of topologies in this sense, and
+this works well. The big caveat is that it does not interact well with the main body of
+topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
+is not defined in this setting.
+
+As the product of different topological spaces is very important in several areas of
+mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
+and reformulate afterwards the consequences in terms of type classes (which are of course very
+handy for applications).
+
+Given this limitation, it looks to me that it would be very beneficial to revamp the theory
+of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
+type classes as consequences of more general statements in terms of topologies (but I am
+probably too naive here).
+
+Here is an example of a reformulation using topologies. Let
+\begin{verbatim}
+continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
+                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
+\end{verbatim}
+be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
+the current \verb+continuous_on+ (with type classes) can be redefined as
+\begin{verbatim}
+continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
+\end{verbatim}
+
+In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
+for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
+the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
+
+I only develop the basics of the product topology in this theory. The most important missing piece
+is Tychonov theorem, stating that a product of compact spaces is always compact for the product
+topology, even when the product is not finite (or even countable).
+
+I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
+*}
+
+subsection {*Topology without type classes*}
+
+subsubsection {*The topology generated by some (open) subsets*}
+
+text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
+as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
+and is never a problem in proofs, so I prefer to write it down explicitly.
+
+We do not require UNIV to be an open set, as this will not be the case in applications. (We are
+thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)*}
+
+inductive generate_topology_on for S where
+Empty: "generate_topology_on S {}"
+|Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
+| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
+| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
+
+lemma istopology_generate_topology_on:
+  "istopology (generate_topology_on S)"
+unfolding istopology_def by (auto intro: generate_topology_on.intros)
+
+text {*The basic property of the topology generated by a set $S$ is that it is the
+smallest topology containing all the elements of $S$:*}
+
+lemma generate_topology_on_coarsest:
+  assumes "istopology T"
+          "\<And>s. s \<in> S \<Longrightarrow> T s"
+          "generate_topology_on S s0"
+  shows "T s0"
+using assms(3) apply (induct rule: generate_topology_on.induct)
+using assms(1) assms(2) unfolding istopology_def by auto
+
+definition topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+  where "topology_generated_by S = topology (generate_topology_on S)"
+
+lemma openin_topology_generated_by_iff:
+  "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
+using topology_inverse'[OF istopology_generate_topology_on[of S]]
+unfolding topology_generated_by_def by simp
+
+lemma openin_topology_generated_by:
+  "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
+using openin_topology_generated_by_iff by auto
+
+lemma topology_generated_by_topspace:
+  "topspace (topology_generated_by S) = (\<Union>S)"
+proof
+  {
+    fix s assume "openin (topology_generated_by S) s"
+    then have "generate_topology_on S s" by (rule openin_topology_generated_by)
+    then have "s \<subseteq> (\<Union>S)" by (induct, auto)
+  }
+  then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
+    unfolding topspace_def by auto
+next
+  have "generate_topology_on S (\<Union>S)"
+    using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
+  then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
+    unfolding topspace_def using openin_topology_generated_by_iff by auto
+qed
+
+lemma topology_generated_by_Basis:
+  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
+by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
+
+subsubsection {*Continuity*}
+
+text {*We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.*}
+
+definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
+                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
+
+lemma continuous_on_continuous_on_topo:
+  "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
+unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
+topspace_euclidean_subtopology open_openin topspace_euclidean by fast
+
+lemma continuous_on_topo_UNIV:
+  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
+using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
+
+lemma continuous_on_topo_open [intro]:
+  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+unfolding continuous_on_topo_def by auto
+
+lemma continuous_on_topo_topspace [intro]:
+  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
+unfolding continuous_on_topo_def by auto
+
+lemma continuous_on_generated_topo_iff:
+  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
+      ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
+unfolding continuous_on_topo_def topology_generated_by_topspace
+proof (auto simp add: topology_generated_by_Basis)
+  assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
+  fix U assume "openin (topology_generated_by S) U"
+  then have "generate_topology_on S U" by (rule openin_topology_generated_by)
+  then show "openin T1 (f -` U \<inter> topspace T1)"
+  proof (induct)
+    fix a b
+    assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
+    have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
+      by auto
+    then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
+  next
+    fix K
+    assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
+    define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
+    have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
+    have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
+    moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
+    ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
+  qed (auto simp add: H)
+qed
+
+lemma continuous_on_generated_topo:
+  assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+          "f`(topspace T1) \<subseteq> (\<Union> S)"
+  shows "continuous_on_topo T1 (topology_generated_by S) f"
+using assms continuous_on_generated_topo_iff by blast
+
+lemma continuous_on_topo_compose:
+  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
+  shows "continuous_on_topo T1 T3 (g o f)"
+using assms unfolding continuous_on_topo_def
+proof (auto)
+  fix U :: "'c set"
+  assume H: "openin T3 U"
+  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
+    using H assms by blast
+  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
+    using H assms continuous_on_topo_topspace by fastforce
+  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
+    by simp
+qed (blast)
+
+lemma continuous_on_topo_preimage_topspace [intro]:
+  assumes "continuous_on_topo T1 T2 f"
+  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
+using assms unfolding continuous_on_topo_def by auto
+
+
+subsubsection {*Pullback topology*}
+
+text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
+a special case of this notion, pulling back by the identity. We introduce the general notion as
+we will need it to define the strong operator topology on the space of continuous linear operators,
+by pulling back the product topology on the space of all functions.*}
+
+text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
+the set $A$.*}
+
+definition pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
+  where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+
+lemma istopology_pullback_topology:
+  "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+unfolding istopology_def proof (auto)
+  fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
+  then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
+    by (rule bchoice)
+  then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
+    by blast
+  define V where "V = (\<Union>S\<in>K. U S)"
+  have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
+  then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
+qed
+
+lemma openin_pullback_topology:
+  "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
+
+lemma topspace_pullback_topology:
+  "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
+by (auto simp add: topspace_def openin_pullback_topology)
+
+lemma continuous_on_topo_pullback [intro]:
+  assumes "continuous_on_topo T1 T2 g"
+  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
+unfolding continuous_on_topo_def
+proof (auto)
+  fix U::"'b set" assume "openin T2 U"
+  then have "openin T1 (g-`U \<inter> topspace T1)"
+    using assms unfolding continuous_on_topo_def by auto
+  have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
+    unfolding topspace_pullback_topology by auto
+  also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
+    by auto
+  also have "openin (pullback_topology A f T1) (...)"
+    unfolding openin_pullback_topology using `openin T1 (g-\`U \<inter> topspace T1)` by auto
+  finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
+    by auto
+next
+  fix x assume "x \<in> topspace (pullback_topology A f T1)"
+  then have "f x \<in> topspace T1"
+    unfolding topspace_pullback_topology by auto
+  then show "g (f x) \<in> topspace T2"
+    using assms unfolding continuous_on_topo_def by auto
+qed
+
+lemma continuous_on_topo_pullback' [intro]:
+  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
+  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
+unfolding continuous_on_topo_def
+proof (auto)
+  fix U assume "openin (pullback_topology A f T2) U"
+  then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
+    unfolding openin_pullback_topology by auto
+  then obtain V where "openin T2 V" "U = f-`V \<inter> A"
+    by blast
+  then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
+    by blast
+  also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
+    by auto
+  also have "... = (f o g)-`V \<inter> topspace T1"
+    using assms(2) by auto
+  also have "openin T1 (...)"
+    using assms(1) `openin T2 V` by auto
+  finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
+next
+  fix x assume "x \<in> topspace T1"
+  have "(f o g) x \<in> topspace T2"
+    using assms(1) `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+  then have "g x \<in> f-`(topspace T2)"
+    unfolding comp_def by blast
+  moreover have "g x \<in> A" using assms(2) `x \<in> topspace T1` by blast
+  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
+    unfolding topspace_pullback_topology by blast
+qed
+
+subsubsection {*Miscellaneous*}
+
+text {*The following could belong to \verb+Topology_Euclidean_Spaces.thy+, and will be needed
+below.*}
+lemma openin_INT [intro]:
+  assumes "finite I"
+          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+  shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
+using assms by (induct, auto simp add: inf_sup_aci(2) openin_Int)
+
+lemma openin_INT2 [intro]:
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+  shows "openin T (\<Inter>i \<in> I. U i)"
+proof -
+  have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
+    using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
+  then show ?thesis
+    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
+qed
+
+
+subsection {*The product topology*}
+
+text {*We can now define the product topology, as generated by
+the sets which are products of open sets along finitely many coordinates, and the whole
+space along the other coordinates. Equivalently, it is generated by sets which are one open
+set along one single coordinate, and the whole space along other coordinates. In fact, this is only
+equivalent for nonempty products, but for the empty product the first formulation is better
+(the second one gives an empty product space, while an empty product should have exactly one
+point, equal to \verb+undefined+ along all coordinates.
+
+So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
+*}
+
+definition product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
+  where "product_topology T I =
+    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)}}"
+
+text {*The total set of the product topology is the product of the total sets
+along each coordinate.*}
+
+lemma product_topology_topspace:
+  "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
+proof
+  show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
+    unfolding product_topology_def apply (simp only: topology_generated_by_topspace)
+    unfolding topspace_def by auto
+  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)}}"
+    using openin_topspace not_finite_existsD by auto
+  then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
+    unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
+qed
+
+lemma product_topology_basis:
+  assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
+  shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
+unfolding product_topology_def apply (rule topology_generated_by_Basis) using assms by auto
+
+lemma product_topology_open_contains_basis:
+  assumes "openin (product_topology T I) U"
+          "x \<in> U"
+  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"
+proof -
+  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"
+    using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
+  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"
+  proof induction
+    case (Int U V x)
+    then obtain XU XV where H:
+      "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"
+      "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"
+      by auto meson
+    define X where "X = (\<lambda>i. XU i \<inter> XV i)"
+    have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
+      unfolding X_def by (auto simp add: PiE_iff)
+    then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
+    moreover have "\<forall>i. openin (T i) (X i)"
+      unfolding X_def using H by auto
+    moreover have "finite {i. X i \<noteq> topspace (T i)}"
+      apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
+      unfolding X_def using H by auto
+    moreover have "x \<in> Pi\<^sub>E I X"
+      unfolding X_def using H by auto
+    ultimately show ?case
+      by auto
+  next
+    case (UN K x)
+    then obtain k where "k \<in> K" "x \<in> k" by auto
+    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"
+      by simp
+    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"
+      by blast
+    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)"
+      using `k \<in> K` by auto
+    then show ?case
+      by auto
+  qed auto
+  then show ?thesis using `x \<in> U` by auto
+qed
+
+
+text {*The basic property of the product topology is the continuity of projections:*}
+
+lemma continuous_on_topo_product_coordinates [simp]:
+  assumes "i \<in> I"
+  shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
+proof -
+  {
+    fix U assume "openin (T i) U"
+    define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
+    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)"
+      unfolding X_def using assms openin_subset[OF `openin (T i) U`]
+      by (auto simp add: PiE_iff, auto, metis subsetCE)
+    have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
+      unfolding X_def using `openin (T i) U` by auto
+    have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
+      unfolding product_topology_def
+      apply (rule topology_generated_by_Basis)
+      apply (subst *)
+      using ** by auto
+  }
+  then show ?thesis unfolding continuous_on_topo_def
+    by (auto simp add: assms product_topology_topspace PiE_iff)
+qed
+
+lemma continuous_on_topo_coordinatewise_then_product [intro]:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+          "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
+  shows "continuous_on_topo T1 (product_topology T I) f"
+unfolding product_topology_def
+proof (rule continuous_on_generated_topo)
+  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)}}"
+  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)}"
+    by blast
+  define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
+  have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
+  have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
+    using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
+  then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
+    using that unfolding J_def by auto
+  have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
+    by (subst H(1), auto simp add: PiE_iff assms)
+  also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
+    using * `J \<subseteq> I` by auto
+  also have "openin T1 (...)"
+    apply (rule openin_INT)
+    apply (simp add: `finite J`)
+    using H(2) assms(1) `J \<subseteq> I` by auto
+  ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
+next
+  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)}}"
+    apply (subst topology_generated_by_topspace[symmetric])
+    apply (subst product_topology_def[symmetric])
+    apply (simp only: product_topology_topspace)
+    apply (auto simp add: PiE_iff)
+    using assms unfolding continuous_on_topo_def by auto
+qed
+
+lemma continuous_on_topo_product_then_coordinatewise [intro]:
+  assumes "continuous_on_topo T1 (product_topology T I) f"
+  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+        "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
+proof -
+  fix i assume "i \<in> I"
+  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
+  also have "continuous_on_topo T1 (T i) (...)"
+    apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
+    using assms `i \<in> I` by auto
+  ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+    by simp
+next
+  fix i x assume "i \<notin> I" "x \<in> topspace T1"
+  have "f x \<in> topspace (product_topology T I)"
+    using assms `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+  then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
+    using product_topology_topspace by metis
+  then show "f x i = undefined"
+    using `i \<notin> I` by (auto simp add: PiE_iff extensional_def)
+qed
+
+lemma continuous_on_restrict:
+  assumes "J \<subseteq> I"
+  shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
+proof (rule continuous_on_topo_coordinatewise_then_product)
+  fix i assume "i \<in> J"
+  then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
+  then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
+    using `i \<in> J` `J \<subseteq> I` by auto
+next
+  fix i assume "i \<notin> J"
+  then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
+    unfolding restrict_def by auto
+qed
+
+
+subsubsection {*Powers of a single topological space as a topological space, using type classes*}
+
+instantiation "fun" :: (type, topological_space) topological_space
+begin
+
+definition open_fun_def:
+  "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+
+instance proof
+  have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
+    unfolding product_topology_topspace topspace_euclidean by auto
+  then show "open (UNIV::('a \<Rightarrow> 'b) set)"
+    unfolding open_fun_def by (metis openin_topspace)
+qed (auto simp add: open_fun_def)
+
+end
+
+lemma euclidean_product_topology:
+  "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
+by (metis open_openin topology_eq open_fun_def)
+
+lemma product_topology_basis':
+  fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
+  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+  shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
+proof -
+  define J where "J = x`I"
+  define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
+  define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
+  have *: "open (X i)" for i
+    unfolding X_def V_def using assms by auto
+  have **: "finite {i. X i \<noteq> UNIV}"
+    unfolding X_def V_def J_def using assms(1) by auto
+  have "open (Pi\<^sub>E UNIV X)"
+    unfolding open_fun_def apply (rule product_topology_basis)
+    using * ** unfolding open_openin topspace_euclidean by auto
+  moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
+    apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
+    proof (auto)
+      fix f :: "'a \<Rightarrow> 'b" and i :: 'i
+      assume a1: "i \<in> I"
+      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)"
+      have f3: "x i \<in> x`I"
+        using a1 by blast
+      have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
+        using a1 by blast
+      then show "f (x i) \<in> U i"
+        using f3 a2 by (meson Inter_iff)
+    qed
+  ultimately show ?thesis by simp
+qed
+
+text {*The results proved in the general situation of products of possibly different
+spaces have their counterparts in this simpler setting.*}
+
+lemma continuous_on_product_coordinates [simp]:
+  "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
+unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_product_coordinates, simp)
+
+lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+  assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
+  shows "continuous_on UNIV f"
+using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_coordinatewise_then_product, simp)
+
+lemma continuous_on_product_then_coordinatewise:
+  assumes "continuous_on UNIV f"
+  shows "continuous_on UNIV (\<lambda>x. f x i)"
+using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
+
+lemma continuous_on_product_coordinatewise_iff:
+  "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
+by (auto intro: continuous_on_product_then_coordinatewise)
+
+subsubsection {*Topological countability for product spaces*}
+
+text {*The next two lemmas are useful to prove first or second countability
+of product spaces, but they have more to do with countability and could
+be put in the corresponding theory.*}
+
+lemma countable_nat_product_event_const:
+  fixes F::"'a set" and a::'a
+  assumes "a \<in> F" "countable F"
+  shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
+proof -
+  have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
+                  \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
+    using infinite_nat_iff_unbounded_le by fastforce
+  have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
+  proof (induction N)
+    case 0
+    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
+      using `a \<in> F` by auto
+    then show ?case by auto
+  next
+    case (Suc N)
+    define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
+      where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
+    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)"
+    proof (auto)
+      fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
+      define y where "y = (\<lambda>i. if i = N then a else x i)"
+      have "f (y, x N) = x"
+        unfolding f_def y_def by auto
+      moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
+        unfolding y_def using H `a \<in> F` by auto
+      ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+        by (metis (no_types, lifting) image_eqI)
+    qed
+    moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+      using Suc.IH assms(2) by auto
+    ultimately show ?case
+      by (meson countable_image countable_subset)
+  qed
+  then show ?thesis using countable_subset[OF *] by auto
+qed
+
+lemma countable_product_event_const:
+  fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
+  assumes "\<And>i. countable (F i)"
+  shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
+proof -
+  define G where "G = (\<Union>i. F i) \<union> {b}"
+  have "countable G" unfolding G_def using assms by auto
+  have "b \<in> G" unfolding G_def by auto
+  define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
+  have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
+        \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
+  proof (auto)
+    fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
+    define I where "I = {i. f i \<noteq> b}"
+    define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
+    have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
+    then have "finite {j. g j \<noteq> b}"
+      unfolding I_def using H(2) using finite_surj by blast
+    moreover have "g j \<in> G" for j
+      unfolding g_def G_def using H by auto
+    ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
+      by auto
+    moreover have "f = pi g"
+      unfolding pi_def g_def I_def using H by fastforce
+    ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
+      by auto
+  qed
+  then show ?thesis
+    using countable_nat_product_event_const[OF `b \<in> G` `countable G`]
+    by (meson countable_image countable_subset)
+qed
+
+instance "fun" :: (countable, first_countable_topology) first_countable_topology
+proof
+  fix x::"'a \<Rightarrow> 'b"
+  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))"
+    apply (rule choice) using first_countable_basis by auto
+  then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
+                                                  "\<And>x i. open (A x i)"
+                                                  "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
+    by metis
+  text {*$B i$ is a countable basis of neighborhoods of $x_i$.*}
+  define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
+  have "countable (B i)" for i unfolding B_def by auto
+
+  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
+  have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
+    unfolding K_def B_def by auto
+  then have "K \<noteq> {}" by auto
+  have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
+    apply (rule countable_product_event_const) using `\<And>i. countable (B i)` by auto
+  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}}"
+    unfolding K_def by auto
+  ultimately have "countable K" by auto
+  have "x \<in> k" if "k \<in> K" for k
+    using that unfolding K_def B_def apply auto using A(1) by auto
+  have "open k" if "k \<in> K" for k
+    using that unfolding open_fun_def K_def B_def apply (auto)
+    apply (rule product_topology_basis)
+    unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
+
+  have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
+  proof -
+    have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
+      using `open U \<and> x \<in> U` unfolding open_fun_def by auto
+    with product_topology_open_contains_basis[OF this]
+    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"
+      unfolding topspace_euclidean open_openin by simp
+    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+                           "\<And>i. open (X i)"
+                           "finite {i. X i \<noteq> UNIV}"
+                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+      by auto
+    define I where "I = {i. X i \<noteq> UNIV}"
+    define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
+    have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
+      unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
+    have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
+      apply (cases "i \<in> I")
+      unfolding Y_def using * that apply (auto)
+      apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
+      unfolding B_def apply simp
+      unfolding I_def apply auto
+      done
+    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
+      unfolding Y_def by auto
+    then have ***: "finite {i. Y i \<noteq> UNIV}"
+      unfolding I_def using H(3) rev_finite_subset by blast
+    have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
+      using ** *** by auto
+    then have "Pi\<^sub>E UNIV Y \<in> K"
+      unfolding K_def by auto
+
+    have "Y i \<subseteq> X i" for i
+      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+    then show ?thesis using `Pi\<^sub>E UNIV Y \<in> K` by auto
+  qed
+
+  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))"
+    apply (rule first_countableI[of K])
+    using `countable K` `\<And>k. k \<in> K \<Longrightarrow> x \<in> k` `\<And>k. k \<in> K \<Longrightarrow> open k` Inc by auto
+qed
+
+lemma product_topology_countable_basis:
+  shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
+          topological_basis K \<and> countable K \<and>
+          (\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
+proof -
+  obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
+    using ex_countable_basis by auto
+  then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
+  define B2 where "B2 = B \<union> {UNIV}"
+  have "countable B2"
+    unfolding B2_def using B by auto
+  have "open U" if "U \<in> B2" for U
+    using that unfolding B2_def using B topological_basis_open by auto
+
+  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+  have i: "\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+    unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
+
+  have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+    apply (rule countable_product_event_const) using `countable B2` by auto
+  moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+    unfolding K_def by auto
+  ultimately have ii: "countable K" by auto
+
+  have iii: "topological_basis K"
+  proof (rule topological_basisI)
+    fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
+    then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+      unfolding open_fun_def by auto
+    with product_topology_open_contains_basis[OF this `x \<in> U`]
+    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"
+      unfolding topspace_euclidean open_openin by simp
+    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+                           "\<And>i. open (X i)"
+                           "finite {i. X i \<noteq> UNIV}"
+                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+      by auto
+    then have "x i \<in> X i" for i by auto
+    define I where "I = {i. X i \<noteq> UNIV}"
+    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)"
+    have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
+      unfolding B2_def using B `open (X i)` `x i \<in> X i` by (meson UnCI topological_basisE)
+    have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
+      using someI_ex[OF *]
+      apply (cases "i \<in> I")
+      unfolding Y_def using * apply (auto)
+      unfolding B2_def I_def by auto
+    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
+      unfolding Y_def by auto
+    then have ***: "finite {i. Y i \<noteq> UNIV}"
+      unfolding I_def using H(3) rev_finite_subset by blast
+    have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
+      using ** *** by auto
+    then have "Pi\<^sub>E UNIV Y \<in> K"
+      unfolding K_def by auto
+
+    have "Y i \<subseteq> X i" for i
+      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+
+    have "x \<in> Pi\<^sub>E UNIV Y"
+      using ** by auto
+
+    show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
+      using `Pi\<^sub>E UNIV Y \<in> K` `Pi\<^sub>E UNIV Y \<subseteq> U` `x \<in> Pi\<^sub>E UNIV Y` by auto
+  next
+    fix U assume "U \<in> K"
+    show "open U"
+      using `U \<in> K` unfolding open_fun_def K_def apply (auto)
+      apply (rule product_topology_basis)
+      using `\<And>V. V \<in> B2 \<Longrightarrow> open V` open_UNIV unfolding topspace_euclidean open_openin[symmetric]
+      by auto
+  qed
+
+  show ?thesis using i ii iii by auto
+qed
+
+instance "fun" :: (countable, second_countable_topology) second_countable_topology
+  apply standard
+  using product_topology_countable_basis topological_basis_imp_subbasis by auto
+
+
+subsection {*The strong operator topology on continuous linear operators*}
+
+text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
+operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
+
+However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
+$T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when 'b is the set
+of real numbers, since then this topology is compact.
+
+We can not implement it using type classes as there is already a topology, but at least we
+can define it as a topology.
+
+Note that there is yet another (common and useful) topology on operator spaces, the weak operator
+topology, defined analogously using the product topology, but where the target space is given the
+weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
+canonical embedding of a space into its bidual. We do not define it there, although it could also be
+defined analogously.
+*}
+
+definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
+where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
+
+lemma strong_operator_topology_topspace:
+  "topspace strong_operator_topology = UNIV"
+unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
+
+lemma strong_operator_topology_basis:
+  fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
+  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
+proof -
+  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
+    by (rule product_topology_basis'[OF assms])
+  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
+                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
+    by auto
+  ultimately show ?thesis
+    unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
+qed
+
+lemma strong_operator_topology_continuous_evaluation:
+  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+proof -
+  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
+    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+  then show ?thesis unfolding comp_def by simp
+qed
+
+lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+  "continuous_on_topo T strong_operator_topology f
+    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+proof (auto)
+  fix x::"'b"
+  assume "continuous_on_topo T strong_operator_topology f"
+  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
+  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+    by simp
+  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+    unfolding comp_def by auto
+next
+  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+  have "continuous_on_topo T euclidean (blinfun_apply o f)"
+    unfolding euclidean_product_topology
+    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+    using * unfolding comp_def by auto
+  show "continuous_on_topo T strong_operator_topology f"
+    unfolding strong_operator_topology_def
+    apply (rule continuous_on_topo_pullback')
+    by (auto simp add: `continuous_on_topo T euclidean (blinfun_apply o f)`)
+qed
+
+lemma strong_operator_topology_weaker_than_euclidean:
+  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+
+
+subsection {*Metrics on product spaces*}
+
+
+text {*In general, the product topology is not metrizable, unless the index set is countable.
+When the index set is countable, essentially any (convergent) combination of the metrics on the
+factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
+for instance.
+
+What is not completely trivial is that the distance thus defined induces the same topology
+as the product topology. This is what we have to prove to show that we have an instance
+of \verb+metric_space+.
+
+The proofs below would work verbatim for general countable products of metric spaces. However,
+since distances are only implemented in terms of type classes, we only develop the theory
+for countable products of the same space.*}
+
+instantiation "fun" :: (countable, metric_space) metric_space
+begin
+
+definition dist_fun_def:
+  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+
+definition uniformity_fun_def:
+  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
+
+text {*Except for the first one, the auxiliary lemmas below are only useful when proving the
+instance: once it is proved, they become trivial consequences of the general theory of metric
+spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
+to do this.*}
+
+lemma dist_fun_le_dist_first_terms:
+  "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+proof -
+  have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+          = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
+    by (rule suminf_cong, simp add: power_add)
+  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)"
+    apply (rule suminf_mult)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
+    apply (simp, rule suminf_le, simp)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... = (1/2)^(Suc N) * 2"
+    using suminf_geometric[of "1/2"] by auto
+  also have "... = (1/2)^N"
+    by auto
+  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"
+    by simp
+
+  define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
+  have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
+    unfolding M_def by (rule Max_ge, auto)
+  then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
+  have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
+    unfolding M_def apply (rule Max_ge) using that by auto
+  then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
+    using that by force
+  have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
+      (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
+    by (rule sum_mono, simp add: i)
+  also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
+    by (rule sum_distrib_left[symmetric])
+  also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
+    by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
+  also have "... = M * 2"
+    using suminf_geometric[of "1/2"] by auto
+  finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
+    by simp
+
+  have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    unfolding dist_fun_def by simp
+  also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+                  + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    apply (rule suminf_split_initial_segment)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... \<le> 2 * M + (1/2)^N"
+    using * ** by auto
+  finally show ?thesis unfolding M_def by simp
+qed
+
+lemma open_fun_contains_ball_aux:
+  assumes "open (U::(('a \<Rightarrow> 'b) set))"
+          "x \<in> U"
+  shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
+proof -
+  have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+    using open_fun_def assms by auto
+  obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
+                    "\<And>i. openin euclidean (X i)"
+                    "finite {i. X i \<noteq> topspace euclidean}"
+                    "x \<in> Pi\<^sub>E UNIV X"
+    using product_topology_open_contains_basis[OF * `x \<in> U`] by auto
+  define I where "I = {i. X i \<noteq> topspace euclidean}"
+  have "finite I" unfolding I_def using H(3) by auto
+  {
+    fix i
+    have "x i \<in> X i" using `x \<in> U` H by auto
+    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
+      using `openin euclidean (X i)` open_openin open_contains_ball by blast
+    then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
+    define f where "f = min e (1/2)"
+    have "f>0" "f<1" unfolding f_def using `e>0` by auto
+    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using `ball (x i) e \<subseteq> X i` by auto
+    ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
+  } note * = this
+  have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
+    by (rule choice, auto simp add: *)
+  then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
+    by blast
+  define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
+  have "m > 0" if "I\<noteq>{}"
+    unfolding m_def apply (rule Min_grI) using `finite I` `I \<noteq> {}` `\<And>i. e i > 0` by auto
+  moreover have "{y. dist x y < m} \<subseteq> U"
+  proof (auto)
+    fix y assume "dist x y < m"
+    have "y i \<in> X i" if "i \<in> I" for i
+    proof -
+      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+      define n where "n = to_nat i"
+      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
+        using `dist x y < m` unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
+      then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
+        using `n = to_nat i` by auto
+      also have "... \<le> (1/2)^(to_nat i) * e i"
+        unfolding m_def apply (rule Min_le) using `finite I` `i \<in> I` by auto
+      ultimately have "min (dist (x i) (y i)) 1 < e i"
+        by (auto simp add: divide_simps)
+      then have "dist (x i) (y i) < e i"
+        using `e i < 1` by auto
+      then show "y i \<in> X i" using `ball (x i) (e i) \<subseteq> X i` by auto
+    qed
+    then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+    then show "y \<in> U" using `Pi\<^sub>E UNIV X \<subseteq> U` by auto
+  qed
+  ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
+
+  have "U = UNIV" if "I = {}"
+    using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+  then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
+  then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
+qed
+
+lemma ball_fun_contains_open_aux:
+  fixes x::"('a \<Rightarrow> 'b)" and e::real
+  assumes "e>0"
+  shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
+proof -
+  have "\<exists>N::nat. 2^N > 8/e"
+    by (simp add: real_arch_pow)
+  then obtain N::nat where "2^N > 8/e" by auto
+  define f where "f = e/4"
+  have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
+  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)"
+  have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
+    unfolding X_def by auto
+  then have "finite {i. X i \<noteq> topspace euclidean}"
+    unfolding topspace_euclidean using finite_surj by blast
+  have "\<And>i. open (X i)"
+    unfolding X_def using metric_space_class.open_ball open_UNIV by auto
+  then have "\<And>i. openin euclidean (X i)"
+    using open_openin by auto
+  define U where "U = Pi\<^sub>E UNIV X"
+  have "open U"
+    unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
+    unfolding U_def using `\<And>i. openin euclidean (X i)` `finite {i. X i \<noteq> topspace euclidean}`
+    by auto
+  moreover have "x \<in> U"
+    unfolding U_def X_def by (auto simp add: PiE_iff)
+  moreover have "dist x y < e" if "y \<in> U" for y
+  proof -
+    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
+      using `y \<in> U` unfolding U_def apply (auto simp add: PiE_iff)
+      unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
+    have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
+      apply (rule Max.boundedI) using * by auto
+
+    have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+      by (rule dist_fun_le_dist_first_terms)
+    also have "... \<le> 2 * f + e / 8"
+      apply (rule add_mono) using ** `2^N > 8/e` by(auto simp add: algebra_simps divide_simps)
+    also have "... \<le> e/2 + e/8"
+      unfolding f_def by auto
+    also have "... < e"
+      by auto
+    finally show "dist x y < e" by simp
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma fun_open_ball_aux:
+  fixes U::"('a \<Rightarrow> 'b) set"
+  shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
+proof (auto)
+  assume "open U"
+  fix x assume "x \<in> U"
+  then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+    using open_fun_contains_ball_aux[OF `open U` `x \<in> U`] by auto
+next
+  assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+  define K where "K = {V. open V \<and> V \<subseteq> U}"
+  {
+    fix x assume "x \<in> U"
+    then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
+    then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
+      using ball_fun_contains_open_aux[OF `e>0`, of x] by auto
+    have "V \<in> K"
+      unfolding K_def using e(2) V(1) V(3) by auto
+    then have "x \<in> (\<Union>K)" using `x \<in> V` by auto
+  }
+  then have "(\<Union>K) = U"
+    unfolding K_def by auto
+  moreover have "open (\<Union>K)"
+    unfolding K_def by auto
+  ultimately show "open U" by simp
+qed
+
+instance proof
+  fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
+  proof
+    assume "x = y"
+    then show "dist x y = 0" unfolding dist_fun_def using `x = y` by auto
+  next
+    assume "dist x y = 0"
+    have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+    have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
+      using `dist x y = 0` unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
+    then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
+      by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
+                zero_eq_1_divide_iff zero_neq_numeral)
+    then have "x (from_nat n) = y (from_nat n)" for n
+      by auto
+    then have "x i = y i" for i
+      by (metis from_nat_to_nat)
+    then show "x = y"
+      by auto
+  qed
+next
+  text{*The proof of the triangular inequality is trivial, modulo the fact that we are dealing
+        with infinite series, hence we should justify the convergence at each step. In this
+        respect, the following simplification rule is extremely handy.*}
+  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"
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  fix x y z::"'a \<Rightarrow> 'b"
+  {
+    fix n
+    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
+            dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
+      by (simp add: dist_triangle2)
+    have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
+      using zero_le_dist by blast
+    moreover
+    {
+      assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
+      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"
+        by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
+    }
+    ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
+            min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
+      using * by linarith
+  } note ineq = this
+  have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    unfolding dist_fun_def by simp
+  also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
+                        + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+    apply (rule suminf_le)
+    using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
+      le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
+    by (auto simp add: summable_add)
+  also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
+                  + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+    by (rule suminf_add[symmetric], auto)
+  also have "... = dist x z + dist y z"
+    unfolding dist_fun_def by simp
+  finally show "dist x y \<le> dist x z + dist y z"
+    by simp
+next
+  text{*Finally, we show that the topology generated by the distance and the product
+        topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
+        except that the condition to prove is expressed with filters. To deal with this,
+        we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
+        \verb+Real_Vector_Spaces.thy+*}
+  fix U::"('a \<Rightarrow> 'b) set"
+  have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
+  unfolding uniformity_fun_def apply (subst eventually_INF_base)
+    by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
+  then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
+    unfolding fun_open_ball_aux by simp
+qed (simp add: uniformity_fun_def)
+
+end
+
+text {*Nice properties of spaces are preserved under countable products. In addition
+to first countability, second countability and metrizability, as we have seen above,
+completeness is also preserved, and therefore being Polish.*}
+
+instance "fun" :: (countable, complete_space) complete_space
+proof
+  fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
+  have "Cauchy (\<lambda>n. u n i)" for i
+  unfolding cauchy_def proof (intro impI allI)
+    fix e assume "e>(0::real)"
+    obtain k where "i = from_nat k"
+      using from_nat_to_nat[of i] by metis
+    have "(1/2)^k * min e 1 > 0" using `e>0` by auto
+    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"
+      using `Cauchy u` unfolding cauchy_def by blast
+    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"
+      by blast
+    have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+    proof (auto)
+      fix m n::nat assume "m \<ge> N" "n \<ge> N"
+      have "(1/2)^k * min (dist (u m i) (u n i)) 1
+              = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
+        using `i = from_nat k` by auto
+      also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
+        apply (rule sum_le_suminf)
+        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+      also have "... = dist (u m) (u n)"
+        unfolding dist_fun_def by auto
+      also have "... < (1/2)^k * min e 1"
+        using C `m \<ge> N` `n \<ge> N` by auto
+      finally have "min (dist (u m i) (u n i)) 1 < min e 1"
+        by (auto simp add: algebra_simps divide_simps)
+      then show "dist (u m i) (u n i) < e" by auto
+    qed
+    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+      by blast
+  qed
+  then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
+    using Cauchy_convergent convergent_def by auto
+  then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
+    using choice by force
+  then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
+  have "u \<longlonglongrightarrow> x"
+  proof (rule metric_LIMSEQ_I)
+    fix e assume [simp]: "e>(0::real)"
+    have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
+      by (rule metric_LIMSEQ_D, auto simp add: *)
+    have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
+      apply (rule choice) using i by auto
+    then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
+      by blast
+
+    have "\<exists>N::nat. 2^N > 4/e"
+      by (simp add: real_arch_pow)
+    then obtain N::nat where "2^N > 4/e" by auto
+    define L where "L = Max {K (from_nat n)|n. n \<le> N}"
+    have "dist (u k) x < e" if "k \<ge> L" for k
+    proof -
+      have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
+      proof -
+        have "K (from_nat n) \<le> L"
+          unfolding L_def apply (rule Max_ge) using `n \<le> N` by auto
+        then have "k \<ge> K (from_nat n)" using `k \<ge> L` by auto
+        then show ?thesis using K less_imp_le by auto
+      qed
+      have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
+        apply (rule Max.boundedI) using * by auto
+      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"
+        using dist_fun_le_dist_first_terms by auto
+      also have "... \<le> 2 * e/4 + e/4"
+        apply (rule add_mono)
+        using ** `2^N > 4/e` less_imp_le by (auto simp add: algebra_simps divide_simps)
+      also have "... < e" by auto
+      finally show ?thesis by simp
+    qed
+    then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
+  qed
+  then show "convergent u" using convergent_def by blast
+qed
+
+instance "fun" :: (countable, polish_space) polish_space
+by standard
+
+
+subsection {*Measurability*}
+
+text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
+generated by open sets in the product, and the product sigma algebra, countably generated by
+products of measurable sets along finitely many coordinates. The second one is defined and studied
+in \verb+Finite_Product_Measure.thy+.
+
+These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
+but there is a fundamental difference: open sets are generated by arbitrary unions, not only
+countable ones, so typically many open sets will not be measurable with respect to the product sigma
+algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
+only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
+the factor is countably generated).
+
+In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
+compare it with the product sigma algebra as explained above.
+*}
+
+lemma measurable_product_coordinates [measurable (raw)]:
+  "(\<lambda>x. x i) \<in> measurable borel borel"
+by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+
+lemma measurable_product_then_coordinatewise:
+  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
+  assumes [measurable]: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
+    unfolding comp_def by auto
+  then show ?thesis by simp
+qed
+
+text {*To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+of the product sigma algebra that is more similar to the one we used above for the product
+topology.*}
+
+lemma sets_PiM_finite:
+  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+proof
+  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
+  proof (auto)
+    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
+    then have *: "X i \<in> sets (M i)" for i by simp
+    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
+    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
+    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
+    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
+      unfolding Y_def apply (rule sets_PiM_I) using `finite J` `J \<subseteq> I` * by auto
+    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
+      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
+      by (auto simp add: PiE_iff, blast)
+    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
+  qed
+  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
+              \<subseteq> sets (Pi\<^sub>M I M)"
+    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
+
+  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
+                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
+    if "i \<in> I" "A \<in> sets (M i)" for i A
+  proof -
+    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
+    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
+      unfolding X_def using sets.sets_into_space[OF `A \<in> sets (M i)`] `i \<in> I`
+      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
+    moreover have "X j \<in> sets (M j)" for j
+      unfolding X_def using `A \<in> sets (M i)` by auto
+    moreover have "finite {j. X j \<noteq> space (M j)}"
+      unfolding X_def by simp
+    ultimately show ?thesis by auto
+  qed
+  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+    unfolding sets_PiM_single
+    apply (rule sigma_sets_mono')
+    apply (auto simp add: PiE_iff *)
+    done
+qed
+
+lemma sets_PiM_subset_borel:
+  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
+proof -
+  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
+  proof -
+    define I where "I = {i. X i \<noteq> UNIV}"
+    have "finite I" unfolding I_def using that by simp
+    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
+      unfolding I_def by auto
+    also have "... \<in> sets borel"
+      using that `finite I` by measurable
+    finally show ?thesis by simp
+  qed
+  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
+    by auto
+  then show ?thesis unfolding sets_PiM_finite space_borel
+    by (simp add: * sets.sigma_sets_subset')
+qed
+
+lemma sets_PiM_equal_borel:
+  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
+proof
+  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
+            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+    using product_topology_countable_basis by fast
+  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
+  proof -
+    obtain X where H: "k = PiE UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+      using K(3)[OF `k \<in> K`] by blast
+    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
+  qed
+  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
+  proof -
+    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
+      using `open U` `topological_basis K` by (metis topological_basis_def)
+    have "countable B" using `B \<subseteq> K` `countable K` countable_subset by blast
+    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
+      using `B \<subseteq> K` * that by auto
+    ultimately show ?thesis unfolding `U = (\<Union>B)` by auto
+  qed
+  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
+    apply (rule sets.sigma_sets_subset') using ** by auto
+  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+    unfolding borel_def by auto
+qed (simp add: sets_PiM_subset_borel)
+
+lemma measurable_coordinatewise_then_product:
+  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
+  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
+  shows "f \<in> borel_measurable M"
+proof -
+  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+    by (rule measurable_PiM_single', auto simp add: assms)
+  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
+qed
+
+end