src/HOL/Analysis/Function_Topology.thy

{* verbatim *} is explicit legacy feature;

(*  Author:  Sébastien Gouëzel   [e-mail] with additions from LCP
    License: BSD
*)

theory Function_Topology
imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
begin


section%important \<open>Product topology\<close>

text \<open>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 "Pi\<^sub>E 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+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+.
\<close>

subsection%important \<open>Topology without type classes\<close>

subsubsection%important \<open>The topology generated by some (open) subsets\<close>

text \<open>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.)\<close>

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%unimportant istopology_generate_topology_on:
  "istopology (generate_topology_on S)"
unfolding istopology_def by (auto intro: generate_topology_on.intros)

text \<open>The basic property of the topology generated by a set $S$ is that it is the
smallest topology containing all the elements of $S$:\<close>

lemma%unimportant 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

abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"

lemma%unimportant 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]] by simp

lemma%unimportant 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%important topology_generated_by_topspace:
  "topspace (topology_generated_by S) = (\<Union>S)"
proof%unimportant
  {
    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%important topology_generated_by_Basis:
  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)

lemma generate_topology_on_Inter:
  "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
  by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)

subsection\<open>Topology bases and sub-bases\<close>

lemma istopology_base_alt:
   "istopology (arbitrary union_of P) \<longleftrightarrow>
    (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
           \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)

lemma istopology_base_eq:
   "istopology (arbitrary union_of P) \<longleftrightarrow>
    (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)

lemma istopology_base:
   "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
  by (simp add: arbitrary_def istopology_base_eq union_of_inc)

lemma openin_topology_base_unique:
   "openin X = arbitrary union_of P \<longleftrightarrow>
        (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: union_of_def arbitrary_def)
next
  assume R: ?rhs
  then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
    using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
  from R show ?lhs
    by (fastforce simp add: union_of_def arbitrary_def intro: *)
qed

lemma topology_base_unique:
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
     \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
    \<Longrightarrow> topology(arbitrary union_of P) = X"
  by (metis openin_topology_base_unique openin_inverse [of X])

lemma topology_bases_eq_aux:
   "\<lbrakk>(arbitrary union_of P) S;
     \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
        \<Longrightarrow> (arbitrary union_of Q) S"
  by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)

lemma topology_bases_eq:
   "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
    \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
        \<Longrightarrow> topology (arbitrary union_of P) =
            topology (arbitrary union_of Q)"
  by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)

lemma istopology_subbase:
   "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
  by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)

