src/HOL/Analysis/Function_Topology.thy

 theory Function_Topology
 imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
 begin
 
 
-section {*Product topology*}
-
-text {*We want to define the product topology.
+section \<open>Product topology\<close>
+
+text \<open>We want to define the product topology.
 
 The product topology on a product of topological spaces is generated by
 the sets which are products of open sets along finitely many coordinates, and the whole
 space along the other coordinates. This is the coarsest topology for which the projection
 to each factor is continuous.

 I only develop the basics of the product topology in this theory. The most important missing piece
 is Tychonov theorem, stating that a product of compact spaces is always compact for the product
 topology, even when the product is not finite (or even countable).
 
 I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
-*}
-
-subsection {*Topology without type classes*}
-
-subsubsection {*The topology generated by some (open) subsets*}
-
-text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
+\<close>
+
+subsection \<open>Topology without type classes\<close>
+
+subsubsection \<open>The topology generated by some (open) subsets\<close>
+
+text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
 as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
 and is never a problem in proofs, so I prefer to write it down explicitly.
 
 We do not require UNIV to be an open set, as this will not be the case in applications. (We are
-thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)*}
+thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
 
 inductive generate_topology_on for S where
 Empty: "generate_topology_on S {}"
 |Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"

 
 lemma istopology_generate_topology_on:
   "istopology (generate_topology_on S)"
 unfolding istopology_def by (auto intro: generate_topology_on.intros)
 
-text {*The basic property of the topology generated by a set $S$ is that it is the
-smallest topology containing all the elements of $S$:*}
+text \<open>The basic property of the topology generated by a set $S$ is that it is the
+smallest topology containing all the elements of $S$:\<close>
 
 lemma generate_topology_on_coarsest:
   assumes "istopology T"
           "\<And>s. s \<in> S \<Longrightarrow> T s"
           "generate_topology_on S s0"

 
 lemma topology_generated_by_Basis:
   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
 by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
 
-subsubsection {*Continuity*}
-
-text {*We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.*}
+subsubsection \<open>Continuity\<close>
+
+text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.\<close>
 
 definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
                                       \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
 

   assumes "continuous_on_topo T1 T2 f"
   shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
 using assms unfolding continuous_on_topo_def by auto
 
 
-subsubsection {*Pullback topology*}
-
-text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
+subsubsection \<open>Pullback topology\<close>
+
+text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
 a special case of this notion, pulling back by the identity. We introduce the general notion as
 we will need it to define the strong operator topology on the space of continuous linear operators,
-by pulling back the product topology on the space of all functions.*}
-
-text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
-the set $A$.*}
+by pulling back the product topology on the space of all functions.\<close>
+
+text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
+the set $A$.\<close>
 
 definition pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
 
 lemma istopology_pullback_topology:

   have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
     unfolding topspace_pullback_topology by auto
   also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
     by auto
   also have "openin (pullback_topology A f T1) (...)"
-    unfolding openin_pullback_topology using `openin T1 (g-\`U \<inter> topspace T1)` by auto
+    unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
   finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
     by auto
 next
   fix x assume "x \<in> topspace (pullback_topology A f T1)"
   then have "f x \<in> topspace T1"

   also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
     by auto
   also have "... = (f o g)-`V \<inter> topspace T1"
     using assms(2) by auto
   also have "openin T1 (...)"
-    using assms(1) `openin T2 V` by auto
+    using assms(1) \<open>openin T2 V\<close> by auto
   finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
 next
   fix x assume "x \<in> topspace T1"
   have "(f o g) x \<in> topspace T2"
-    using assms(1) `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   then have "g x \<in> f-`(topspace T2)"
     unfolding comp_def by blast
-  moreover have "g x \<in> A" using assms(2) `x \<in> topspace T1` by blast
+  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
   ultimately show "g x \<in> topspace (pullback_topology A f T2)"
     unfolding topspace_pullback_topology by blast
 qed
 
 
