src/HOL/Analysis/Function_Topology.thy

 topology, even when the product is not finite (or even countable).
 
 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,

   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:
+lemma 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%unimportant generate_topology_on_coarsest:
+lemma generate_topology_on_coarsest:
   assumes "istopology T"
           "\<And>s. s \<in> S \<Longrightarrow> T s"
           "generate_topology_on S s0"
   shows "T s0"
 using assms(3) apply (induct rule: generate_topology_on.induct)
 using assms(1) assms(2) unfolding istopology_def by auto
 
 abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
 
-lemma%unimportant openin_topology_generated_by_iff:
+lemma 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%unimportant openin_topology_generated_by:
+lemma 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%important topology_generated_by_topspace:
+lemma topology_generated_by_topspace:
   "topspace (topology_generated_by S) = (\<Union>S)"
-proof%unimportant
+proof
   {
     fix s assume "openin (topology_generated_by S) s"
     then have "generate_topology_on S s" by (rule openin_topology_generated_by)
     then have "s \<subseteq> (\<Union>S)" by (induct, auto)
   }

     using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
   then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
     unfolding topspace_def using openin_topology_generated_by_iff by auto
 qed
 
-lemma%important topology_generated_by_Basis:
+lemma topology_generated_by_Basis:
   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
-by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
+  by (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>)"
   by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
 

 
 definition%important 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)))"
 
-lemma%important continuous_on_continuous_on_topo:
+lemma continuous_on_continuous_on_topo:
   "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
-unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
+  unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
 topspace_euclidean_subtopology open_openin topspace_euclidean by fast
 
-lemma%unimportant continuous_on_topo_UNIV:
+lemma 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%important continuous_on_topo_open [intro]:
+lemma continuous_on_topo_open [intro]:
   "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
-unfolding%unimportant continuous_on_topo_def by auto
-
-lemma%unimportant continuous_on_topo_topspace [intro]:
+  unfolding continuous_on_topo_def by auto
+
+lemma 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%important continuous_on_generated_topo_iff:
+lemma 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%unimportant (auto simp add: topology_generated_by_Basis)
+proof (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)
   then show "openin T1 (f -` U \<inter> topspace T1)"
   proof (induct)

     moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
     ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
   qed (auto simp add: H)
 qed
 
-lemma%important continuous_on_generated_topo:
+lemma 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%unimportant assms continuous_on_generated_topo_iff by blast
-
-lemma%important continuous_on_topo_compose:
+  using assms continuous_on_generated_topo_iff by blast
+
+proposition 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%unimportant assms unfolding continuous_on_topo_def
-proof%unimportant (auto)
+  using assms unfolding continuous_on_topo_def
+proof (auto)
   fix U :: "'c set"
   assume H: "openin T3 U"
   have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
     using H assms by blast
   moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
     using H assms continuous_on_topo_topspace by fastforce
   ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
     by simp
 qed (blast)
 
-lemma%unimportant continuous_on_topo_preimage_topspace [intro]:
+lemma 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
 
 

 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:
+lemma istopology_pullback_topology:
   "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
-unfolding%unimportant istopology_def proof (auto)
+  unfolding 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)
   then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
     by blast
   define V where "V = (\<Union>S\<in>K. U S)"
   have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
   then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
 qed
 
-lemma%unimportant openin_pullback_topology:
+lemma 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%unimportant topspace_pullback_topology:
+lemma topspace_pullback_topology:
   "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
 by (auto simp add: topspace_def openin_pullback_topology)
 
-lemma%important continuous_on_topo_pullback [intro]:
+proposition 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%unimportant (auto)
+proof (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
   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

     unfolding topspace_pullback_topology by auto
   then show "g (f x) \<in> topspace T2"
     using assms unfolding continuous_on_topo_def by auto
 qed
 
-lemma%important continuous_on_topo_pullback' [intro]:
+proposition 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%unimportant (auto)
+proof (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
   then obtain V where "openin T2 V" "U = f-`V \<inter> A"
     by blast

     apply (rule arg_cong [where f = "(union_of)arbitrary"])
     apply (force simp: *)
     done
 qed
 
-lemma%important topspace_product_topology:
+lemma topspace_product_topology:
   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
-proof%unimportant
+proof
   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
   have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
     using openin_topspace not_finite_existsD by auto
   then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
     unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
 qed
 
-lemma%unimportant product_topology_basis:
+lemma 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)
 
-lemma%important product_topology_open_contains_basis:
+proposition 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%unimportant -
+proof -
   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"
   proof induction
     case (Int U V x)

   done
 
 
 text \<open>The basic property of the product topology is the continuity of projections:\<close>
 
-lemma%unimportant continuous_on_topo_product_coordinates [simp]:
+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"

   }
   then show ?thesis unfolding continuous_on_topo_def
     by (auto simp add: assms topspace_product_topology PiE_iff)
 qed
 
-lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
+lemma 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%unimportant (rule continuous_on_generated_topo)
+proof (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
   define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
   have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto

     apply (simp only: topspace_product_topology)
     apply (auto simp add: PiE_iff)
     using assms unfolding continuous_on_topo_def by auto
 qed
 
-lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:
+lemma 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"
 proof -
   fix i assume "i \<in> I"

     using topspace_product_topology by metis
   then show "f x i = undefined"
     using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
 qed
 
-lemma%unimportant continuous_on_restrict:
+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

 begin
 
 definition%important open_fun_def:
   "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
 
-instance proof%unimportant
+instance proof
   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)"
     unfolding open_fun_def by (metis openin_topspace)
 qed (auto simp add: open_fun_def)
 
 end
 
-lemma%unimportant euclidean_product_topology:
+lemma euclidean_product_topology:
   "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
 by (metis open_openin topology_eq open_fun_def)
 
-lemma%important product_topology_basis':
+proposition 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%unimportant -
+proof -
   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)"
   have *: "open (X i)" for i
     unfolding X_def V_def using assms by auto

 qed
 
 text \<open>The results proved in the general situation of products of possibly different
 spaces have their counterparts in this simpler setting.\<close>
 
-lemma%unimportant continuous_on_product_coordinates [simp]:
+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%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+lemma 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%unimportant continuous_on_product_then_coordinatewise:
+lemma 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%unimportant continuous_on_product_coordinatewise_iff:
+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%important \<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.\<close>
 
-lemma%unimportant countable_nat_product_event_const:
+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}}"
 proof -
   have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}

       by (meson countable_image countable_subset)
   qed
   then show ?thesis using countable_subset[OF *] by auto
 qed
 
-lemma%unimportant countable_product_event_const:
+lemma 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})}"
 proof -
   define G where "G = (\<Union>i. F i) \<union> {b}"

     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%unimportant
+proof
   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
   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)"

   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 \<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%important product_topology_countable_basis:
+proposition 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%unimportant -
+proof -
   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)
   define B2 where "B2 = B \<union> {UNIV}"
   have "countable B2"

 \<close>
 
 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%unimportant strong_operator_topology_topspace:
+lemma strong_operator_topology_topspace:
   "topspace strong_operator_topology = UNIV"
 unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
 
-lemma%important strong_operator_topology_basis:
+lemma 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%unimportant -
+proof -
   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}
                 = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
     by auto
   ultimately show ?thesis
     unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
 qed
 
-lemma%important strong_operator_topology_continuous_evaluation:
+lemma strong_operator_topology_continuous_evaluation:
   "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
-proof%unimportant -
+proof -
   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%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:
+lemma 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)
   fix x::"'b"
   assume "continuous_on_topo T strong_operator_topology f"

     unfolding strong_operator_topology_def
     apply (rule continuous_on_topo_pullback')
     by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
 qed
 
-lemma%important strong_operator_topology_weaker_than_euclidean:
+lemma strong_operator_topology_weaker_than_euclidean:
   "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
-by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
 
 
 subsection%important \<open>Metrics on product spaces\<close>
 

 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.\<close>
 
-lemma%important dist_fun_le_dist_first_terms:
+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%unimportant -
+proof -
   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)
   also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
     apply (rule suminf_mult)

   also have "... \<le> 2 * M + (1/2)^N"
     using * ** by auto
   finally show ?thesis unfolding M_def by simp
 qed
 
-lemma%unimportant open_fun_contains_ball_aux:
+lemma 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"
 proof -
   have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"

     using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
   then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
   then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
 qed
 
-lemma%unimportant ball_fun_contains_open_aux:
+lemma 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}"
 proof -
   have "\<exists>N::nat. 2^N > 8/e"

     finally show "dist x y < e" by simp
   qed
   ultimately show ?thesis by auto
 qed
 
-lemma%unimportant fun_open_ball_aux:
+lemma 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)
   assume "open U"
   fix x assume "x \<in> U"

 by standard
 
 
 
 
-subsection%important \<open>Measurability\<close> (*FIX ME mv *)
+subsection%important \<open>Measurability\<close> (*FIX ME move? *)
 
 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 \<^file>\<open>Finite_Product_Measure.thy\<close>.

 
 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%unimportant measurable_product_coordinates [measurable (raw)]:
+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])
 
-lemma%unimportant measurable_product_then_coordinatewise:
+lemma 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"
 proof -
   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"

 
 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.\<close>
 
-lemma%important sets_PiM_finite:
+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%unimportant
+proof
   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)}"
     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)}"

     apply (rule sigma_sets_mono')
     apply (auto simp add: PiE_iff *)
     done
 qed
 
-lemma%important sets_PiM_subset_borel:
+lemma sets_PiM_subset_borel:
   "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
-proof%unimportant -
+proof -
   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}"
     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"

     by auto
   then show ?thesis unfolding sets_PiM_finite space_borel
     by (simp add: * sets.sigma_sets_subset')
 qed
 
-lemma%important sets_PiM_equal_borel:
+proposition sets_PiM_equal_borel:
   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
-proof%unimportant
+proof
   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
   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   proof -

     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
 qed (simp add: sets_PiM_subset_borel)
 
-lemma%important measurable_coordinatewise_then_product:
+lemma 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%unimportant -
+proof -
   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
 qed