lemma openin_subbase:
  "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
   \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
  by (simp add: istopology_subbase topology_inverse')

lemma topspace_subbase [simp]:
   "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
proof
  show "?lhs \<subseteq> U"
    by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
  show "U \<subseteq> ?lhs"
    by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
              openin_subset relative_to_inc subset_UNIV topology_inverse')
qed

lemma minimal_topology_subbase:
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
     openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
    \<Longrightarrow> openin X S"
  apply (simp add: istopology_subbase topology_inverse)
  apply (simp add: union_of_def intersection_of_def relative_to_def)
  apply (blast intro: openin_Int_Inter)
  done

lemma istopology_subbase_UNIV:
   "istopology (arbitrary union_of (finite intersection_of P))"
  by (simp add: istopology_base finite_intersection_of_Int)


lemma generate_topology_on_eq:
  "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
proof (intro ext iffI)
  fix A
  assume "?lhs A"
  then show "?rhs A"
  proof induction
    case (Int a b)
    then show ?case
      by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
  next
    case (UN K)
    then show ?case
      by (simp add: arbitrary_union_of_Union)
  next
    case (Basis s)
    then show ?case
      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
  qed auto
next
  fix A
  assume "?rhs A"
  then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"
    unfolding union_of_def intersection_of_def by auto
  show "?lhs A"
    unfolding eq
  proof (rule generate_topology_on.UN)
    fix T
    assume "T \<in> \<U>"
    with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
      by blast
    have "generate_topology_on S (\<Inter>\<F>)"
    proof (rule generate_topology_on_Inter)
      show "finite \<F>" "\<F> \<noteq> {}"
        by (auto simp: \<open>finite' \<F>\<close>)
      show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
        by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
    qed
    then show "generate_topology_on S T"
      using \<open>\<Inter>\<F> = T\<close> by blast
  qed
qed

subsubsection%important \<open>Continuity\<close>

text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
of type classes, as defined below.\<close>

definition%important 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%important continuous_on_continuous_on_topo:
  "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
topspace_euclidean_subtopology open_openin topspace_euclidean by fast

lemma%unimportant 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%important continuous_on_topo_open [intro]:
  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
unfolding%unimportant continuous_on_topo_def by auto

lemma%unimportant 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%important 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%unimportant (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%important 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%unimportant assms continuous_on_generated_topo_iff by blast

lemma%important 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%unimportant assms unfolding continuous_on_topo_def
proof%unimportant (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%unimportant 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%important \<open>Pullback topology\<close>

text \<open>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.\<close>

text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
the set $A$.\<close>

definition%important 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%important istopology_pullback_topology:
  "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
unfolding%unimportant 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%unimportant 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%unimportant topspace_pullback_topology:
  "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
by (auto simp add: topspace_def openin_pullback_topology)

lemma%important 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%unimportant (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 \<open>openin T1 (g-`U \<inter> topspace T1)\<close> 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%important 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%unimportant (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) \<open>openin T2 V\<close> 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) \<open>x \<in> topspace T1\<close> 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) \<open>x \<in> topspace T1\<close> by blast
  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
    unfolding topspace_pullback_topology by blast
qed


subsection%important \<open>The product topology\<close>

text \<open>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.
\<close>

definition%important 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 \<open>The total set of the product topology is the product of the total sets
along each coordinate.\<close>

proposition product_topology:
  "product_topology X I =
   topology
    (arbitrary union_of
       ((finite intersection_of
        (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
        relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
  (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
proof -
  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)})"
  have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
  proof -
    have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
      if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
    proof -
      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)}"
        using \<U> by auto
      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)}"
        by metis
      obtain U where "U \<in> \<U>"
        using \<open>\<U> \<noteq> {}\<close> by blast
      let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
      show ?thesis
      proof (intro conjI exI)
        show "finite (\<Union>U\<in>\<U>. ?F U)"
          using Y \<open>finite' \<U>\<close> by auto
        show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
        proof
          have *: "f \<in> U"
            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"
              and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
          proof -
            have "Pi\<^sub>E I (Y U) = U"
              using Y \<open>U \<in> \<U>\<close> by blast
            then show "f \<in> U"
              using that unfolding PiE_def Pi_def by blast
          qed
          show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
            by (auto simp: PiE_iff *)
          show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
            using Y openin_subset \<open>finite' \<U>\<close> by fastforce
        qed
      qed (use Y openin_subset in \<open>blast+\<close>)
    qed
    have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
      if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
    proof (cases "\<U>={}")
      case True
      then show ?thesis
        apply (rule_tac x="{?TOP}" in exI, simp)
        apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
        apply force
        done
    next
      case False
      then obtain U where "U \<in> \<U>"
        by blast
      have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
        using \<U> by auto
      then obtain J Y where
        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)"
        by metis
      let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
      show ?thesis
      proof (intro conjI exI)
        show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
          using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
        have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
          using Y by force
        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)}}"
          apply clarsimp
          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
          apply (auto simp: *)
          done
      next
        show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
        proof
          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))"
            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
          then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
            using \<open>U \<in> \<U>\<close>
            by fastforce
          moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
            using PiE_mem Y by fastforce
          ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
            by auto
        qed (use Y in fastforce)
      qed
    qed
    show ?thesis
      unfolding relative_to_def intersection_of_def
      by (safe; blast dest!: 1 2)
  qed
  show ?thesis
    unfolding product_topology_def generate_topology_on_eq
    apply (rule arg_cong [where f = topology])
    apply (rule arg_cong [where f = "(union_of)arbitrary"])
    apply (force simp: *)
    done
qed

lemma%important topspace_product_topology:
  "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
proof%unimportant
  show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
    unfolding product_topology_def 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%unimportant 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
  by (rule topology_generated_by_Basis) (use assms in auto)

lemma%important 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%unimportant -
  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 \<open>k \<in> K\<close> by auto
    then show ?case
      by auto
  qed auto
  then show ?thesis using \<open>x \<in> U\<close> by auto
qed


lemma openin_product_topology:
   "openin (product_topology X I) =
    arbitrary union_of
          ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
           relative_to topspace (product_topology X I))"
  apply (subst product_topology)
  apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
  done

lemma subtopology_PiE:
  "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
proof -
  let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
  let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
        finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
    by (rule finite_intersection_of_relative_to)
  also have "\<dots> = finite intersection_of
                      ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
                       relative_to ?X \<inter> Pi\<^sub>E I S)
                   relative_to ?X \<inter> Pi\<^sub>E I S"
    apply (rule arg_cong2 [where f = "(relative_to)"])
     apply (rule arg_cong [where f = "(intersection_of)finite"])
     apply (rule ext)
     apply (auto simp: relative_to_def intersection_of_def)
    done
  finally
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
        finite intersection_of
          (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
          relative_to ?X \<inter> Pi\<^sub>E I S"
    by (metis finite_intersection_of_relative_to)
  then show ?thesis
  unfolding topology_eq
  apply clarify
  apply (simp add: openin_product_topology flip: openin_relative_to)
  apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
  done
qed


lemma product_topology_base_alt:
   "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
    relative_to topspace(product_topology X I) =
    (\<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))))"
   (is "?lhs = ?rhs")
proof -
  have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
    unfolding all_relative_to all_intersection_of topspace_product_topology
  proof clarify
    fix \<F>
    assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
    then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<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))"
    proof (induction)
      case (insert F \<F>)
      then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
        and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
        and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
        by auto
      obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
        using insert by auto
      let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
      show ?case
      proof (intro exI conjI)
        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
        using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
      next
        show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
          by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
      next
        show "\<forall>i\<in>I. openin (X i) (?U i)"
          by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
      qed
    qed (auto intro: dest: not_finite_existsD)
  qed
  moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
  proof clarify
    fix U :: "'a \<Rightarrow> 'b set"
    assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
    let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
    show "?lhs (Pi\<^sub>E I U)"
      unfolding relative_to_def topspace_product_topology
    proof (intro exI conjI)
      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"
        using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
      show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
        using ope openin_subset by fastforce
    qed
  qed
  ultimately show ?thesis
    by meson
qed


lemma topspace_product_topology_alt:
   "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
  by (force simp: product_topology PiE_def)

lemma openin_product_topology_alt:
  "openin (product_topology X I) S \<longleftrightarrow>
    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
                 (\<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)"
  apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
  apply (drule bspec; blast)
  done


text \<open>The basic property of the product topology is the continuity of projections:\<close>

lemma%unimportant 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 \<open>openin (T i) U\<close>]
      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 \<open>openin (T i) U\<close> 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 topspace_product_topology PiE_iff)
qed

lemma%important 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%unimportant (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 * \<open>J \<subseteq> I\<close> by auto
  also have "openin T1 (...)"
    apply (rule openin_INT)
    apply (simp add: \<open>finite J\<close>)
    using H(2) assms(1) \<open>J \<subseteq> I\<close> 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: topspace_product_topology)
    apply (auto simp add: PiE_iff)
    using assms unfolding continuous_on_topo_def by auto
qed

lemma%unimportant 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 \<open>i \<in> I\<close> 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 \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
  then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
    using topspace_product_topology by metis
  then show "f x i = undefined"
    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed

lemma%unimportant 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 \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> 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%important \<open>Powers of a single topological space as a topological space, using type classes\<close>

instantiation "fun" :: (type, topological_space) topological_space
begin

definition%important open_fun_def:
  "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"

instance proof%unimportant
  have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
    unfolding topspace_product_topology 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%unimportant euclidean_product_topology:
  "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
by (metis open_openin topology_eq open_fun_def)

lemma%important 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%unimportant -
  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 \<open>The results proved in the general situation of products of possibly different
spaces have their counterparts in this simpler setting.\<close>

lemma%unimportant 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%unimportant 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%unimportant 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%unimportant 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%important \<open>Topological countability for product spaces\<close>

text \<open>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.\<close>

lemma%unimportant 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 \<open>a \<in> F\<close> 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 \<open>a \<in> F\<close> 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%unimportant 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 \<open>b \<in> G\<close> \<open>countable G\<close>]
    by (meson countable_image countable_subset)
qed

instance "fun" :: (countable, first_countable_topology) first_countable_topology
proof%unimportant
  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 \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
  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 \<open>\<And>i. countable (B i)\<close> 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>open U \<and> x \<in> U\<close> 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 \<open>Pi\<^sub>E UNIV Y \<in> K\<close> 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 \<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
qed

lemma%important 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 = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
proof%unimportant -
  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 = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> 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 \<open>countable B2\<close> 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 \<open>x \<in> U\<close>]
    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>open (X i)\<close> \<open>x i \<in> X i\<close> 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 \<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
  next
    fix U assume "U \<in> K"
    show "open U"
      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
      apply (rule product_topology_basis)
      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> 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%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)

text \<open>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.
\<close>

definition%important 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%unimportant strong_operator_topology_topspace:
  "topspace strong_operator_topology = UNIV"
unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto

lemma%important 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%unimportant -
  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%important strong_operator_topology_continuous_evaluation:
  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
proof%unimportant -
  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%unimportant 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: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
qed

lemma%important strong_operator_topology_weaker_than_euclidean:
  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)


subsection%important \<open>Metrics on product spaces\<close>


text \<open>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.\<close>

instantiation "fun" :: (countable, metric_space) metric_space
begin

definition%important dist_fun_def:
  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"

definition%important uniformity_fun_def:
  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"

text \<open>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.\<close>

lemma%important 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%unimportant -
  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%unimportant 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 * \<open>x \<in> U\<close>] 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 \<open>x \<in> U\<close> H by auto
    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
      using \<open>openin euclidean (X i)\<close> 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 \<open>e>0\<close> by auto
    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> 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 Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> 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 \<open>dist x y < m\<close> 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 \<open>n = to_nat i\<close> by auto
      also have "... \<le> (1/2)^(to_nat i) * e i"
        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> 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 \<open>e i < 1\<close> by auto
      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> 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 \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> 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%unimportant 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 \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
    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 \<open>y \<in> U\<close> 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 ** \<open>2^N > 8/e\<close> 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%unimportant 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>open U\<close> \<open>x \<in> U\<close>] 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 \<open>e>0\<close>, 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 \<open>x \<in> V\<close> 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 \<open>x = y\<close> 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 \<open>dist x y = 0\<close> 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\<open>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.\<close>
  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\<open>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+\<close>
  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 \<open>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.\<close>

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 \<open>e>0\<close> 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 \<open>Cauchy u\<close> 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 \<open>i = from_nat k\<close> 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 \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> 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 \<open>n \<le> N\<close> by auto
        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> 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 ** \<open>2^N > 4/e\<close> 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%important \<open>Measurability\<close> (*FIX ME mv *)

text \<open>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.
\<close>

lemma%unimportant 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%unimportant 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 \<open>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.\<close>

lemma%important 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%unimportant
  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 \<open>finite J\<close> \<open>J \<subseteq> I\<close> * 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 \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
      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 \<open>A \<in> sets (M i)\<close> 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%important sets_PiM_subset_borel:
  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
proof%unimportant -
  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 \<open>finite I\<close> 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%important sets_PiM_equal_borel:
  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
proof%unimportant
  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E 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 = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
      using K(3)[OF \<open>k \<in> K\<close>] 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>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
      using \<open>B \<subseteq> K\<close> * that by auto
    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> 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%important 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%unimportant -
  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