--- a/src/HOL/Analysis/Function_Topology.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Tue Jan 17 13:59:10 2017 +0100
@@ -7,9 +7,9 @@
begin
-section {*Product topology*}
+section \<open>Product topology\<close>
-text {*We want to define the product topology.
+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
@@ -60,18 +60,18 @@
topology, even when the product is not finite (or even countable).
I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
-*}
+\<close>
-subsection {*Topology without type classes*}
+subsection \<open>Topology without type classes\<close>
-subsubsection {*The topology generated by some (open) subsets*}
+subsubsection \<open>The topology generated by some (open) subsets\<close>
-text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
+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 {}"
@@ -83,8 +83,8 @@
"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"
@@ -127,10 +127,10 @@
"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*}
+subsubsection \<open>Continuity\<close>
-text {*We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.*}
+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)))
@@ -206,15 +206,15 @@
using assms unfolding continuous_on_topo_def by auto
-subsubsection {*Pullback topology*}
+subsubsection \<open>Pullback topology\<close>
-text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
+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.*}
+by pulling back the product topology on the space of all functions.\<close>
-text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
-the set $A$.*}
+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)"
@@ -253,7 +253,7 @@
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
@@ -281,23 +281,23 @@
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*}
+subsection \<open>The product topology\<close>
-text {*We can now define the product topology, as generated by
+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
@@ -306,14 +306,14 @@
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))"
@@ -367,15 +367,15 @@
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
+ then show ?thesis using \<open>x \<in> U\<close> by auto
qed
-text {*The basic property of the product topology is the continuity of projections:*}
+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"
@@ -385,10 +385,10 @@
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)
@@ -417,11 +417,11 @@
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)}}"
@@ -441,17 +441,17 @@
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:
@@ -461,7 +461,7 @@
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"
@@ -469,7 +469,7 @@
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
@@ -521,8 +521,8 @@
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))"
@@ -545,11 +545,11 @@
"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*}
+subsubsection \<open>Topological countability for product spaces\<close>
-text {*The next two lemmas are useful to prove first or second countability
+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
@@ -563,7 +563,7 @@
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)
@@ -576,7 +576,7 @@
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
@@ -616,7 +616,7 @@
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
@@ -629,7 +629,7 @@
"\<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
@@ -638,7 +638,7 @@
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
@@ -652,7 +652,7 @@
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
@@ -685,12 +685,12 @@
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:
@@ -709,10 +709,10 @@
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
@@ -722,7 +722,7 @@
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)"
@@ -734,7 +734,7 @@
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")
@@ -758,13 +758,13 @@
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
@@ -776,9 +776,9 @@
using product_topology_countable_basis topological_basis_imp_subbasis by auto
-subsection {*The strong operator topology on continuous linear operators*}
+subsection \<open>The strong operator topology on continuous linear operators\<close>
-text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
+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+).
@@ -795,7 +795,7 @@
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"
@@ -847,7 +847,7 @@
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:
@@ -856,10 +856,10 @@
auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
-subsection {*Metrics on product spaces*}
+subsection \<open>Metrics on product spaces\<close>
-text {*In general, the product topology is not metrizable, unless the index set is countable.
+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.
@@ -870,7 +870,7 @@
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
@@ -881,10 +881,10 @@
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"
@@ -947,18 +947,18 @@
"\<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"
@@ -967,7 +967,7 @@
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"
@@ -977,19 +977,19 @@
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
@@ -1021,14 +1021,14 @@
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
@@ -1036,7 +1036,7 @@
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"
@@ -1053,7 +1053,7 @@
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}"
@@ -1061,10 +1061,10 @@
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
@@ -1077,13 +1077,13 @@
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)
@@ -1095,9 +1095,9 @@
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"
@@ -1134,11 +1134,11 @@
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)
@@ -1149,9 +1149,9 @@
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
@@ -1161,9 +1161,9 @@
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"
@@ -1171,14 +1171,14 @@
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
@@ -1210,8 +1210,8 @@
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"
@@ -1220,7 +1220,7 @@
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
@@ -1233,9 +1233,9 @@
by standard
-subsection {*Measurability*}
+subsection \<open>Measurability\<close>
-text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
+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+.
@@ -1249,7 +1249,7 @@
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"
@@ -1265,9 +1265,9 @@
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))
@@ -1281,7 +1281,7 @@
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)
@@ -1297,10 +1297,10 @@
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
@@ -1322,7 +1322,7 @@
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"
@@ -1340,17 +1340,17 @@
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