--- a/src/HOL/Analysis/Function_Topology.thy Thu Jan 17 16:08:41 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Jan 17 16:22:21 2019 -0500
@@ -61,8 +61,6 @@
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>
@@ -80,14 +78,14 @@
| 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 istopology_generate_topology_on:
+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 \<open>S\<close> is that it is the
smallest topology containing all the elements of \<open>S\<close>:\<close>
-lemma generate_topology_on_coarsest:
+lemma%unimportant generate_topology_on_coarsest:
assumes "istopology T"
"\<And>s. s \<in> S \<Longrightarrow> T s"
"generate_topology_on S s0"
@@ -98,17 +96,17 @@
abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
-lemma openin_topology_generated_by_iff:
+lemma%unimportant openin_topology_generated_by_iff:
"openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
-lemma openin_topology_generated_by:
+lemma%unimportant openin_topology_generated_by:
"openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
using openin_topology_generated_by_iff by auto
-lemma topology_generated_by_topspace:
+lemma%important topology_generated_by_topspace:
"topspace (topology_generated_by S) = (\<Union>S)"
-proof
+proof%unimportant
{
fix s assume "openin (topology_generated_by S) s"
then have "generate_topology_on S s" by (rule openin_topology_generated_by)
@@ -123,9 +121,9 @@
unfolding topspace_def using openin_topology_generated_by_iff by auto
qed
-lemma topology_generated_by_Basis:
+lemma%important 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)
+by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
lemma generate_topology_on_Inter:
"\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
@@ -268,28 +266,28 @@
where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
\<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
-lemma continuous_on_continuous_on_topo:
+lemma%important continuous_on_continuous_on_topo:
"continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
- unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
+unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
topspace_euclidean_subtopology open_openin topspace_euclidean by fast
-lemma continuous_on_topo_UNIV:
+lemma%unimportant continuous_on_topo_UNIV:
"continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
-lemma continuous_on_topo_open [intro]:
+lemma%important continuous_on_topo_open [intro]:
"continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
- unfolding continuous_on_topo_def by auto
+unfolding%unimportant continuous_on_topo_def by auto
-lemma continuous_on_topo_topspace [intro]:
+lemma%unimportant continuous_on_topo_topspace [intro]:
"continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
unfolding continuous_on_topo_def by auto
-lemma continuous_on_generated_topo_iff:
+lemma%important continuous_on_generated_topo_iff:
"continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
unfolding continuous_on_topo_def topology_generated_by_topspace
-proof (auto simp add: topology_generated_by_Basis)
+proof%unimportant (auto simp add: topology_generated_by_Basis)
assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
fix U assume "openin (topology_generated_by S) U"
then have "generate_topology_on S U" by (rule openin_topology_generated_by)
@@ -311,17 +309,17 @@
qed (auto simp add: H)
qed
-lemma continuous_on_generated_topo:
+lemma%important continuous_on_generated_topo:
assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
"f`(topspace T1) \<subseteq> (\<Union> S)"
shows "continuous_on_topo T1 (topology_generated_by S) f"
- using assms continuous_on_generated_topo_iff by blast
+using%unimportant assms continuous_on_generated_topo_iff by blast
-proposition continuous_on_topo_compose:
+lemma%important continuous_on_topo_compose:
assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
shows "continuous_on_topo T1 T3 (g o f)"
- using assms unfolding continuous_on_topo_def
-proof (auto)
+using%unimportant assms unfolding continuous_on_topo_def
+proof%unimportant (auto)
fix U :: "'c set"
assume H: "openin T3 U"
have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
@@ -332,7 +330,7 @@
by simp
qed (blast)
-lemma continuous_on_topo_preimage_topspace [intro]:
+lemma%unimportant continuous_on_topo_preimage_topspace [intro]:
assumes "continuous_on_topo T1 T2 f"
shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
using assms unfolding continuous_on_topo_def by auto
@@ -351,9 +349,9 @@
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 istopology_pullback_topology:
+lemma%important istopology_pullback_topology:
"istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
- unfolding istopology_def proof (auto)
+unfolding%unimportant istopology_def proof (auto)
fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
by (rule bchoice)
@@ -364,19 +362,19 @@
then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
qed
-lemma openin_pullback_topology:
+lemma%unimportant openin_pullback_topology:
"openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
-lemma topspace_pullback_topology:
+lemma%unimportant topspace_pullback_topology:
"topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
by (auto simp add: topspace_def openin_pullback_topology)
-proposition continuous_on_topo_pullback [intro]:
+lemma%important continuous_on_topo_pullback [intro]:
assumes "continuous_on_topo T1 T2 g"
shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
unfolding continuous_on_topo_def
-proof (auto)
+proof%unimportant (auto)
fix U::"'b set" assume "openin T2 U"
then have "openin T1 (g-`U \<inter> topspace T1)"
using assms unfolding continuous_on_topo_def by auto
@@ -396,11 +394,11 @@
using assms unfolding continuous_on_topo_def by auto
qed
-proposition continuous_on_topo_pullback' [intro]:
+lemma%important continuous_on_topo_pullback' [intro]:
assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
shows "continuous_on_topo T1 (pullback_topology A f T2) g"
unfolding continuous_on_topo_def
-proof (auto)
+proof%unimportant (auto)
fix U assume "openin (pullback_topology A f T2) U"
then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
unfolding openin_pullback_topology by auto
@@ -549,9 +547,9 @@
done
qed
-lemma topspace_product_topology:
+lemma%important topspace_product_topology:
"topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
-proof
+proof%unimportant
show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
unfolding product_topology_def topology_generated_by_topspace
unfolding topspace_def by auto
@@ -561,16 +559,16 @@
unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
qed
-lemma product_topology_basis:
+lemma%unimportant product_topology_basis:
assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
unfolding product_topology_def
by (rule topology_generated_by_Basis) (use assms in auto)
-proposition product_topology_open_contains_basis:
+lemma%important product_topology_open_contains_basis:
assumes "openin (product_topology T I) U" "x \<in> U"
shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
-proof -
+proof%unimportant -
have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
@@ -719,7 +717,7 @@
text \<open>The basic property of the product topology is the continuity of projections:\<close>
-lemma continuous_on_topo_product_coordinates [simp]:
+lemma%unimportant continuous_on_topo_product_coordinates [simp]:
assumes "i \<in> I"
shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
proof -
@@ -741,12 +739,12 @@
by (auto simp add: assms topspace_product_topology PiE_iff)
qed
-lemma continuous_on_topo_coordinatewise_then_product [intro]:
+lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
shows "continuous_on_topo T1 (product_topology T I) f"
unfolding product_topology_def
-proof (rule continuous_on_generated_topo)
+proof%unimportant (rule continuous_on_generated_topo)
fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
by blast
@@ -774,7 +772,7 @@
using assms unfolding continuous_on_topo_def by auto
qed
-lemma continuous_on_topo_product_then_coordinatewise [intro]:
+lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:
assumes "continuous_on_topo T1 (product_topology T I) f"
shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
@@ -796,7 +794,7 @@
using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed
-lemma continuous_on_restrict:
+lemma%unimportant continuous_on_restrict:
assumes "J \<subseteq> I"
shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
proof (rule continuous_on_topo_coordinatewise_then_product)
@@ -819,7 +817,7 @@
definition%important open_fun_def:
"open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
-instance proof
+instance proof%unimportant
have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
unfolding topspace_product_topology topspace_euclidean by auto
then show "open (UNIV::('a \<Rightarrow> 'b) set)"
@@ -828,15 +826,15 @@
end
-lemma euclidean_product_topology:
+lemma%unimportant euclidean_product_topology:
"euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
by (metis open_openin topology_eq open_fun_def)
-proposition product_topology_basis':
+lemma%important product_topology_basis':
fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
-proof -
+proof%unimportant -
define J where "J = x`I"
define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
@@ -866,24 +864,24 @@
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]:
+lemma%unimportant continuous_on_product_coordinates [simp]:
"continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
unfolding continuous_on_topo_UNIV euclidean_product_topology
by (rule continuous_on_topo_product_coordinates, simp)
-lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:
assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
shows "continuous_on UNIV f"
using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
by (rule continuous_on_topo_coordinatewise_then_product, simp)
-lemma continuous_on_product_then_coordinatewise:
+lemma%unimportant continuous_on_product_then_coordinatewise:
assumes "continuous_on UNIV f"
shows "continuous_on UNIV (\<lambda>x. f x i)"
using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
-lemma continuous_on_product_coordinatewise_iff:
+lemma%unimportant continuous_on_product_coordinatewise_iff:
"continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
by (auto intro: continuous_on_product_then_coordinatewise)
@@ -893,7 +891,7 @@
of product spaces, but they have more to do with countability and could
be put in the corresponding theory.\<close>
-lemma countable_nat_product_event_const:
+lemma%unimportant countable_nat_product_event_const:
fixes F::"'a set" and a::'a
assumes "a \<in> F" "countable F"
shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
@@ -930,7 +928,7 @@
then show ?thesis using countable_subset[OF *] by auto
qed
-lemma countable_product_event_const:
+lemma%unimportant countable_product_event_const:
fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
assumes "\<And>i. countable (F i)"
shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
@@ -963,7 +961,7 @@
qed
instance "fun" :: (countable, first_countable_topology) first_countable_topology
-proof
+proof%unimportant
fix x::"'a \<Rightarrow> 'b"
have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
apply (rule choice) using first_countable_basis by auto
@@ -1035,11 +1033,11 @@
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
-proposition product_topology_countable_basis:
+lemma%important product_topology_countable_basis:
shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
topological_basis K \<and> countable K \<and>
(\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
-proof -
+proof%unimportant -
obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
using ex_countable_basis by auto
then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
@@ -1142,15 +1140,15 @@
definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
-lemma strong_operator_topology_topspace:
+lemma%unimportant strong_operator_topology_topspace:
"topspace strong_operator_topology = UNIV"
unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
-lemma strong_operator_topology_basis:
+lemma%important strong_operator_topology_basis:
fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
-proof -
+proof%unimportant -
have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
by (rule product_topology_basis'[OF assms])
moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
@@ -1160,16 +1158,16 @@
unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
qed
-lemma strong_operator_topology_continuous_evaluation:
+lemma%important strong_operator_topology_continuous_evaluation:
"continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
-proof -
+proof%unimportant -
have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
then show ?thesis unfolding comp_def by simp
qed
-lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:
"continuous_on_topo T strong_operator_topology f
\<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
proof (auto)
@@ -1192,9 +1190,9 @@
by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
qed
-lemma strong_operator_topology_weaker_than_euclidean:
+lemma%important 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,
+by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
@@ -1228,9 +1226,9 @@
spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
to do this.\<close>
-lemma dist_fun_le_dist_first_terms:
+lemma%important dist_fun_le_dist_first_terms:
"dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
-proof -
+proof%unimportant -
have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
= (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
by (rule suminf_cong, simp add: power_add)
@@ -1278,7 +1276,7 @@
finally show ?thesis unfolding M_def by simp
qed
-lemma open_fun_contains_ball_aux:
+lemma%unimportant open_fun_contains_ball_aux:
assumes "open (U::(('a \<Rightarrow> 'b) set))"
"x \<in> U"
shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
@@ -1341,7 +1339,7 @@
then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
qed
-lemma ball_fun_contains_open_aux:
+lemma%unimportant ball_fun_contains_open_aux:
fixes x::"('a \<Rightarrow> 'b)" and e::real
assumes "e>0"
shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
@@ -1388,7 +1386,7 @@
ultimately show ?thesis by auto
qed
-lemma fun_open_ball_aux:
+lemma%unimportant fun_open_ball_aux:
fixes U::"('a \<Rightarrow> 'b) set"
shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
proof (auto)
@@ -1577,7 +1575,7 @@
-subsection%important \<open>Measurability\<close> (*FIX ME move? *)
+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
@@ -1595,11 +1593,11 @@
compare it with the product sigma algebra as explained above.
\<close>
-lemma measurable_product_coordinates [measurable (raw)]:
+lemma%unimportant measurable_product_coordinates [measurable (raw)]:
"(\<lambda>x. x i) \<in> measurable borel borel"
by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
-lemma measurable_product_then_coordinatewise:
+lemma%unimportant measurable_product_then_coordinatewise:
fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
assumes [measurable]: "f \<in> borel_measurable M"
shows "(\<lambda>x. f x i) \<in> borel_measurable M"
@@ -1613,10 +1611,10 @@
of the product sigma algebra that is more similar to the one we used above for the product
topology.\<close>
-lemma sets_PiM_finite:
+lemma%important sets_PiM_finite:
"sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
-proof
+proof%unimportant
have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
proof (auto)
fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
@@ -1656,9 +1654,9 @@
done
qed
-lemma sets_PiM_subset_borel:
+lemma%important sets_PiM_subset_borel:
"sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
-proof -
+proof%unimportant -
have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
proof -
define I where "I = {i. X i \<noteq> UNIV}"
@@ -1675,9 +1673,9 @@
by (simp add: * sets.sigma_sets_subset')
qed
-proposition sets_PiM_equal_borel:
+lemma%important sets_PiM_equal_borel:
"sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
-proof
+proof%unimportant
obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
"\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
using product_topology_countable_basis by fast
@@ -1702,11 +1700,11 @@
unfolding borel_def by auto
qed (simp add: sets_PiM_subset_borel)
-lemma measurable_coordinatewise_then_product:
+lemma%important measurable_coordinatewise_then_product:
fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
shows "f \<in> borel_measurable M"
-proof -
+proof%unimportant -
have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
by (rule measurable_PiM_single', auto simp add: assms)
then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast