src/HOL/Analysis/Elementary_Metric_Spaces.thy

     using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
 
 lemma compact_lemma_general:
   fixes f :: "nat \<Rightarrow> 'a"
-  fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60)
+  fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl \<open>proj\<close> 60)
   fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a"
   assumes finite_basis: "finite basis"
   assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
   assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
   assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"