src/HOL/Analysis/Homotopy.thy

 subsection\<open>Homotopy equivalence\<close>
 
 subsection\<open>Homotopy equivalence of topological spaces.\<close>
 
 definition\<^marker>\<open>tag important\<close> homotopy_equivalent_space
-             (infix "homotopy'_equivalent'_space" 50)
+             (infix \<open>homotopy'_equivalent'_space\<close> 50)
   where "X homotopy_equivalent_space Y \<equiv>
         (\<exists>f g. continuous_map X Y f \<and>
               continuous_map Y X g \<and>
               homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>
               homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id)"

     by simp
 qed
 
 
 abbreviation\<^marker>\<open>tag important\<close> homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
-             (infix "homotopy'_eqv" 50)
+             (infix \<open>homotopy'_eqv\<close> 50)
   where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
 
 lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
   unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
   by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology)