src/HOL/Analysis/Brouwer_Fixpoint.thy

 (* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
 (*                                                                           *)
 (*              (c) Copyright, John Harrison 1998-2008                       *)
 (* ========================================================================= *)
 
-section \<open>Results connected with topological dimension.\<close>
+section \<open>Results connected with topological dimension\<close>
 
 theory Brouwer_Fixpoint
 imports Path_Connected Homeomorphism
 begin
 

     unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
     by (subst choice_iff[symmetric])+ blast
 qed
 
 
-subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
+subsection \<open>The key "counting" observation, somewhat abstracted\<close>
 
 lemma kuhn_counting_lemma:
   fixes bnd compo compo' face S F
   defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
   assumes [simp, intro]: "finite F" \<comment> \<open>faces\<close> and [simp, intro]: "finite S" \<comment> \<open>simplices\<close>

     using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
   ultimately show ?thesis
     by auto
 qed
 
-subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
+subsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
 
 lemma kuhn_complete_lemma:
   assumes [simp]: "finite simplices"
     and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
     and card_s[simp]:  "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"

   ultimately show ?thesis
     using that deformation_retract  by metis
 qed
 
 
-subsection\<open>Punctured affine hulls, etc.\<close>
+subsection\<open>Punctured affine hulls, etc\<close>
 
 lemma continuous_on_compact_surface_projection_aux:
   fixes S :: "'a::t2_space set"
   assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
       and contp: "continuous_on T p"

   }
   then show ?thesis
     by blast
 qed
 
-subsection\<open>Absolute retracts, Etc.\<close>
+subsection\<open>Absolute retracts, etc\<close>
 
 text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
  Euclidean neighbourhood retracts (ENR). We define AR and ANR by
  specializing the standard definitions for a set to embedding in
 spaces of higher dimension. \<close>

 lemma homeomorphic_ANR_iff_ANR:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
 by (metis ANR_homeomorphic_ANR homeomorphic_sym)
 
-subsection\<open> Analogous properties of ENRs.\<close>
+subsection\<open> Analogous properties of ENRs\<close>
 
 proposition ENR_imp_absolute_neighbourhood_retract:
   fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   assumes "ENR S" and hom: "S homeomorphic S'"
       and "S' \<subseteq> U"

   fixes S :: "'a::euclidean_space set"
   assumes "ANR S" "c \<in> components S"
   shows "ANR c"
   by (metis ANR_connected_component_ANR assms componentsE)
 
-subsection\<open>Original ANR material, now for ENRs.\<close>
+subsection\<open>Original ANR material, now for ENRs\<close>
 
 lemma ENR_bounded:
   fixes S :: "'a::euclidean_space set"
   assumes "bounded S"
   shows "ENR S \<longleftrightarrow> (\<exists>U. open U \<and> bounded U \<and> S retract_of U)"

   fixes a :: "'a::euclidean_space"
   shows "ANR(sphere a r)"
   by (simp add: ENR_imp_ANR ENR_sphere)
 
 
-subsection\<open>Spheres are connected, etc.\<close>
+subsection\<open>Spheres are connected, etc\<close>
 
 lemma locally_path_connected_sphere_gen:
   fixes S :: "'a::euclidean_space set"
   assumes "bounded S" and "convex S" 
   shows "locally path_connected (rel_frontier S)"