-subsection {*The product topology*}
-
-text {*We can now define the product topology, as generated by
+subsection \<open>The product topology\<close>
+
+text \<open>We can now define the product topology, as generated by
 the sets which are products of open sets along finitely many coordinates, and the whole
 space along the other coordinates. Equivalently, it is generated by sets which are one open
 set along one single coordinate, and the whole space along other coordinates. In fact, this is only
 equivalent for nonempty products, but for the empty product the first formulation is better
 (the second one gives an empty product space, while an empty product should have exactly one
 point, equal to \verb+undefined+ along all coordinates.
 
 So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
-*}
+\<close>
 
 definition product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
   where "product_topology T I =
     topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
 
-text {*The total set of the product topology is the product of the total sets
-along each coordinate.*}
+text \<open>The total set of the product topology is the product of the total sets
+along each coordinate.\<close>
 
 lemma product_topology_topspace:
   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
 proof
   show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"

     with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
       by simp
     then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
       by blast
     then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
-      using `k \<in> K` by auto
+      using \<open>k \<in> K\<close> by auto
     then show ?case
       by auto
   qed auto
-  then show ?thesis using `x \<in> U` by auto
-qed
-
-
-text {*The basic property of the product topology is the continuity of projections:*}
+  then show ?thesis using \<open>x \<in> U\<close> by auto
+qed
+
+
+text \<open>The basic property of the product topology is the continuity of projections:\<close>
 
 lemma continuous_on_topo_product_coordinates [simp]:
   assumes "i \<in> I"
   shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
 proof -
   {
     fix U assume "openin (T i) U"
     define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
     then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
-      unfolding X_def using assms openin_subset[OF `openin (T i) U`]
+      unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
       by (auto simp add: PiE_iff, auto, metis subsetCE)
     have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
-      unfolding X_def using `openin (T i) U` by auto
+      unfolding X_def using \<open>openin (T i) U\<close> by auto
     have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
       unfolding product_topology_def
       apply (rule topology_generated_by_Basis)
       apply (subst *)
       using ** by auto

   then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
     using that unfolding J_def by auto
   have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
     by (subst H(1), auto simp add: PiE_iff assms)
   also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
-    using * `J \<subseteq> I` by auto
+    using * \<open>J \<subseteq> I\<close> by auto
   also have "openin T1 (...)"
     apply (rule openin_INT)
-    apply (simp add: `finite J`)
-    using H(2) assms(1) `J \<subseteq> I` by auto
+    apply (simp add: \<open>finite J\<close>)
+    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
   ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
 next
   show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
     apply (subst topology_generated_by_topspace[symmetric])
     apply (subst product_topology_def[symmetric])

 proof -
   fix i assume "i \<in> I"
   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
   also have "continuous_on_topo T1 (T i) (...)"
     apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
-    using assms `i \<in> I` by auto
+    using assms \<open>i \<in> I\<close> by auto
   ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
     by simp
 next
   fix i x assume "i \<notin> I" "x \<in> topspace T1"
   have "f x \<in> topspace (product_topology T I)"
-    using assms `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
     using product_topology_topspace by metis
   then show "f x i = undefined"
-    using `i \<notin> I` by (auto simp add: PiE_iff extensional_def)
+    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
 qed
 
 lemma continuous_on_restrict:
   assumes "J \<subseteq> I"
   shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
 proof (rule continuous_on_topo_coordinatewise_then_product)
   fix i assume "i \<in> J"
   then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
   then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
-    using `i \<in> J` `J \<subseteq> I` by auto
+    using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
 next
   fix i assume "i \<notin> J"
   then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
     unfolding restrict_def by auto
 qed
 
 
-subsubsection {*Powers of a single topological space as a topological space, using type classes*}
+subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
 
 instantiation "fun" :: (type, topological_space) topological_space
 begin
 
 definition open_fun_def:

         using f3 a2 by (meson Inter_iff)
     qed
   ultimately show ?thesis by simp
 qed
 
-text {*The results proved in the general situation of products of possibly different
-spaces have their counterparts in this simpler setting.*}
+text \<open>The results proved in the general situation of products of possibly different
+spaces have their counterparts in this simpler setting.\<close>
 
 lemma continuous_on_product_coordinates [simp]:
   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
 unfolding continuous_on_topo_UNIV euclidean_product_topology
 by (rule continuous_on_topo_product_coordinates, simp)

 
 lemma continuous_on_product_coordinatewise_iff:
   "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
 by (auto intro: continuous_on_product_then_coordinatewise)
 
-subsubsection {*Topological countability for product spaces*}
-
-text {*The next two lemmas are useful to prove first or second countability
+subsubsection \<open>Topological countability for product spaces\<close>
+
+text \<open>The next two lemmas are useful to prove first or second countability
 of product spaces, but they have more to do with countability and could
-be put in the corresponding theory.*}
+be put in the corresponding theory.\<close>
 
 lemma countable_nat_product_event_const:
   fixes F::"'a set" and a::'a
   assumes "a \<in> F" "countable F"
   shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"

     using infinite_nat_iff_unbounded_le by fastforce
   have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
   proof (induction N)
     case 0
     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
-      using `a \<in> F` by auto
+      using \<open>a \<in> F\<close> by auto
     then show ?case by auto
   next
     case (Suc N)
     define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
       where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"

       fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
       define y where "y = (\<lambda>i. if i = N then a else x i)"
       have "f (y, x N) = x"
         unfolding f_def y_def by auto
       moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
-        unfolding y_def using H `a \<in> F` by auto
+        unfolding y_def using H \<open>a \<in> F\<close> by auto
       ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
         by (metis (no_types, lifting) image_eqI)
     qed
     moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
       using Suc.IH assms(2) by auto

       unfolding pi_def g_def I_def using H by fastforce
     ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
       by auto
   qed
   then show ?thesis
-    using countable_nat_product_event_const[OF `b \<in> G` `countable G`]
+    using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
     by (meson countable_image countable_subset)
 qed
 
 instance "fun" :: (countable, first_countable_topology) first_countable_topology
 proof

     apply (rule choice) using first_countable_basis by auto
   then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
                                                   "\<And>x i. open (A x i)"
                                                   "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
     by metis
-  text {*$B i$ is a countable basis of neighborhoods of $x_i$.*}
+  text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
   define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
   have "countable (B i)" for i unfolding B_def by auto
 
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
   have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
     unfolding K_def B_def by auto
   then have "K \<noteq> {}" by auto
   have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using `\<And>i. countable (B i)` by auto
+    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have "countable K" by auto
   have "x \<in> k" if "k \<in> K" for k
     using that unfolding K_def B_def apply auto using A(1) by auto

     unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
 
   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
   proof -
     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
-      using `open U \<and> x \<in> U` unfolding open_fun_def by auto
+      using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
       unfolding topspace_euclidean open_openin by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"

 
     have "Y i \<subseteq> X i" for i
       apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
     then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
     then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
-    then show ?thesis using `Pi\<^sub>E UNIV Y \<in> K` by auto
+    then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
   qed
 
   show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
     apply (rule first_countableI[of K])
-    using `countable K` `\<And>k. k \<in> K \<Longrightarrow> x \<in> k` `\<And>k. k \<in> K \<Longrightarrow> open k` Inc by auto
+    using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
 qed
 
 lemma product_topology_countable_basis:
   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
           topological_basis K \<and> countable K \<and>

   have "open U" if "U \<in> B2" for U
     using that unfolding B2_def using B topological_basis_open by auto
 
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
   have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
-    unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
+    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
 
   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using `countable B2` by auto
+    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have ii: "countable K" by auto
 
   have iii: "topological_basis K"
   proof (rule topological_basisI)
     fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
     then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
       unfolding open_fun_def by auto
-    with product_topology_open_contains_basis[OF this `x \<in> U`]
+    with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
       unfolding topspace_euclidean open_openin by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"

       by auto
     then have "x i \<in> X i" for i by auto
     define I where "I = {i. X i \<noteq> UNIV}"
     define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
     have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
-      unfolding B2_def using B `open (X i)` `x i \<in> X i` by (meson UnCI topological_basisE)
+      unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
     have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
       using someI_ex[OF *]
       apply (cases "i \<in> I")
       unfolding Y_def using * apply (auto)
       unfolding B2_def I_def by auto

 
     have "x \<in> Pi\<^sub>E UNIV Y"
       using ** by auto
 
     show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
-      using `Pi\<^sub>E UNIV Y \<in> K` `Pi\<^sub>E UNIV Y \<subseteq> U` `x \<in> Pi\<^sub>E UNIV Y` by auto
+      using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
   next
     fix U assume "U \<in> K"
     show "open U"
-      using `U \<in> K` unfolding open_fun_def K_def apply (auto)
+      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
       apply (rule product_topology_basis)
-      using `\<And>V. V \<in> B2 \<Longrightarrow> open V` open_UNIV unfolding topspace_euclidean open_openin[symmetric]
+      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
       by auto
   qed
 
   show ?thesis using i ii iii by auto
 qed

 instance "fun" :: (countable, second_countable_topology) second_countable_topology
   apply standard
   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
 
-subsection {*The strong operator topology on continuous linear operators*}
-
-text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
+subsection \<open>The strong operator topology on continuous linear operators\<close>
+
+text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
 operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
 (the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
 
 However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
 $T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology

 Note that there is yet another (common and useful) topology on operator spaces, the weak operator
 topology, defined analogously using the product topology, but where the target space is given the
 weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
 canonical embedding of a space into its bidual. We do not define it there, although it could also be
 defined analogously.
-*}
+\<close>
 
 definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
 where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
 
 lemma strong_operator_topology_topspace:

     apply (rule continuous_on_topo_coordinatewise_then_product, auto)
     using * unfolding comp_def by auto
   show "continuous_on_topo T strong_operator_topology f"
     unfolding strong_operator_topology_def
     apply (rule continuous_on_topo_pullback')
-    by (auto simp add: `continuous_on_topo T euclidean (blinfun_apply o f)`)
+    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
 qed
 
 lemma strong_operator_topology_weaker_than_euclidean:
   "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
 by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
 
 
-subsection {*Metrics on product spaces*}
-
-
-text {*In general, the product topology is not metrizable, unless the index set is countable.
+subsection \<open>Metrics on product spaces\<close>
+
+
+text \<open>In general, the product topology is not metrizable, unless the index set is countable.
 When the index set is countable, essentially any (convergent) combination of the metrics on the
 factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
 for instance.
 
 What is not completely trivial is that the distance thus defined induces the same topology
 as the product topology. This is what we have to prove to show that we have an instance
 of \verb+metric_space+.
 
 The proofs below would work verbatim for general countable products of metric spaces. However,
 since distances are only implemented in terms of type classes, we only develop the theory
-for countable products of the same space.*}
+for countable products of the same space.\<close>
 
 instantiation "fun" :: (countable, metric_space) metric_space
 begin
 
 definition dist_fun_def:
   "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
 
 definition uniformity_fun_def:
   "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
 
-text {*Except for the first one, the auxiliary lemmas below are only useful when proving the
+text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
 instance: once it is proved, they become trivial consequences of the general theory of metric
 spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
-to do this.*}
+to do this.\<close>
 
 lemma dist_fun_le_dist_first_terms:
   "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
 proof -
   have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)

     using open_fun_def assms by auto
   obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
                     "\<And>i. openin euclidean (X i)"
                     "finite {i. X i \<noteq> topspace euclidean}"
                     "x \<in> Pi\<^sub>E UNIV X"
-    using product_topology_open_contains_basis[OF * `x \<in> U`] by auto
+    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
   define I where "I = {i. X i \<noteq> topspace euclidean}"
   have "finite I" unfolding I_def using H(3) by auto
   {
     fix i
-    have "x i \<in> X i" using `x \<in> U` H by auto
+    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
     then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
-      using `openin euclidean (X i)` open_openin open_contains_ball by blast
+      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
     then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
     define f where "f = min e (1/2)"
-    have "f>0" "f<1" unfolding f_def using `e>0` by auto
-    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using `ball (x i) e \<subseteq> X i` by auto
+    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
+    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
     ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
   } note * = this
   have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
     by (rule choice, auto simp add: *)
   then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
     by blast
   define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
   have "m > 0" if "I\<noteq>{}"
-    unfolding m_def apply (rule Min_grI) using `finite I` `I \<noteq> {}` `\<And>i. e i > 0` by auto
+    unfolding m_def apply (rule Min_grI) using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
   moreover have "{y. dist x y < m} \<subseteq> U"
   proof (auto)
     fix y assume "dist x y < m"
     have "y i \<in> X i" if "i \<in> I" for i
     proof -
       have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
       define n where "n = to_nat i"
       have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
-        using `dist x y < m` unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
+        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
       then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
-        using `n = to_nat i` by auto
+        using \<open>n = to_nat i\<close> by auto
       also have "... \<le> (1/2)^(to_nat i) * e i"
-        unfolding m_def apply (rule Min_le) using `finite I` `i \<in> I` by auto
+        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
       ultimately have "min (dist (x i) (y i)) 1 < e i"
         by (auto simp add: divide_simps)
       then have "dist (x i) (y i) < e i"
-        using `e i < 1` by auto
-      then show "y i \<in> X i" using `ball (x i) (e i) \<subseteq> X i` by auto
+        using \<open>e i < 1\<close> by auto
+      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
     qed
     then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
-    then show "y \<in> U" using `Pi\<^sub>E UNIV X \<subseteq> U` by auto
+    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
   qed
   ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
 
   have "U = UNIV" if "I = {}"
     using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)

   then have "\<And>i. openin euclidean (X i)"
     using open_openin by auto
   define U where "U = Pi\<^sub>E UNIV X"
   have "open U"
     unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
-    unfolding U_def using `\<And>i. openin euclidean (X i)` `finite {i. X i \<noteq> topspace euclidean}`
+    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
     by auto
   moreover have "x \<in> U"
     unfolding U_def X_def by (auto simp add: PiE_iff)
   moreover have "dist x y < e" if "y \<in> U" for y
   proof -
     have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
-      using `y \<in> U` unfolding U_def apply (auto simp add: PiE_iff)
+      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
       unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
     have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
       apply (rule Max.boundedI) using * by auto
 
     have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
       by (rule dist_fun_le_dist_first_terms)
     also have "... \<le> 2 * f + e / 8"
-      apply (rule add_mono) using ** `2^N > 8/e` by(auto simp add: algebra_simps divide_simps)
+      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
     also have "... \<le> e/2 + e/8"
       unfolding f_def by auto
     also have "... < e"
       by auto
     finally show "dist x y < e" by simp

   shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
 proof (auto)
   assume "open U"
   fix x assume "x \<in> U"
   then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
-    using open_fun_contains_ball_aux[OF `open U` `x \<in> U`] by auto
+    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
 next
   assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
   define K where "K = {V. open V \<and> V \<subseteq> U}"
   {
     fix x assume "x \<in> U"
     then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
     then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
-      using ball_fun_contains_open_aux[OF `e>0`, of x] by auto
+      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
     have "V \<in> K"
       unfolding K_def using e(2) V(1) V(3) by auto
-    then have "x \<in> (\<Union>K)" using `x \<in> V` by auto
+    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
   }
   then have "(\<Union>K) = U"
     unfolding K_def by auto
   moreover have "open (\<Union>K)"
     unfolding K_def by auto

 
 instance proof
   fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
   proof
     assume "x = y"
-    then show "dist x y = 0" unfolding dist_fun_def using `x = y` by auto
+    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
   next
     assume "dist x y = 0"
     have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
       by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
     have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
-      using `dist x y = 0` unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
+      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
     then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
       by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
                 zero_eq_1_divide_iff zero_neq_numeral)
     then have "x (from_nat n) = y (from_nat n)" for n
       by auto

       by (metis from_nat_to_nat)
     then show "x = y"
       by auto
   qed
 next
-  text{*The proof of the triangular inequality is trivial, modulo the fact that we are dealing
+  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
         with infinite series, hence we should justify the convergence at each step. In this
-        respect, the following simplification rule is extremely handy.*}
+        respect, the following simplification rule is extremely handy.\<close>
   have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
     by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
   fix x y z::"'a \<Rightarrow> 'b"
   {
     fix n

   also have "... = dist x z + dist y z"
     unfolding dist_fun_def by simp
   finally show "dist x y \<le> dist x z + dist y z"
     by simp
 next
-  text{*Finally, we show that the topology generated by the distance and the product
+  text\<open>Finally, we show that the topology generated by the distance and the product
         topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
         except that the condition to prove is expressed with filters. To deal with this,
         we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
-        \verb+Real_Vector_Spaces.thy+*}
+        \verb+Real_Vector_Spaces.thy+\<close>
   fix U::"('a \<Rightarrow> 'b) set"
   have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
   unfolding uniformity_fun_def apply (subst eventually_INF_base)
     by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
   then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
     unfolding fun_open_ball_aux by simp
 qed (simp add: uniformity_fun_def)
 
 end
 
-text {*Nice properties of spaces are preserved under countable products. In addition
+text \<open>Nice properties of spaces are preserved under countable products. In addition
 to first countability, second countability and metrizability, as we have seen above,
-completeness is also preserved, and therefore being Polish.*}
+completeness is also preserved, and therefore being Polish.\<close>
 
 instance "fun" :: (countable, complete_space) complete_space
 proof
   fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
   have "Cauchy (\<lambda>n. u n i)" for i
   unfolding cauchy_def proof (intro impI allI)
     fix e assume "e>(0::real)"
     obtain k where "i = from_nat k"
       using from_nat_to_nat[of i] by metis
-    have "(1/2)^k * min e 1 > 0" using `e>0` by auto
+    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
     then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
-      using `Cauchy u` unfolding cauchy_def by blast
+      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
     then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
       by blast
     have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
     proof (auto)
       fix m n::nat assume "m \<ge> N" "n \<ge> N"
       have "(1/2)^k * min (dist (u m i) (u n i)) 1
               = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
-        using `i = from_nat k` by auto
+        using \<open>i = from_nat k\<close> by auto
       also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
         apply (rule sum_le_suminf)
         by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
       also have "... = dist (u m) (u n)"
         unfolding dist_fun_def by auto
       also have "... < (1/2)^k * min e 1"
-        using C `m \<ge> N` `n \<ge> N` by auto
+        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
       finally have "min (dist (u m i) (u n i)) 1 < min e 1"
         by (auto simp add: algebra_simps divide_simps)
       then show "dist (u m i) (u n i) < e" by auto
     qed
     then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"

     have "dist (u k) x < e" if "k \<ge> L" for k
     proof -
       have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
       proof -
         have "K (from_nat n) \<le> L"
-          unfolding L_def apply (rule Max_ge) using `n \<le> N` by auto
-        then have "k \<ge> K (from_nat n)" using `k \<ge> L` by auto
+          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
+        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
         then show ?thesis using K less_imp_le by auto
       qed
       have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
         apply (rule Max.boundedI) using * by auto
       have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
         using dist_fun_le_dist_first_terms by auto
       also have "... \<le> 2 * e/4 + e/4"
         apply (rule add_mono)
-        using ** `2^N > 4/e` less_imp_le by (auto simp add: algebra_simps divide_simps)
+        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
       also have "... < e" by auto
       finally show ?thesis by simp
     qed
     then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
   qed

 
 instance "fun" :: (countable, polish_space) polish_space
 by standard
 
 
-subsection {*Measurability*}
-
-text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
+subsection \<open>Measurability\<close>
+
+text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
 generated by open sets in the product, and the product sigma algebra, countably generated by
 products of measurable sets along finitely many coordinates. The second one is defined and studied
 in \verb+Finite_Product_Measure.thy+.
 
 These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),

 only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
 the factor is countably generated).
 
 In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
 compare it with the product sigma algebra as explained above.
-*}
+\<close>
 
 lemma measurable_product_coordinates [measurable (raw)]:
   "(\<lambda>x. x i) \<in> measurable borel borel"
 by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
 

   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
     unfolding comp_def by auto
   then show ?thesis by simp
 qed
 
-text {*To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
 of the product sigma algebra that is more similar to the one we used above for the product
-topology.*}
+topology.\<close>
 
 lemma sets_PiM_finite:
   "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
         {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
 proof

     then have *: "X i \<in> sets (M i)" for i by simp
     define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
     have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
     define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
     have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
-      unfolding Y_def apply (rule sets_PiM_I) using `finite J` `J \<subseteq> I` * by auto
+      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
     moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
       unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
       by (auto simp add: PiE_iff, blast)
     ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
   qed

                 (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
     if "i \<in> I" "A \<in> sets (M i)" for i A
   proof -
     define X where "X = (\<lambda>j. if j = i then A else space (M j))"
     have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
-      unfolding X_def using sets.sets_into_space[OF `A \<in> sets (M i)`] `i \<in> I`
+      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
       by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
     moreover have "X j \<in> sets (M j)" for j
-      unfolding X_def using `A \<in> sets (M i)` by auto
+      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
     moreover have "finite {j. X j \<noteq> space (M j)}"
       unfolding X_def by simp
     ultimately show ?thesis by auto
   qed
   show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"

     define I where "I = {i. X i \<noteq> UNIV}"
     have "finite I" unfolding I_def using that by simp
     have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
       unfolding I_def by auto
     also have "... \<in> sets borel"
-      using that `finite I` by measurable
+      using that \<open>finite I\<close> by measurable
     finally show ?thesis by simp
   qed
   then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
     by auto
   then show ?thesis unfolding sets_PiM_finite space_borel

             "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     using product_topology_countable_basis by fast
   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   proof -
     obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
-      using K(3)[OF `k \<in> K`] by blast
+      using K(3)[OF \<open>k \<in> K\<close>] by blast
     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
   qed
   have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
   proof -
     obtain B where "B \<subseteq> K" "U = (\<Union>B)"
-      using `open U` `topological_basis K` by (metis topological_basis_def)
-    have "countable B" using `B \<subseteq> K` `countable K` countable_subset by blast
+      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
+    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
     moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
-      using `B \<subseteq> K` * that by auto
-    ultimately show ?thesis unfolding `U = (\<Union>B)` by auto
+      using \<open>B \<subseteq> K\<close> * that by auto
+    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
   qed
   have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
     apply (rule sets.sigma_sets_subset') using ** by auto
   then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
     unfolding borel_def by auto