src/HOL/Analysis/Further_Topology.thy

 lemma not_simply_connected_circle:
   fixes a :: complex
   shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
 by (simp add: simply_connected_sphere_eq)
 
-  
+
 proposition simply_connected_punctured_convex:
   fixes a :: "'a::euclidean_space"
   assumes "convex S" and 3: "3 \<le> aff_dim S"
     shows "simply_connected(S - {a})"
 proof (cases "a \<in> rel_interior S")

 qed
 
 
 subsection\<open>The "Borsukian" property of sets\<close>
 
-text\<open>This doesn't have a standard name. Kuratowski uses "contractible with respect to [S^1]"
- while Whyburn uses "property b". It's closely related to unicoherence.\<close>
+text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to $[S^1]$''
+ while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
 
 definition Borsukian where
     "Borsukian S \<equiv>
         \<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
             \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"