src/HOL/Analysis/Polytope.thy

 imports Cartesian_Euclidean_Space Path_Connected
 begin
 
 subsection \<open>Faces of a (usually convex) set\<close>
 
-definition\<^marker>\<open>tag important\<close> face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
+definition\<^marker>\<open>tag important\<close> face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr \<open>(face'_of)\<close> 50)
   where
   "T face_of S \<longleftrightarrow>
         T \<subseteq> S \<and> convex T \<and>
         (\<forall>a \<in> S. \<forall>b \<in> S. \<forall>x \<in> T. x \<in> open_segment a b \<longrightarrow> a \<in> T \<and> b \<in> T)"
 

 subsection\<open>Exposed faces\<close>
 
 text\<open>That is, faces that are intersection with supporting hyperplane\<close>
 
 definition\<^marker>\<open>tag important\<close> exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
-                               (infixr "(exposed'_face'_of)" 50)
+                               (infixr \<open>(exposed'_face'_of)\<close> 50)
   where "T exposed_face_of S \<longleftrightarrow>
          T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
 
 lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
 proof -

 qed
 
 subsection\<open>Extreme points of a set: its singleton faces\<close>
 
 definition\<^marker>\<open>tag important\<close> extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
-                               (infixr "(extreme'_point'_of)" 50)
+                               (infixr \<open>(extreme'_point'_of)\<close> 50)
   where "x extreme_point_of S \<longleftrightarrow>
          x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
 
 lemma extreme_point_of_stillconvex:
    "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"

 qed
 
 subsection\<open>Facets\<close>
 
 definition\<^marker>\<open>tag important\<close> facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
-                    (infixr "(facet'_of)" 50)
+                    (infixr \<open>(facet'_of)\<close> 50)
   where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
 
 lemma facet_of_empty [simp]: "\<not> S facet_of {}"
   by (simp add: facet_of_def)
 

   "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   using facet_of_halfspace_le [of F "-a" "-b"] by simp
 
 subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
 
-definition\<^marker>\<open>tag important\<close> edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
+definition\<^marker>\<open>tag important\<close> edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr \<open>(edge'_of)\<close> 50)
   where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
 
 lemma edge_of_imp_subset:
    "S edge_of T \<Longrightarrow> S \<subseteq> T"
 by (simp add: edge_of_def face_of_imp_subset)

 
 subsection\<open>Simplexes\<close>
 
 text\<open>The notion of n-simplex for integer \<^term>\<open>n \<ge> -1\<close>\<close>
 
-definition\<^marker>\<open>tag important\<close> simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
+definition\<^marker>\<open>tag important\<close> simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix \<open>simplex\<close> 50)
   where "n simplex S \<equiv> \<exists>C. \<not> affine_dependent C \<and> int(card C) = n + 1 \<and> S = convex hull C"
 
 lemma simplex:
     "n simplex S \<longleftrightarrow> (\<exists>C. finite C \<and>
                        \<not> affine_dependent C \<and>