src/HOL/Analysis/Brouwer_Fixpoint.thy

 John Harrison writes: "This turns out to be sufficient (since any set in \<open>\<real>\<^sup>n\<close> can be
 embedded as a closed subset of a convex subset of \<open>\<real>\<^sup>n\<^sup>+\<^sup>1\<close>) to derive the usual
 definitions, but we need to split them into two implications because of the lack of type
 quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
 
-definition%important AR :: "'a::topological_space set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> AR :: "'a::topological_space set \<Rightarrow> bool" where
 "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
   S homeomorphic S' \<and> closedin (top_of_set U) S' \<longrightarrow> S' retract_of U"
 
-definition%important ANR :: "'a::topological_space set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> ANR :: "'a::topological_space set \<Rightarrow> bool" where
 "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
   S homeomorphic S' \<and> closedin (top_of_set U) S'
   \<longrightarrow> (\<exists>T. openin (top_of_set U) T \<and> S' retract_of T)"
 
-definition%important ENR :: "'a::topological_space set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> ENR :: "'a::topological_space set \<Rightarrow> bool" where
 "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
 
 text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
 
 lemma AR_imp_absolute_extensor:

   then show ?thesis
     using finite_imp_ENR
     by (metis finite_insert infinite_imp_nonempty less_linear sphere_eq_empty sphere_trivial)
 qed
 
-corollary%unimportant ANR_sphere:
+corollary\<^marker>\<open>tag unimportant\<close> ANR_sphere:
   fixes a :: "'a::euclidean_space"
   shows "ANR(sphere a r)"
   by (simp add: ENR_imp_ANR ENR_sphere)
 
 subsubsection\<open>Spheres are connected, etc\<close>

     by (simp add: B_def a1 h'_def keq)
   qed
 qed
 
 
-corollary%unimportant nullhomotopic_into_ANR_extension:
+corollary\<^marker>\<open>tag unimportant\<close> nullhomotopic_into_ANR_extension:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "closed S"
       and contf: "continuous_on S f"
       and "ANR T"
       and fim: "f ` S \<subseteq> T"

     by (simp add: homotopic_from_subtopology)
   then show ?lhs
     by (force elim: homotopic_with_eq [of _ _ _ g "\<lambda>x. c"] simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
 qed
 
-corollary%unimportant nullhomotopic_into_rel_frontier_extension:
+corollary\<^marker>\<open>tag unimportant\<close> nullhomotopic_into_rel_frontier_extension:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "closed S"
       and contf: "continuous_on S f"
       and "convex T" "bounded T"
       and fim: "f ` S \<subseteq> rel_frontier T"
       and "S \<noteq> {}"
    shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
 by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
 
-corollary%unimportant nullhomotopic_into_sphere_extension:
+corollary\<^marker>\<open>tag unimportant\<close> nullhomotopic_into_sphere_extension:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes "closed S" and contf: "continuous_on S f"
       and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
     shows "((\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
            (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> sphere a r \<and> (\<forall>x \<in> S. g x = f x)))"

     apply (rule nullhomotopic_into_rel_frontier_extension [OF \<open>closed S\<close> contf convex_cball bounded_cball])
     apply (rule \<open>S \<noteq> {}\<close>)
     done
 qed
 
-proposition%unimportant Borsuk_map_essential_bounded_component:
+proposition\<^marker>\<open>tag unimportant\<close> Borsuk_map_essential_bounded_component:
   fixes a :: "'a :: euclidean_space"
   assumes "compact S" and "a \<notin> S"
    shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
           \<not>(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
                                (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"

     show "S \<times> \<Union>(F ` T) \<subseteq> U"
       using F by auto
   qed
 qed
 
-proposition%unimportant homotopic_neighbourhood_extension:
+proposition\<^marker>\<open>tag unimportant\<close> homotopic_neighbourhood_extension:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
       and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
       and clo: "closedin (top_of_set S) T"
       and "ANR U" and hom: "homotopic_with_canon (\<lambda>x. True) T U f g"

   ultimately show ?thesis
     by (blast intro: that)
 qed
 
 text\<open> Homotopy on a union of closed-open sets.\<close>
-proposition%unimportant homotopic_on_clopen_Union:
+proposition\<^marker>\<open>tag unimportant\<close> homotopic_on_clopen_Union:
   fixes \<F> :: "'a::euclidean_space set set"
   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
   shows "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f g"