src/HOL/Analysis/Function_Topology.thy

 the sets which are products of open sets along finitely many coordinates, and the whole
 space along the other coordinates. This is the coarsest topology for which the projection
 to each factor is continuous.
 
 To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
-'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
-coordinate belongs to $X\;i$ for all $i \in I$.
+'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from \<open>'i\<close> to \<open>'a\<close> such that the \<open>i\<close>-th
+coordinate belongs to \<open>X i\<close> for all \<open>i \<in> I\<close>.
 
 Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
 This means that type classes can not be used to define such a product if one wants to take the
 product of different topological spaces (as the type 'a can only be given one structure of
 topological space using type classes). On the other hand, one can define different topologies (as
-introduced in \verb+thy+) on one type, and these topologies do not need to
+introduced in \<open>thy\<close>) on one type, and these topologies do not need to
 share the same maximal open set. Hence, one can form a product of topologies in this sense, and
 this works well. The big caveat is that it does not interact well with the main body of
 topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
 is not defined in this setting.
 

 of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
 type classes as consequences of more general statements in terms of topologies (but I am
 probably too naive here).
 
 Here is an example of a reformulation using topologies. Let
-\begin{verbatim}
-continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
-                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
-\end{verbatim}
-be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
-the current \verb+continuous_on+ (with type classes) can be redefined as
-\begin{verbatim}
-continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
-\end{verbatim}
-
-In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
-for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
-the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
+@{text [display]
+\<open>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)))\<close>}
+be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
+the current \<open>continuous_on\<close> (with type classes) can be redefined as
+@{text [display] \<open>continuous_on s f =
+    continuous_on_topo (subtopology euclidean s) (topology euclidean) f\<close>}
+
+In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
+for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
+the above equivalence in Lemma~\<open>continuous_on_continuous_on_topo\<close>.
 
 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+.
+I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
 \<close>
 
 subsection%important \<open>Topology without type classes\<close>
 
 subsubsection%important \<open>The topology generated by some (open) subsets\<close>
 
 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
-as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
+as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
 and is never a problem in proofs, so I prefer to write it down explicitly.
 
-We do not require UNIV to be an open set, as this will not be the case in applications. (We are
-thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
+We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
+thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> 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)"
+  Empty: "generate_topology_on S {}"
+| Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
 | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
 
 lemma%unimportant istopology_generate_topology_on:
   "istopology (generate_topology_on S)"
 unfolding istopology_def by (auto intro: generate_topology_on.intros)
 
-text \<open>The basic property of the topology generated by a set $S$ is that it is the
-smallest topology containing all the elements of $S$:\<close>
+text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
+smallest topology containing all the elements of \<open>S\<close>:\<close>
 
 lemma%unimportant generate_topology_on_coarsest:
   assumes "istopology T"
           "\<And>s. s \<in> S \<Longrightarrow> T s"
           "generate_topology_on S s0"

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

 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.
+point, equal to \<open>undefined\<close> along all coordinates.
 
 So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
 \<close>
 
 definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"

     apply (rule choice) using first_countable_basis by auto
   then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
                                                   "\<And>x i. open (A x i)"
                                                   "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
     by metis
-  text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
+  text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<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"

   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
 
 subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
 
-text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
-operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
-(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
-
-However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
-$T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
-where the target space is endowed with the norm topology. It is especially useful when 'b is the set
+text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
+operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
+
+However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
+\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
 of real numbers, since then this topology is compact.
 
 We can not implement it using type classes as there is already a topology, but at least we
 can define it as a topology.
 

 subsection%important \<open>Metrics on product spaces\<close>
 
 
 text \<open>In general, the product topology is not metrizable, unless the index set is countable.
 When the index set is countable, essentially any (convergent) combination of the metrics on the
-factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
+factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
 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+.
+of \<^class>\<open>metric_space\<close>.
 
 The proofs below would work verbatim for general countable products of metric spaces. However,
 since distances are only implemented in terms of type classes, we only develop the theory
 for countable products of the same space.\<close>
 

     unfolding dist_fun_def by simp
   finally show "dist x y \<le> dist x z + dist y z"
     by simp
 next
   text\<open>Finally, we show that the topology generated by the distance and the product
-        topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
+        topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
         except that the condition to prove is expressed with filters. To deal with this,
-        we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
-        \verb+Real_Vector_Spaces.thy+\<close>
+        we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
+        \<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<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)"

 subsection%important \<open>Measurability\<close> (*FIX ME mv *)
 
 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
 generated by open sets in the product, and the product sigma algebra, countably generated by
 products of measurable sets along finitely many coordinates. The second one is defined and studied
-in \verb+Finite_Product_Measure.thy+.
+in \<^file>\<open>Finite_Product_Measure.thy\<close>.
 
 These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
 but there is a fundamental difference: open sets are generated by arbitrary unions, not only
 countable ones, so typically many open sets will not be measurable with respect to the product sigma
 algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide