diff -r 7414ce0256e1 -r fde093888c16 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Aug 28 13:28:39 2018 +0100
@@ -7,7 +7,7 @@
 begin
 
 
-section \<open>Product topology\<close>
+section%important \<open>Product topology\<close>
 
 text \<open>We want to define the product topology.
 
@@ -62,9 +62,9 @@
 I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
 \<close>
 
-subsection \<open>Topology without type classes\<close>
+subsection%important \<open>Topology without type classes\<close>
 
-subsubsection \<open>The topology generated by some (open) subsets\<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,
@@ -79,14 +79,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 $S$ is that it is the
 smallest topology containing all the elements of $S$:\<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"
@@ -94,21 +94,21 @@
 using assms(3) apply (induct rule: generate_topology_on.induct)
 using assms(1) assms(2) unfolding istopology_def by auto
 
-definition topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+definition%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
   where "topology_generated_by S = 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]]
 unfolding topology_generated_by_def 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,41 +123,41 @@
     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)
 
-subsubsection \<open>Continuity\<close>
+subsubsection%important \<open>Continuity\<close>
 
 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
 of type classes, as defined below.\<close>
 
-definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+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 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)
@@ -179,17 +179,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
 
-lemma 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)"
@@ -200,13 +200,13 @@
     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
 
 
-subsubsection \<open>Pullback topology\<close>
+subsubsection%important \<open>Pullback topology\<close>
 
 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
 a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -216,12 +216,12 @@
 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)"
+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)
@@ -232,19 +232,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)
 
-lemma 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
@@ -264,11 +264,11 @@
     using assms unfolding continuous_on_topo_def by auto
 qed
 
-lemma 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
@@ -295,7 +295,7 @@
 qed
 
 
-subsection \<open>The product topology\<close>
+subsection%important \<open>The product topology\<close>
 
 text \<open>We can now define the product topology, as generated by
 the sets which are products of open sets along finitely many coordinates, and the whole
@@ -308,16 +308,16 @@
 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)"
+definition%important 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 \<open>The total set of the product topology is the product of the total sets
 along each coordinate.\<close>
 
-lemma product_topology_topspace:
+lemma%important product_topology_topspace:
   "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 apply (simp only: topology_generated_by_topspace)
     unfolding topspace_def by auto
@@ -327,16 +327,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 apply (rule topology_generated_by_Basis) using assms by auto
 
-lemma 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"
@@ -377,7 +377,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 -
@@ -399,12 +399,12 @@
     by (auto simp add: assms product_topology_topspace 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
@@ -432,7 +432,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"
@@ -454,7 +454,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)
@@ -469,15 +469,15 @@
 qed
 
 
-subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
+subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
 
 instantiation "fun" :: (type, topological_space) topological_space
 begin
 
-definition open_fun_def:
+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 product_topology_topspace topspace_euclidean by auto
   then show "open (UNIV::('a \<Rightarrow> 'b) set)"
@@ -486,15 +486,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)
 
-lemma 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)"
@@ -524,34 +524,34 @@
 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)
 
-subsubsection \<open>Topological countability for product spaces\<close>
+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 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}}"
@@ -588,7 +588,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})}"
@@ -621,7 +621,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
@@ -693,11 +693,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
 
-lemma 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)
@@ -776,7 +776,7 @@
   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
 
-subsection \<open>The strong operator topology on continuous linear operators\<close>
+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
@@ -797,18 +797,18 @@
 defined analogously.
 \<close>
 
-definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
+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}
@@ -818,16 +818,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)
@@ -850,13 +850,13 @@
     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)
 
 
-subsection \<open>Metrics on product spaces\<close>
+subsection%important \<open>Metrics on product spaces\<close>
 
 
 text \<open>In general, the product topology is not metrizable, unless the index set is countable.
@@ -875,10 +875,10 @@
 instantiation "fun" :: (countable, metric_space) metric_space
 begin
 
-definition dist_fun_def:
+definition%important dist_fun_def:
   "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
 
-definition uniformity_fun_def:
+definition%important 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 \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
@@ -886,9 +886,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)
@@ -936,7 +936,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"
@@ -999,7 +999,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}"
@@ -1046,7 +1046,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)
@@ -1233,7 +1233,7 @@
 by standard
 
 
-subsection \<open>Measurability\<close>
+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
@@ -1251,11 +1251,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"
@@ -1269,10 +1269,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)}"
@@ -1312,9 +1312,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}"
@@ -1331,9 +1331,9 @@
     by (simp add: * sets.sigma_sets_subset')
 qed
 
-lemma 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
@@ -1358,11 +1358,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