src/HOL/Analysis/Function_Topology.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69517 dc20f278e8f3
child 69566 c41954ee87cf
permissions -rw-r--r--
capitalize proper names in lemma names
     1 (*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP
     2     License: BSD
     3 *)
     4 
     5 theory Function_Topology
     6 imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
     7 begin
     8 
     9 
    10 section%important \<open>Product Topology\<close>
    11 
    12 text \<open>We want to define the product topology.
    13 
    14 The product topology on a product of topological spaces is generated by
    15 the sets which are products of open sets along finitely many coordinates, and the whole
    16 space along the other coordinates. This is the coarsest topology for which the projection
    17 to each factor is continuous.
    18 
    19 To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
    20 'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
    21 coordinate belongs to $X\;i$ for all $i \in I$.
    22 
    23 Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
    24 This means that type classes can not be used to define such a product if one wants to take the
    25 product of different topological spaces (as the type 'a can only be given one structure of
    26 topological space using type classes). On the other hand, one can define different topologies (as
    27 introduced in \verb+thy+) on one type, and these topologies do not need to
    28 share the same maximal open set. Hence, one can form a product of topologies in this sense, and
    29 this works well. The big caveat is that it does not interact well with the main body of
    30 topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
    31 is not defined in this setting.
    32 
    33 As the product of different topological spaces is very important in several areas of
    34 mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
    35 and reformulate afterwards the consequences in terms of type classes (which are of course very
    36 handy for applications).
    37 
    38 Given this limitation, it looks to me that it would be very beneficial to revamp the theory
    39 of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
    40 type classes as consequences of more general statements in terms of topologies (but I am
    41 probably too naive here).
    42 
    43 Here is an example of a reformulation using topologies. Let
    44 \begin{verbatim}
    45 continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
    46                                       \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
    47 \end{verbatim}
    48 be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
    49 the current \verb+continuous_on+ (with type classes) can be redefined as
    50 \begin{verbatim}
    51 continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
    52 \end{verbatim}
    53 
    54 In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
    55 for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
    56 the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
    57 
    58 I only develop the basics of the product topology in this theory. The most important missing piece
    59 is Tychonov theorem, stating that a product of compact spaces is always compact for the product
    60 topology, even when the product is not finite (or even countable).
    61 
    62 I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
    63 \<close>
    64 
    65 subsection%important \<open>Topology without type classes\<close>
    66 
    67 subsubsection%important \<open>The topology generated by some (open) subsets\<close>
    68 
    69 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
    70 as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
    71 and is never a problem in proofs, so I prefer to write it down explicitly.
    72 
    73 We do not require UNIV to be an open set, as this will not be the case in applications. (We are
    74 thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
    75 
    76 inductive generate_topology_on for S where
    77 Empty: "generate_topology_on S {}"
    78 |Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
    79 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
    80 | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
    81 
    82 lemma%unimportant istopology_generate_topology_on:
    83   "istopology (generate_topology_on S)"
    84 unfolding istopology_def by (auto intro: generate_topology_on.intros)
    85 
    86 text \<open>The basic property of the topology generated by a set $S$ is that it is the
    87 smallest topology containing all the elements of $S$:\<close>
    88 
    89 lemma%unimportant generate_topology_on_coarsest:
    90   assumes "istopology T"
    91           "\<And>s. s \<in> S \<Longrightarrow> T s"
    92           "generate_topology_on S s0"
    93   shows "T s0"
    94 using assms(3) apply (induct rule: generate_topology_on.induct)
    95 using assms(1) assms(2) unfolding istopology_def by auto
    96 
    97 abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
    98   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
    99 
   100 lemma%unimportant openin_topology_generated_by_iff:
   101   "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
   102   using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
   103 
   104 lemma%unimportant openin_topology_generated_by:
   105   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
   106 using openin_topology_generated_by_iff by auto
   107 
   108 lemma%important topology_generated_by_topspace:
   109   "topspace (topology_generated_by S) = (\<Union>S)"
   110 proof%unimportant
   111   {
   112     fix s assume "openin (topology_generated_by S) s"
   113     then have "generate_topology_on S s" by (rule openin_topology_generated_by)
   114     then have "s \<subseteq> (\<Union>S)" by (induct, auto)
   115   }
   116   then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
   117     unfolding topspace_def by auto
   118 next
   119   have "generate_topology_on S (\<Union>S)"
   120     using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
   121   then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
   122     unfolding topspace_def using openin_topology_generated_by_iff by auto
   123 qed
   124 
   125 lemma%important topology_generated_by_Basis:
   126   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
   127 by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
   128 
   129 lemma generate_topology_on_Inter:
   130   "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
   131   by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
   132 
   133 subsection\<open>Topology bases and sub-bases\<close>
   134 
   135 lemma istopology_base_alt:
   136    "istopology (arbitrary union_of P) \<longleftrightarrow>
   137     (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
   138            \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
   139   by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
   140 
   141 lemma istopology_base_eq:
   142    "istopology (arbitrary union_of P) \<longleftrightarrow>
   143     (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
   144   by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
   145 
   146 lemma istopology_base:
   147    "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
   148   by (simp add: arbitrary_def istopology_base_eq union_of_inc)
   149 
   150 lemma openin_topology_base_unique:
   151    "openin X = arbitrary union_of P \<longleftrightarrow>
   152         (\<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))"
   153    (is "?lhs = ?rhs")
   154 proof
   155   assume ?lhs
   156   then show ?rhs
   157     by (auto simp: union_of_def arbitrary_def)
   158 next
   159   assume R: ?rhs
   160   then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
   161     using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
   162   from R show ?lhs
   163     by (fastforce simp add: union_of_def arbitrary_def intro: *)
   164 qed
   165 
   166 lemma topology_base_unique:
   167    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
   168      \<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>
   169     \<Longrightarrow> topology(arbitrary union_of P) = X"
   170   by (metis openin_topology_base_unique openin_inverse [of X])
   171 
   172 lemma topology_bases_eq_aux:
   173    "\<lbrakk>(arbitrary union_of P) S;
   174      \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
   175         \<Longrightarrow> (arbitrary union_of Q) S"
   176   by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
   177 
   178 lemma topology_bases_eq:
   179    "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
   180     \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
   181         \<Longrightarrow> topology (arbitrary union_of P) =
   182             topology (arbitrary union_of Q)"
   183   by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)
   184 
   185 lemma istopology_subbase:
   186    "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
   187   by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
   188 
   189 lemma openin_subbase:
   190   "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
   191    \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
   192   by (simp add: istopology_subbase topology_inverse')
   193 
   194 lemma topspace_subbase [simp]:
   195    "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
   196 proof
   197   show "?lhs \<subseteq> U"
   198     by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
   199   show "U \<subseteq> ?lhs"
   200     by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
   201               openin_subset relative_to_inc subset_UNIV topology_inverse')
   202 qed
   203 
   204 lemma minimal_topology_subbase:
   205    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
   206      openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
   207     \<Longrightarrow> openin X S"
   208   apply (simp add: istopology_subbase topology_inverse)
   209   apply (simp add: union_of_def intersection_of_def relative_to_def)
   210   apply (blast intro: openin_Int_Inter)
   211   done
   212 
   213 lemma istopology_subbase_UNIV:
   214    "istopology (arbitrary union_of (finite intersection_of P))"
   215   by (simp add: istopology_base finite_intersection_of_Int)
   216 
   217 
   218 lemma generate_topology_on_eq:
   219   "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
   220 proof (intro ext iffI)
   221   fix A
   222   assume "?lhs A"
   223   then show "?rhs A"
   224   proof induction
   225     case (Int a b)
   226     then show ?case
   227       by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
   228   next
   229     case (UN K)
   230     then show ?case
   231       by (simp add: arbitrary_union_of_Union)
   232   next
   233     case (Basis s)
   234     then show ?case
   235       by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
   236   qed auto
   237 next
   238   fix A
   239   assume "?rhs A"
   240   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>"
   241     unfolding union_of_def intersection_of_def by auto
   242   show "?lhs A"
   243     unfolding eq
   244   proof (rule generate_topology_on.UN)
   245     fix T
   246     assume "T \<in> \<U>"
   247     with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
   248       by blast
   249     have "generate_topology_on S (\<Inter>\<F>)"
   250     proof (rule generate_topology_on_Inter)
   251       show "finite \<F>" "\<F> \<noteq> {}"
   252         by (auto simp: \<open>finite' \<F>\<close>)
   253       show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
   254         by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
   255     qed
   256     then show "generate_topology_on S T"
   257       using \<open>\<Inter>\<F> = T\<close> by blast
   258   qed
   259 qed
   260 
   261 subsubsection%important \<open>Continuity\<close>
   262 
   263 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
   264 of type classes, as defined below.\<close>
   265 
   266 definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   267   where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
   268                                       \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
   269 
   270 lemma%important continuous_on_continuous_on_topo:
   271   "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
   272 unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
   273 topspace_euclidean_subtopology open_openin topspace_euclidean by fast
   274 
   275 lemma%unimportant continuous_on_topo_UNIV:
   276   "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
   277 using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
   278 
   279 lemma%important continuous_on_topo_open [intro]:
   280   "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
   281 unfolding%unimportant continuous_on_topo_def by auto
   282 
   283 lemma%unimportant continuous_on_topo_topspace [intro]:
   284   "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
   285 unfolding continuous_on_topo_def by auto
   286 
   287 lemma%important continuous_on_generated_topo_iff:
   288   "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
   289       ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
   290 unfolding continuous_on_topo_def topology_generated_by_topspace
   291 proof%unimportant (auto simp add: topology_generated_by_Basis)
   292   assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
   293   fix U assume "openin (topology_generated_by S) U"
   294   then have "generate_topology_on S U" by (rule openin_topology_generated_by)
   295   then show "openin T1 (f -` U \<inter> topspace T1)"
   296   proof (induct)
   297     fix a b
   298     assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
   299     have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
   300       by auto
   301     then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
   302   next
   303     fix K
   304     assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
   305     define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
   306     have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
   307     have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
   308     moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
   309     ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
   310   qed (auto simp add: H)
   311 qed
   312 
   313 lemma%important continuous_on_generated_topo:
   314   assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
   315           "f`(topspace T1) \<subseteq> (\<Union> S)"
   316   shows "continuous_on_topo T1 (topology_generated_by S) f"
   317 using%unimportant assms continuous_on_generated_topo_iff by blast
   318 
   319 lemma%important continuous_on_topo_compose:
   320   assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
   321   shows "continuous_on_topo T1 T3 (g o f)"
   322 using%unimportant assms unfolding continuous_on_topo_def
   323 proof%unimportant (auto)
   324   fix U :: "'c set"
   325   assume H: "openin T3 U"
   326   have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
   327     using H assms by blast
   328   moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
   329     using H assms continuous_on_topo_topspace by fastforce
   330   ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
   331     by simp
   332 qed (blast)
   333 
   334 lemma%unimportant continuous_on_topo_preimage_topspace [intro]:
   335   assumes "continuous_on_topo T1 T2 f"
   336   shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
   337 using assms unfolding continuous_on_topo_def by auto
   338 
   339 
   340 subsubsection%important \<open>Pullback topology\<close>
   341 
   342 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
   343 a special case of this notion, pulling back by the identity. We introduce the general notion as
   344 we will need it to define the strong operator topology on the space of continuous linear operators,
   345 by pulling back the product topology on the space of all functions.\<close>
   346 
   347 text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
   348 the set $A$.\<close>
   349 
   350 definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
   351   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
   352 
   353 lemma%important istopology_pullback_topology:
   354   "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
   355 unfolding%unimportant istopology_def proof (auto)
   356   fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
   357   then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
   358     by (rule bchoice)
   359   then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
   360     by blast
   361   define V where "V = (\<Union>S\<in>K. U S)"
   362   have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
   363   then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
   364 qed
   365 
   366 lemma%unimportant openin_pullback_topology:
   367   "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
   368 unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
   369 
   370 lemma%unimportant topspace_pullback_topology:
   371   "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
   372 by (auto simp add: topspace_def openin_pullback_topology)
   373 
   374 lemma%important continuous_on_topo_pullback [intro]:
   375   assumes "continuous_on_topo T1 T2 g"
   376   shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
   377 unfolding continuous_on_topo_def
   378 proof%unimportant (auto)
   379   fix U::"'b set" assume "openin T2 U"
   380   then have "openin T1 (g-`U \<inter> topspace T1)"
   381     using assms unfolding continuous_on_topo_def by auto
   382   have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
   383     unfolding topspace_pullback_topology by auto
   384   also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
   385     by auto
   386   also have "openin (pullback_topology A f T1) (...)"
   387     unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
   388   finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
   389     by auto
   390 next
   391   fix x assume "x \<in> topspace (pullback_topology A f T1)"
   392   then have "f x \<in> topspace T1"
   393     unfolding topspace_pullback_topology by auto
   394   then show "g (f x) \<in> topspace T2"
   395     using assms unfolding continuous_on_topo_def by auto
   396 qed
   397 
   398 lemma%important continuous_on_topo_pullback' [intro]:
   399   assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
   400   shows "continuous_on_topo T1 (pullback_topology A f T2) g"
   401 unfolding continuous_on_topo_def
   402 proof%unimportant (auto)
   403   fix U assume "openin (pullback_topology A f T2) U"
   404   then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
   405     unfolding openin_pullback_topology by auto
   406   then obtain V where "openin T2 V" "U = f-`V \<inter> A"
   407     by blast
   408   then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
   409     by blast
   410   also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
   411     by auto
   412   also have "... = (f o g)-`V \<inter> topspace T1"
   413     using assms(2) by auto
   414   also have "openin T1 (...)"
   415     using assms(1) \<open>openin T2 V\<close> by auto
   416   finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
   417 next
   418   fix x assume "x \<in> topspace T1"
   419   have "(f o g) x \<in> topspace T2"
   420     using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   421   then have "g x \<in> f-`(topspace T2)"
   422     unfolding comp_def by blast
   423   moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
   424   ultimately show "g x \<in> topspace (pullback_topology A f T2)"
   425     unfolding topspace_pullback_topology by blast
   426 qed
   427 
   428 
   429 subsection%important \<open>The product topology\<close>
   430 
   431 text \<open>We can now define the product topology, as generated by
   432 the sets which are products of open sets along finitely many coordinates, and the whole
   433 space along the other coordinates. Equivalently, it is generated by sets which are one open
   434 set along one single coordinate, and the whole space along other coordinates. In fact, this is only
   435 equivalent for nonempty products, but for the empty product the first formulation is better
   436 (the second one gives an empty product space, while an empty product should have exactly one
   437 point, equal to \verb+undefined+ along all coordinates.
   438 
   439 So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
   440 \<close>
   441 
   442 definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
   443   where "product_topology T I =
   444     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)}}"
   445 
   446 text \<open>The total set of the product topology is the product of the total sets
   447 along each coordinate.\<close>
   448 
   449 proposition product_topology:
   450   "product_topology X I =
   451    topology
   452     (arbitrary union_of
   453        ((finite intersection_of
   454         (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
   455         relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
   456   (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
   457 proof -
   458   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)})"
   459   have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
   460   proof -
   461     have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
   462       if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
   463     proof -
   464       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)}"
   465         using \<U> by auto
   466       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)}"
   467         by metis
   468       obtain U where "U \<in> \<U>"
   469         using \<open>\<U> \<noteq> {}\<close> by blast
   470       let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
   471       show ?thesis
   472       proof (intro conjI exI)
   473         show "finite (\<Union>U\<in>\<U>. ?F U)"
   474           using Y \<open>finite' \<U>\<close> by auto
   475         show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
   476         proof
   477           have *: "f \<in> U"
   478             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"
   479               and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
   480           proof -
   481             have "Pi\<^sub>E I (Y U) = U"
   482               using Y \<open>U \<in> \<U>\<close> by blast
   483             then show "f \<in> U"
   484               using that unfolding PiE_def Pi_def by blast
   485           qed
   486           show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
   487             by (auto simp: PiE_iff *)
   488           show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
   489             using Y openin_subset \<open>finite' \<U>\<close> by fastforce
   490         qed
   491       qed (use Y openin_subset in \<open>blast+\<close>)
   492     qed
   493     have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
   494       if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
   495     proof (cases "\<U>={}")
   496       case True
   497       then show ?thesis
   498         apply (rule_tac x="{?TOP}" in exI, simp)
   499         apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
   500         apply force
   501         done
   502     next
   503       case False
   504       then obtain U where "U \<in> \<U>"
   505         by blast
   506       have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
   507         using \<U> by auto
   508       then obtain J Y where
   509         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)"
   510         by metis
   511       let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
   512       show ?thesis
   513       proof (intro conjI exI)
   514         show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
   515           using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
   516         have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
   517           using Y by force
   518         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)}}"
   519           apply clarsimp
   520           apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
   521           apply (auto simp: *)
   522           done
   523       next
   524         show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
   525         proof
   526           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))"
   527             apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
   528             using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
   529           then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
   530             using \<open>U \<in> \<U>\<close>
   531             by fastforce
   532           moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
   533             using PiE_mem Y by fastforce
   534           ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
   535             by auto
   536         qed (use Y in fastforce)
   537       qed
   538     qed
   539     show ?thesis
   540       unfolding relative_to_def intersection_of_def
   541       by (safe; blast dest!: 1 2)
   542   qed
   543   show ?thesis
   544     unfolding product_topology_def generate_topology_on_eq
   545     apply (rule arg_cong [where f = topology])
   546     apply (rule arg_cong [where f = "(union_of)arbitrary"])
   547     apply (force simp: *)
   548     done
   549 qed
   550 
   551 lemma%important topspace_product_topology:
   552   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
   553 proof%unimportant
   554   show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
   555     unfolding product_topology_def topology_generated_by_topspace
   556     unfolding topspace_def by auto
   557   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)}}"
   558     using openin_topspace not_finite_existsD by auto
   559   then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
   560     unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
   561 qed
   562 
   563 lemma%unimportant product_topology_basis:
   564   assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
   565   shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
   566   unfolding product_topology_def
   567   by (rule topology_generated_by_Basis) (use assms in auto)
   568 
   569 lemma%important product_topology_open_contains_basis:
   570   assumes "openin (product_topology T I) U" "x \<in> U"
   571   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"
   572 proof%unimportant -
   573   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"
   574     using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
   575   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"
   576   proof induction
   577     case (Int U V x)
   578     then obtain XU XV where H:
   579       "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"
   580       "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"
   581       by auto meson
   582     define X where "X = (\<lambda>i. XU i \<inter> XV i)"
   583     have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
   584       unfolding X_def by (auto simp add: PiE_iff)
   585     then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
   586     moreover have "\<forall>i. openin (T i) (X i)"
   587       unfolding X_def using H by auto
   588     moreover have "finite {i. X i \<noteq> topspace (T i)}"
   589       apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
   590       unfolding X_def using H by auto
   591     moreover have "x \<in> Pi\<^sub>E I X"
   592       unfolding X_def using H by auto
   593     ultimately show ?case
   594       by auto
   595   next
   596     case (UN K x)
   597     then obtain k where "k \<in> K" "x \<in> k" by auto
   598     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"
   599       by simp
   600     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"
   601       by blast
   602     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)"
   603       using \<open>k \<in> K\<close> by auto
   604     then show ?case
   605       by auto
   606   qed auto
   607   then show ?thesis using \<open>x \<in> U\<close> by auto
   608 qed
   609 
   610 
   611 lemma openin_product_topology:
   612    "openin (product_topology X I) =
   613     arbitrary union_of
   614           ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
   615            relative_to topspace (product_topology X I))"
   616   apply (subst product_topology)
   617   apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
   618   done
   619 
   620 lemma subtopology_PiE:
   621   "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
   622 proof -
   623   let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
   624   let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
   625   have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
   626         finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
   627     by (rule finite_intersection_of_relative_to)
   628   also have "\<dots> = finite intersection_of
   629                       ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
   630                        relative_to ?X \<inter> Pi\<^sub>E I S)
   631                    relative_to ?X \<inter> Pi\<^sub>E I S"
   632     apply (rule arg_cong2 [where f = "(relative_to)"])
   633      apply (rule arg_cong [where f = "(intersection_of)finite"])
   634      apply (rule ext)
   635      apply (auto simp: relative_to_def intersection_of_def)
   636     done
   637   finally
   638   have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
   639         finite intersection_of
   640           (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
   641           relative_to ?X \<inter> Pi\<^sub>E I S"
   642     by (metis finite_intersection_of_relative_to)
   643   then show ?thesis
   644   unfolding topology_eq
   645   apply clarify
   646   apply (simp add: openin_product_topology flip: openin_relative_to)
   647   apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
   648   done
   649 qed
   650 
   651 
   652 lemma product_topology_base_alt:
   653    "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
   654     relative_to topspace(product_topology X I) =
   655     (\<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))))"
   656    (is "?lhs = ?rhs")
   657 proof -
   658   have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
   659     unfolding all_relative_to all_intersection_of topspace_product_topology
   660   proof clarify
   661     fix \<F>
   662     assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
   663     then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
   664           finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
   665     proof (induction)
   666       case (insert F \<F>)
   667       then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
   668         and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
   669         and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
   670         by auto
   671       obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
   672         using insert by auto
   673       let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
   674       show ?case
   675       proof (intro exI conjI)
   676         show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
   677         using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
   678       next
   679         show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
   680           by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
   681       next
   682         show "\<forall>i\<in>I. openin (X i) (?U i)"
   683           by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
   684       qed
   685     qed (auto intro: dest: not_finite_existsD)
   686   qed
   687   moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
   688   proof clarify
   689     fix U :: "'a \<Rightarrow> 'b set"
   690     assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
   691     let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
   692     show "?lhs (Pi\<^sub>E I U)"
   693       unfolding relative_to_def topspace_product_topology
   694     proof (intro exI conjI)
   695       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"
   696         using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
   697       show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
   698         using ope openin_subset by fastforce
   699     qed
   700   qed
   701   ultimately show ?thesis
   702     by meson
   703 qed
   704 
   705 
   706 lemma topspace_product_topology_alt:
   707    "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
   708   by (force simp: product_topology PiE_def)
   709 
   710 lemma openin_product_topology_alt:
   711   "openin (product_topology X I) S \<longleftrightarrow>
   712     (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
   713                  (\<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)"
   714   apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
   715   apply (drule bspec; blast)
   716   done
   717 
   718 
   719 text \<open>The basic property of the product topology is the continuity of projections:\<close>
   720 
   721 lemma%unimportant continuous_on_topo_product_coordinates [simp]:
   722   assumes "i \<in> I"
   723   shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
   724 proof -
   725   {
   726     fix U assume "openin (T i) U"
   727     define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
   728     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)"
   729       unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
   730       by (auto simp add: PiE_iff, auto, metis subsetCE)
   731     have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
   732       unfolding X_def using \<open>openin (T i) U\<close> by auto
   733     have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
   734       unfolding product_topology_def
   735       apply (rule topology_generated_by_Basis)
   736       apply (subst *)
   737       using ** by auto
   738   }
   739   then show ?thesis unfolding continuous_on_topo_def
   740     by (auto simp add: assms topspace_product_topology PiE_iff)
   741 qed
   742 
   743 lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
   744   assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   745           "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
   746   shows "continuous_on_topo T1 (product_topology T I) f"
   747 unfolding product_topology_def
   748 proof%unimportant (rule continuous_on_generated_topo)
   749   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)}}"
   750   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)}"
   751     by blast
   752   define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
   753   have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
   754   have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
   755     using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
   756   then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
   757     using that unfolding J_def by auto
   758   have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
   759     by (subst H(1), auto simp add: PiE_iff assms)
   760   also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
   761     using * \<open>J \<subseteq> I\<close> by auto
   762   also have "openin T1 (...)"
   763     apply (rule openin_INT)
   764     apply (simp add: \<open>finite J\<close>)
   765     using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
   766   ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
   767 next
   768   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)}}"
   769     apply (subst topology_generated_by_topspace[symmetric])
   770     apply (subst product_topology_def[symmetric])
   771     apply (simp only: topspace_product_topology)
   772     apply (auto simp add: PiE_iff)
   773     using assms unfolding continuous_on_topo_def by auto
   774 qed
   775 
   776 lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:
   777   assumes "continuous_on_topo T1 (product_topology T I) f"
   778   shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   779         "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
   780 proof -
   781   fix i assume "i \<in> I"
   782   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
   783   also have "continuous_on_topo T1 (T i) (...)"
   784     apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
   785     using assms \<open>i \<in> I\<close> by auto
   786   ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   787     by simp
   788 next
   789   fix i x assume "i \<notin> I" "x \<in> topspace T1"
   790   have "f x \<in> topspace (product_topology T I)"
   791     using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   792   then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
   793     using topspace_product_topology by metis
   794   then show "f x i = undefined"
   795     using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
   796 qed
   797 
   798 lemma%unimportant continuous_on_restrict:
   799   assumes "J \<subseteq> I"
   800   shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
   801 proof (rule continuous_on_topo_coordinatewise_then_product)
   802   fix i assume "i \<in> J"
   803   then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
   804   then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
   805     using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
   806 next
   807   fix i assume "i \<notin> J"
   808   then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
   809     unfolding restrict_def by auto
   810 qed
   811 
   812 
   813 subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
   814 
   815 instantiation "fun" :: (type, topological_space) topological_space
   816 begin
   817 
   818 definition%important open_fun_def:
   819   "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
   820 
   821 instance proof%unimportant
   822   have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
   823     unfolding topspace_product_topology topspace_euclidean by auto
   824   then show "open (UNIV::('a \<Rightarrow> 'b) set)"
   825     unfolding open_fun_def by (metis openin_topspace)
   826 qed (auto simp add: open_fun_def)
   827 
   828 end
   829 
   830 lemma%unimportant euclidean_product_topology:
   831   "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
   832 by (metis open_openin topology_eq open_fun_def)
   833 
   834 lemma%important product_topology_basis':
   835   fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
   836   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   837   shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
   838 proof%unimportant -
   839   define J where "J = x`I"
   840   define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
   841   define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
   842   have *: "open (X i)" for i
   843     unfolding X_def V_def using assms by auto
   844   have **: "finite {i. X i \<noteq> UNIV}"
   845     unfolding X_def V_def J_def using assms(1) by auto
   846   have "open (Pi\<^sub>E UNIV X)"
   847     unfolding open_fun_def apply (rule product_topology_basis)
   848     using * ** unfolding open_openin topspace_euclidean by auto
   849   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
   850     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
   851     proof (auto)
   852       fix f :: "'a \<Rightarrow> 'b" and i :: 'i
   853       assume a1: "i \<in> I"
   854       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)"
   855       have f3: "x i \<in> x`I"
   856         using a1 by blast
   857       have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
   858         using a1 by blast
   859       then show "f (x i) \<in> U i"
   860         using f3 a2 by (meson Inter_iff)
   861     qed
   862   ultimately show ?thesis by simp
   863 qed
   864 
   865 text \<open>The results proved in the general situation of products of possibly different
   866 spaces have their counterparts in this simpler setting.\<close>
   867 
   868 lemma%unimportant continuous_on_product_coordinates [simp]:
   869   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
   870 unfolding continuous_on_topo_UNIV euclidean_product_topology
   871 by (rule continuous_on_topo_product_coordinates, simp)
   872 
   873 lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:
   874   assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
   875   shows "continuous_on UNIV f"
   876 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
   877 by (rule continuous_on_topo_coordinatewise_then_product, simp)
   878 
   879 lemma%unimportant continuous_on_product_then_coordinatewise:
   880   assumes "continuous_on UNIV f"
   881   shows "continuous_on UNIV (\<lambda>x. f x i)"
   882 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
   883 by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
   884 
   885 lemma%unimportant continuous_on_product_coordinatewise_iff:
   886   "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
   887 by (auto intro: continuous_on_product_then_coordinatewise)
   888 
   889 subsubsection%important \<open>Topological countability for product spaces\<close>
   890 
   891 text \<open>The next two lemmas are useful to prove first or second countability
   892 of product spaces, but they have more to do with countability and could
   893 be put in the corresponding theory.\<close>
   894 
   895 lemma%unimportant countable_nat_product_event_const:
   896   fixes F::"'a set" and a::'a
   897   assumes "a \<in> F" "countable F"
   898   shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
   899 proof -
   900   have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
   901                   \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
   902     using infinite_nat_iff_unbounded_le by fastforce
   903   have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
   904   proof (induction N)
   905     case 0
   906     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
   907       using \<open>a \<in> F\<close> by auto
   908     then show ?case by auto
   909   next
   910     case (Suc N)
   911     define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
   912       where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
   913     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)"
   914     proof (auto)
   915       fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
   916       define y where "y = (\<lambda>i. if i = N then a else x i)"
   917       have "f (y, x N) = x"
   918         unfolding f_def y_def by auto
   919       moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
   920         unfolding y_def using H \<open>a \<in> F\<close> by auto
   921       ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
   922         by (metis (no_types, lifting) image_eqI)
   923     qed
   924     moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
   925       using Suc.IH assms(2) by auto
   926     ultimately show ?case
   927       by (meson countable_image countable_subset)
   928   qed
   929   then show ?thesis using countable_subset[OF *] by auto
   930 qed
   931 
   932 lemma%unimportant countable_product_event_const:
   933   fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
   934   assumes "\<And>i. countable (F i)"
   935   shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
   936 proof -
   937   define G where "G = (\<Union>i. F i) \<union> {b}"
   938   have "countable G" unfolding G_def using assms by auto
   939   have "b \<in> G" unfolding G_def by auto
   940   define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
   941   have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
   942         \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
   943   proof (auto)
   944     fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
   945     define I where "I = {i. f i \<noteq> b}"
   946     define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
   947     have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
   948     then have "finite {j. g j \<noteq> b}"
   949       unfolding I_def using H(2) using finite_surj by blast
   950     moreover have "g j \<in> G" for j
   951       unfolding g_def G_def using H by auto
   952     ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
   953       by auto
   954     moreover have "f = pi g"
   955       unfolding pi_def g_def I_def using H by fastforce
   956     ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
   957       by auto
   958   qed
   959   then show ?thesis
   960     using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
   961     by (meson countable_image countable_subset)
   962 qed
   963 
   964 instance "fun" :: (countable, first_countable_topology) first_countable_topology
   965 proof%unimportant
   966   fix x::"'a \<Rightarrow> 'b"
   967   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))"
   968     apply (rule choice) using first_countable_basis by auto
   969   then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
   970                                                   "\<And>x i. open (A x i)"
   971                                                   "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
   972     by metis
   973   text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
   974   define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
   975   have "countable (B i)" for i unfolding B_def by auto
   976 
   977   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
   978   have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
   979     unfolding K_def B_def by auto
   980   then have "K \<noteq> {}" by auto
   981   have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
   982     apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
   983   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}}"
   984     unfolding K_def by auto
   985   ultimately have "countable K" by auto
   986   have "x \<in> k" if "k \<in> K" for k
   987     using that unfolding K_def B_def apply auto using A(1) by auto
   988   have "open k" if "k \<in> K" for k
   989     using that unfolding open_fun_def K_def B_def apply (auto)
   990     apply (rule product_topology_basis)
   991     unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
   992 
   993   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
   994   proof -
   995     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
   996       using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
   997     with product_topology_open_contains_basis[OF this]
   998     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"
   999       unfolding topspace_euclidean open_openin by simp
  1000     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
  1001                            "\<And>i. open (X i)"
  1002                            "finite {i. X i \<noteq> UNIV}"
  1003                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
  1004       by auto
  1005     define I where "I = {i. X i \<noteq> UNIV}"
  1006     define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
  1007     have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
  1008       unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
  1009     have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
  1010       apply (cases "i \<in> I")
  1011       unfolding Y_def using * that apply (auto)
  1012       apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
  1013       unfolding B_def apply simp
  1014       unfolding I_def apply auto
  1015       done
  1016     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
  1017       unfolding Y_def by auto
  1018     then have ***: "finite {i. Y i \<noteq> UNIV}"
  1019       unfolding I_def using H(3) rev_finite_subset by blast
  1020     have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
  1021       using ** *** by auto
  1022     then have "Pi\<^sub>E UNIV Y \<in> K"
  1023       unfolding K_def by auto
  1024 
  1025     have "Y i \<subseteq> X i" for i
  1026       apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
  1027     then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
  1028     then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
  1029     then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
  1030   qed
  1031 
  1032   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))"
  1033     apply (rule first_countableI[of K])
  1034     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
  1035 qed
  1036 
  1037 lemma%important product_topology_countable_basis:
  1038   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
  1039           topological_basis K \<and> countable K \<and>
  1040           (\<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})"
  1041 proof%unimportant -
  1042   obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
  1043     using ex_countable_basis by auto
  1044   then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
  1045   define B2 where "B2 = B \<union> {UNIV}"
  1046   have "countable B2"
  1047     unfolding B2_def using B by auto
  1048   have "open U" if "U \<in> B2" for U
  1049     using that unfolding B2_def using B topological_basis_open by auto
  1050 
  1051   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
  1052   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}"
  1053     unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
  1054 
  1055   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
  1056     apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
  1057   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
  1058     unfolding K_def by auto
  1059   ultimately have ii: "countable K" by auto
  1060 
  1061   have iii: "topological_basis K"
  1062   proof (rule topological_basisI)
  1063     fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
  1064     then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
  1065       unfolding open_fun_def by auto
  1066     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
  1067     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"
  1068       unfolding topspace_euclidean open_openin by simp
  1069     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
  1070                            "\<And>i. open (X i)"
  1071                            "finite {i. X i \<noteq> UNIV}"
  1072                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
  1073       by auto
  1074     then have "x i \<in> X i" for i by auto
  1075     define I where "I = {i. X i \<noteq> UNIV}"
  1076     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)"
  1077     have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
  1078       unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
  1079     have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
  1080       using someI_ex[OF *]
  1081       apply (cases "i \<in> I")
  1082       unfolding Y_def using * apply (auto)
  1083       unfolding B2_def I_def by auto
  1084     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
  1085       unfolding Y_def by auto
  1086     then have ***: "finite {i. Y i \<noteq> UNIV}"
  1087       unfolding I_def using H(3) rev_finite_subset by blast
  1088     have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
  1089       using ** *** by auto
  1090     then have "Pi\<^sub>E UNIV Y \<in> K"
  1091       unfolding K_def by auto
  1092 
  1093     have "Y i \<subseteq> X i" for i
  1094       apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
  1095     then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
  1096     then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
  1097 
  1098     have "x \<in> Pi\<^sub>E UNIV Y"
  1099       using ** by auto
  1100 
  1101     show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
  1102       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
  1103   next
  1104     fix U assume "U \<in> K"
  1105     show "open U"
  1106       using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
  1107       apply (rule product_topology_basis)
  1108       using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
  1109       by auto
  1110   qed
  1111 
  1112   show ?thesis using i ii iii by auto
  1113 qed
  1114 
  1115 instance "fun" :: (countable, second_countable_topology) second_countable_topology
  1116   apply standard
  1117   using product_topology_countable_basis topological_basis_imp_subbasis by auto
  1118 
  1119 
  1120 subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
  1121 
  1122 text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
  1123 operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
  1124 (the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
  1125 
  1126 However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
  1127 $T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
  1128 where the target space is endowed with the norm topology. It is especially useful when 'b is the set
  1129 of real numbers, since then this topology is compact.
  1130 
  1131 We can not implement it using type classes as there is already a topology, but at least we
  1132 can define it as a topology.
  1133 
  1134 Note that there is yet another (common and useful) topology on operator spaces, the weak operator
  1135 topology, defined analogously using the product topology, but where the target space is given the
  1136 weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
  1137 canonical embedding of a space into its bidual. We do not define it there, although it could also be
  1138 defined analogously.
  1139 \<close>
  1140 
  1141 definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
  1142 where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
  1143 
  1144 lemma%unimportant strong_operator_topology_topspace:
  1145   "topspace strong_operator_topology = UNIV"
  1146 unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
  1147 
  1148 lemma%important strong_operator_topology_basis:
  1149   fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
  1150   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
  1151   shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
  1152 proof%unimportant -
  1153   have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
  1154     by (rule product_topology_basis'[OF assms])
  1155   moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
  1156                 = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
  1157     by auto
  1158   ultimately show ?thesis
  1159     unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
  1160 qed
  1161 
  1162 lemma%important strong_operator_topology_continuous_evaluation:
  1163   "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
  1164 proof%unimportant -
  1165   have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
  1166     unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
  1167     using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
  1168   then show ?thesis unfolding comp_def by simp
  1169 qed
  1170 
  1171 lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:
  1172   "continuous_on_topo T strong_operator_topology f
  1173     \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
  1174 proof (auto)
  1175   fix x::"'b"
  1176   assume "continuous_on_topo T strong_operator_topology f"
  1177   with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
  1178   have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
  1179     by simp
  1180   then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
  1181     unfolding comp_def by auto
  1182 next
  1183   assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
  1184   have "continuous_on_topo T euclidean (blinfun_apply o f)"
  1185     unfolding euclidean_product_topology
  1186     apply (rule continuous_on_topo_coordinatewise_then_product, auto)
  1187     using * unfolding comp_def by auto
  1188   show "continuous_on_topo T strong_operator_topology f"
  1189     unfolding strong_operator_topology_def
  1190     apply (rule continuous_on_topo_pullback')
  1191     by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
  1192 qed
  1193 
  1194 lemma%important strong_operator_topology_weaker_than_euclidean:
  1195   "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
  1196 by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
  1197     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
  1198 
  1199 
  1200 subsection%important \<open>Metrics on product spaces\<close>
  1201 
  1202 
  1203 text \<open>In general, the product topology is not metrizable, unless the index set is countable.
  1204 When the index set is countable, essentially any (convergent) combination of the metrics on the
  1205 factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
  1206 for instance.
  1207 
  1208 What is not completely trivial is that the distance thus defined induces the same topology
  1209 as the product topology. This is what we have to prove to show that we have an instance
  1210 of \verb+metric_space+.
  1211 
  1212 The proofs below would work verbatim for general countable products of metric spaces. However,
  1213 since distances are only implemented in terms of type classes, we only develop the theory
  1214 for countable products of the same space.\<close>
  1215 
  1216 instantiation "fun" :: (countable, metric_space) metric_space
  1217 begin
  1218 
  1219 definition%important dist_fun_def:
  1220   "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1221 
  1222 definition%important uniformity_fun_def:
  1223   "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
  1224 
  1225 text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
  1226 instance: once it is proved, they become trivial consequences of the general theory of metric
  1227 spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
  1228 to do this.\<close>
  1229 
  1230 lemma%important dist_fun_le_dist_first_terms:
  1231   "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
  1232 proof%unimportant -
  1233   have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
  1234           = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
  1235     by (rule suminf_cong, simp add: power_add)
  1236   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)"
  1237     apply (rule suminf_mult)
  1238     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1239   also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
  1240     apply (simp, rule suminf_le, simp)
  1241     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1242   also have "... = (1/2)^(Suc N) * 2"
  1243     using suminf_geometric[of "1/2"] by auto
  1244   also have "... = (1/2)^N"
  1245     by auto
  1246   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"
  1247     by simp
  1248 
  1249   define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
  1250   have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
  1251     unfolding M_def by (rule Max_ge, auto)
  1252   then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
  1253   have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
  1254     unfolding M_def apply (rule Max_ge) using that by auto
  1255   then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
  1256     using that by force
  1257   have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
  1258       (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
  1259     by (rule sum_mono, simp add: i)
  1260   also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
  1261     by (rule sum_distrib_left[symmetric])
  1262   also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
  1263     by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
  1264   also have "... = M * 2"
  1265     using suminf_geometric[of "1/2"] by auto
  1266   finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
  1267     by simp
  1268 
  1269   have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1270     unfolding dist_fun_def by simp
  1271   also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
  1272                   + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1273     apply (rule suminf_split_initial_segment)
  1274     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1275   also have "... \<le> 2 * M + (1/2)^N"
  1276     using * ** by auto
  1277   finally show ?thesis unfolding M_def by simp
  1278 qed
  1279 
  1280 lemma%unimportant open_fun_contains_ball_aux:
  1281   assumes "open (U::(('a \<Rightarrow> 'b) set))"
  1282           "x \<in> U"
  1283   shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
  1284 proof -
  1285   have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
  1286     using open_fun_def assms by auto
  1287   obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
  1288                     "\<And>i. openin euclidean (X i)"
  1289                     "finite {i. X i \<noteq> topspace euclidean}"
  1290                     "x \<in> Pi\<^sub>E UNIV X"
  1291     using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
  1292   define I where "I = {i. X i \<noteq> topspace euclidean}"
  1293   have "finite I" unfolding I_def using H(3) by auto
  1294   {
  1295     fix i
  1296     have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
  1297     then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
  1298       using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
  1299     then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
  1300     define f where "f = min e (1/2)"
  1301     have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
  1302     moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
  1303     ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
  1304   } note * = this
  1305   have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
  1306     by (rule choice, auto simp add: *)
  1307   then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
  1308     by blast
  1309   define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
  1310   have "m > 0" if "I\<noteq>{}"
  1311     unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
  1312   moreover have "{y. dist x y < m} \<subseteq> U"
  1313   proof (auto)
  1314     fix y assume "dist x y < m"
  1315     have "y i \<in> X i" if "i \<in> I" for i
  1316     proof -
  1317       have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1318         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1319       define n where "n = to_nat i"
  1320       have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
  1321         using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
  1322       then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
  1323         using \<open>n = to_nat i\<close> by auto
  1324       also have "... \<le> (1/2)^(to_nat i) * e i"
  1325         unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
  1326       ultimately have "min (dist (x i) (y i)) 1 < e i"
  1327         by (auto simp add: divide_simps)
  1328       then have "dist (x i) (y i) < e i"
  1329         using \<open>e i < 1\<close> by auto
  1330       then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
  1331     qed
  1332     then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
  1333     then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
  1334   qed
  1335   ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
  1336 
  1337   have "U = UNIV" if "I = {}"
  1338     using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
  1339   then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
  1340   then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
  1341 qed
  1342 
  1343 lemma%unimportant ball_fun_contains_open_aux:
  1344   fixes x::"('a \<Rightarrow> 'b)" and e::real
  1345   assumes "e>0"
  1346   shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
  1347 proof -
  1348   have "\<exists>N::nat. 2^N > 8/e"
  1349     by (simp add: real_arch_pow)
  1350   then obtain N::nat where "2^N > 8/e" by auto
  1351   define f where "f = e/4"
  1352   have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
  1353   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)"
  1354   have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
  1355     unfolding X_def by auto
  1356   then have "finite {i. X i \<noteq> topspace euclidean}"
  1357     unfolding topspace_euclidean using finite_surj by blast
  1358   have "\<And>i. open (X i)"
  1359     unfolding X_def using metric_space_class.open_ball open_UNIV by auto
  1360   then have "\<And>i. openin euclidean (X i)"
  1361     using open_openin by auto
  1362   define U where "U = Pi\<^sub>E UNIV X"
  1363   have "open U"
  1364     unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
  1365     unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
  1366     by auto
  1367   moreover have "x \<in> U"
  1368     unfolding U_def X_def by (auto simp add: PiE_iff)
  1369   moreover have "dist x y < e" if "y \<in> U" for y
  1370   proof -
  1371     have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
  1372       using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
  1373       unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
  1374     have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
  1375       apply (rule Max.boundedI) using * by auto
  1376 
  1377     have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
  1378       by (rule dist_fun_le_dist_first_terms)
  1379     also have "... \<le> 2 * f + e / 8"
  1380       apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
  1381     also have "... \<le> e/2 + e/8"
  1382       unfolding f_def by auto
  1383     also have "... < e"
  1384       by auto
  1385     finally show "dist x y < e" by simp
  1386   qed
  1387   ultimately show ?thesis by auto
  1388 qed
  1389 
  1390 lemma%unimportant fun_open_ball_aux:
  1391   fixes U::"('a \<Rightarrow> 'b) set"
  1392   shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
  1393 proof (auto)
  1394   assume "open U"
  1395   fix x assume "x \<in> U"
  1396   then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
  1397     using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
  1398 next
  1399   assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
  1400   define K where "K = {V. open V \<and> V \<subseteq> U}"
  1401   {
  1402     fix x assume "x \<in> U"
  1403     then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
  1404     then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
  1405       using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
  1406     have "V \<in> K"
  1407       unfolding K_def using e(2) V(1) V(3) by auto
  1408     then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
  1409   }
  1410   then have "(\<Union>K) = U"
  1411     unfolding K_def by auto
  1412   moreover have "open (\<Union>K)"
  1413     unfolding K_def by auto
  1414   ultimately show "open U" by simp
  1415 qed
  1416 
  1417 instance proof
  1418   fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
  1419   proof
  1420     assume "x = y"
  1421     then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
  1422   next
  1423     assume "dist x y = 0"
  1424     have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1425       by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1426     have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
  1427       using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
  1428     then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
  1429       by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
  1430                 zero_eq_1_divide_iff zero_neq_numeral)
  1431     then have "x (from_nat n) = y (from_nat n)" for n
  1432       by auto
  1433     then have "x i = y i" for i
  1434       by (metis from_nat_to_nat)
  1435     then show "x = y"
  1436       by auto
  1437   qed
  1438 next
  1439   text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
  1440         with infinite series, hence we should justify the convergence at each step. In this
  1441         respect, the following simplification rule is extremely handy.\<close>
  1442   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"
  1443     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1444   fix x y z::"'a \<Rightarrow> 'b"
  1445   {
  1446     fix n
  1447     have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
  1448             dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
  1449       by (simp add: dist_triangle2)
  1450     have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
  1451       using zero_le_dist by blast
  1452     moreover
  1453     {
  1454       assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
  1455       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"
  1456         by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
  1457     }
  1458     ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
  1459             min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
  1460       using * by linarith
  1461   } note ineq = this
  1462   have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
  1463     unfolding dist_fun_def by simp
  1464   also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
  1465                         + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
  1466     apply (rule suminf_le)
  1467     using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
  1468       le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
  1469     by (auto simp add: summable_add)
  1470   also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
  1471                   + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
  1472     by (rule suminf_add[symmetric], auto)
  1473   also have "... = dist x z + dist y z"
  1474     unfolding dist_fun_def by simp
  1475   finally show "dist x y \<le> dist x z + dist y z"
  1476     by simp
  1477 next
  1478   text\<open>Finally, we show that the topology generated by the distance and the product
  1479         topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
  1480         except that the condition to prove is expressed with filters. To deal with this,
  1481         we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
  1482         \verb+Real_Vector_Spaces.thy+\<close>
  1483   fix U::"('a \<Rightarrow> 'b) set"
  1484   have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
  1485   unfolding uniformity_fun_def apply (subst eventually_INF_base)
  1486     by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
  1487   then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
  1488     unfolding fun_open_ball_aux by simp
  1489 qed (simp add: uniformity_fun_def)
  1490 
  1491 end
  1492 
  1493 text \<open>Nice properties of spaces are preserved under countable products. In addition
  1494 to first countability, second countability and metrizability, as we have seen above,
  1495 completeness is also preserved, and therefore being Polish.\<close>
  1496 
  1497 instance "fun" :: (countable, complete_space) complete_space
  1498 proof
  1499   fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
  1500   have "Cauchy (\<lambda>n. u n i)" for i
  1501   unfolding cauchy_def proof (intro impI allI)
  1502     fix e assume "e>(0::real)"
  1503     obtain k where "i = from_nat k"
  1504       using from_nat_to_nat[of i] by metis
  1505     have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
  1506     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"
  1507       using \<open>Cauchy u\<close> unfolding cauchy_def by blast
  1508     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"
  1509       by blast
  1510     have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
  1511     proof (auto)
  1512       fix m n::nat assume "m \<ge> N" "n \<ge> N"
  1513       have "(1/2)^k * min (dist (u m i) (u n i)) 1
  1514               = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
  1515         using \<open>i = from_nat k\<close> by auto
  1516       also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
  1517         apply (rule sum_le_suminf)
  1518         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
  1519       also have "... = dist (u m) (u n)"
  1520         unfolding dist_fun_def by auto
  1521       also have "... < (1/2)^k * min e 1"
  1522         using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
  1523       finally have "min (dist (u m i) (u n i)) 1 < min e 1"
  1524         by (auto simp add: algebra_simps divide_simps)
  1525       then show "dist (u m i) (u n i) < e" by auto
  1526     qed
  1527     then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
  1528       by blast
  1529   qed
  1530   then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
  1531     using Cauchy_convergent convergent_def by auto
  1532   then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
  1533     using choice by force
  1534   then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
  1535   have "u \<longlonglongrightarrow> x"
  1536   proof (rule metric_LIMSEQ_I)
  1537     fix e assume [simp]: "e>(0::real)"
  1538     have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
  1539       by (rule metric_LIMSEQ_D, auto simp add: *)
  1540     have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
  1541       apply (rule choice) using i by auto
  1542     then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
  1543       by blast
  1544 
  1545     have "\<exists>N::nat. 2^N > 4/e"
  1546       by (simp add: real_arch_pow)
  1547     then obtain N::nat where "2^N > 4/e" by auto
  1548     define L where "L = Max {K (from_nat n)|n. n \<le> N}"
  1549     have "dist (u k) x < e" if "k \<ge> L" for k
  1550     proof -
  1551       have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
  1552       proof -
  1553         have "K (from_nat n) \<le> L"
  1554           unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
  1555         then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
  1556         then show ?thesis using K less_imp_le by auto
  1557       qed
  1558       have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
  1559         apply (rule Max.boundedI) using * by auto
  1560       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"
  1561         using dist_fun_le_dist_first_terms by auto
  1562       also have "... \<le> 2 * e/4 + e/4"
  1563         apply (rule add_mono)
  1564         using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
  1565       also have "... < e" by auto
  1566       finally show ?thesis by simp
  1567     qed
  1568     then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
  1569   qed
  1570   then show "convergent u" using convergent_def by blast
  1571 qed
  1572 
  1573 instance "fun" :: (countable, polish_space) polish_space
  1574 by standard
  1575 
  1576 
  1577 
  1578 
  1579 subsection%important \<open>Measurability\<close> (*FIX ME mv *)
  1580 
  1581 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
  1582 generated by open sets in the product, and the product sigma algebra, countably generated by
  1583 products of measurable sets along finitely many coordinates. The second one is defined and studied
  1584 in \verb+Finite_Product_Measure.thy+.
  1585 
  1586 These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
  1587 but there is a fundamental difference: open sets are generated by arbitrary unions, not only
  1588 countable ones, so typically many open sets will not be measurable with respect to the product sigma
  1589 algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
  1590 only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
  1591 the factor is countably generated).
  1592 
  1593 In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
  1594 compare it with the product sigma algebra as explained above.
  1595 \<close>
  1596 
  1597 lemma%unimportant measurable_product_coordinates [measurable (raw)]:
  1598   "(\<lambda>x. x i) \<in> measurable borel borel"
  1599 by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
  1600 
  1601 lemma%unimportant measurable_product_then_coordinatewise:
  1602   fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
  1603   assumes [measurable]: "f \<in> borel_measurable M"
  1604   shows "(\<lambda>x. f x i) \<in> borel_measurable M"
  1605 proof -
  1606   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
  1607     unfolding comp_def by auto
  1608   then show ?thesis by simp
  1609 qed
  1610 
  1611 text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
  1612 of the product sigma algebra that is more similar to the one we used above for the product
  1613 topology.\<close>
  1614 
  1615 lemma%important sets_PiM_finite:
  1616   "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
  1617         {(\<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)}}"
  1618 proof%unimportant
  1619   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)"
  1620   proof (auto)
  1621     fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
  1622     then have *: "X i \<in> sets (M i)" for i by simp
  1623     define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
  1624     have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
  1625     define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
  1626     have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
  1627       unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
  1628     moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
  1629       unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
  1630       by (auto simp add: PiE_iff, blast)
  1631     ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
  1632   qed
  1633   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)}}
  1634               \<subseteq> sets (Pi\<^sub>M I M)"
  1635     by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
  1636 
  1637   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>
  1638                 (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
  1639     if "i \<in> I" "A \<in> sets (M i)" for i A
  1640   proof -
  1641     define X where "X = (\<lambda>j. if j = i then A else space (M j))"
  1642     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"
  1643       unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
  1644       by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
  1645     moreover have "X j \<in> sets (M j)" for j
  1646       unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
  1647     moreover have "finite {j. X j \<noteq> space (M j)}"
  1648       unfolding X_def by simp
  1649     ultimately show ?thesis by auto
  1650   qed
  1651   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)}}"
  1652     unfolding sets_PiM_single
  1653     apply (rule sigma_sets_mono')
  1654     apply (auto simp add: PiE_iff *)
  1655     done
  1656 qed
  1657 
  1658 lemma%important sets_PiM_subset_borel:
  1659   "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
  1660 proof%unimportant -
  1661   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"
  1662   proof -
  1663     define I where "I = {i. X i \<noteq> UNIV}"
  1664     have "finite I" unfolding I_def using that by simp
  1665     have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
  1666       unfolding I_def by auto
  1667     also have "... \<in> sets borel"
  1668       using that \<open>finite I\<close> by measurable
  1669     finally show ?thesis by simp
  1670   qed
  1671   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"
  1672     by auto
  1673   then show ?thesis unfolding sets_PiM_finite space_borel
  1674     by (simp add: * sets.sigma_sets_subset')
  1675 qed
  1676 
  1677 lemma%important sets_PiM_equal_borel:
  1678   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
  1679 proof%unimportant
  1680   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
  1681             "\<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}"
  1682     using product_topology_countable_basis by fast
  1683   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
  1684   proof -
  1685     obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
  1686       using K(3)[OF \<open>k \<in> K\<close>] by blast
  1687     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
  1688   qed
  1689   have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
  1690   proof -
  1691     obtain B where "B \<subseteq> K" "U = (\<Union>B)"
  1692       using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
  1693     have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
  1694     moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
  1695       using \<open>B \<subseteq> K\<close> * that by auto
  1696     ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
  1697   qed
  1698   have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
  1699     apply (rule sets.sigma_sets_subset') using ** by auto
  1700   then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
  1701     unfolding borel_def by auto
  1702 qed (simp add: sets_PiM_subset_borel)
  1703 
  1704 lemma%important measurable_coordinatewise_then_product:
  1705   fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
  1706   assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
  1707   shows "f \<in> borel_measurable M"
  1708 proof%unimportant -
  1709   have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
  1710     by (rule measurable_PiM_single', auto simp add: assms)
  1711   then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
  1712 qed
  1713 
  1714 end