src/HOL/Analysis/Polytope.thy
 changeset 68833 fde093888c16 parent 68074 8d50467f7555 child 69260 0a9688695a1b
```     1.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Aug 27 22:58:36 2018 +0200
1.2 +++ b/src/HOL/Analysis/Polytope.thy	Tue Aug 28 13:28:39 2018 +0100
1.3 @@ -6,18 +6,18 @@
1.4  imports Cartesian_Euclidean_Space
1.5  begin
1.6
1.7 -subsection \<open>Faces of a (usually convex) set\<close>
1.8 -
1.9 -definition face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
1.10 +subsection%important \<open>Faces of a (usually convex) set\<close>
1.11 +
1.12 +definition%important face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
1.13    where
1.14    "T face_of S \<longleftrightarrow>
1.15          T \<subseteq> S \<and> convex T \<and>
1.16          (\<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)"
1.17
1.18 -lemma face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
1.19 +lemma%unimportant face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
1.20    unfolding face_of_def by blast
1.21
1.22 -lemma face_of_translation_eq [simp]:
1.23 +lemma%unimportant face_of_translation_eq [simp]:
1.24      "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
1.25  proof -
1.26    have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
1.27 @@ -32,52 +32,52 @@
1.28      done
1.29  qed
1.30
1.31 -lemma face_of_linear_image:
1.32 +lemma%unimportant face_of_linear_image:
1.33    assumes "linear f" "inj f"
1.34      shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
1.35  by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
1.36
1.37 -lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
1.38 +lemma%unimportant face_of_refl: "convex S \<Longrightarrow> S face_of S"
1.39    by (auto simp: face_of_def)
1.40
1.41 -lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
1.42 +lemma%unimportant face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
1.43    by (auto simp: face_of_def)
1.44
1.45 -lemma empty_face_of [iff]: "{} face_of S"
1.46 +lemma%unimportant empty_face_of [iff]: "{} face_of S"
1.48
1.49 -lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
1.50 +lemma%unimportant face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
1.51    by (meson empty_face_of face_of_def subset_empty)
1.52
1.53 -lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
1.54 +lemma%unimportant face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
1.55    unfolding face_of_def by (safe; blast)
1.56
1.57 -lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
1.58 +lemma%unimportant face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
1.59    unfolding face_of_def by (safe; blast)
1.60
1.61 -lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
1.62 +lemma%unimportant face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
1.63    unfolding face_of_def by (safe; blast)
1.64
1.65 -lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
1.66 +lemma%unimportant face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
1.67    unfolding face_of_def by (blast intro: convex_Int)
1.68
1.69 -lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
1.70 +lemma%unimportant face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
1.71    unfolding face_of_def by (blast intro: convex_Int)
1.72
1.73 -lemma face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
1.74 +lemma%unimportant face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
1.75    unfolding face_of_def by (blast intro: convex_Inter)
1.76
1.77 -lemma face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
1.78 +lemma%unimportant face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
1.79    unfolding face_of_def by (blast intro: convex_Int)
1.80
1.81 -lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
1.82 +lemma%unimportant face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
1.83    unfolding face_of_def by blast
1.84
1.85 -lemma face_of_imp_eq_affine_Int:
1.86 +lemma%important face_of_imp_eq_affine_Int:
1.87    fixes S :: "'a::euclidean_space set"
1.88    assumes S: "convex S"  and T: "T face_of S"
1.89    shows "T = (affine hull T) \<inter> S"
1.90 -proof -
1.91 +proof%unimportant -
1.92    have "convex T" using T by (simp add: face_of_def)
1.93    have *: False if x: "x \<in> affine hull T" and "x \<in> S" "x \<notin> T" and y: "y \<in> rel_interior T" for x y
1.94    proof -
1.95 @@ -114,15 +114,15 @@
1.96      done
1.97  qed
1.98
1.99 -lemma face_of_imp_closed:
1.100 +lemma%unimportant face_of_imp_closed:
1.101       fixes S :: "'a::euclidean_space set"
1.102       assumes "convex S" "closed S" "T face_of S" shows "closed T"
1.103    by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
1.104
1.105 -lemma face_of_Int_supporting_hyperplane_le_strong:
1.106 +lemma%important face_of_Int_supporting_hyperplane_le_strong:
1.107      assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
1.108        shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
1.109 -proof -
1.110 +proof%unimportant -
1.111    have *: "a \<bullet> u = a \<bullet> x" if "x \<in> open_segment u v" "u \<in> S" "v \<in> S" and b: "b = a \<bullet> x"
1.112            for u v x
1.113    proof (rule antisym)
1.114 @@ -145,33 +145,33 @@
1.115      using "*" open_segment_commute by blast
1.116  qed
1.117
1.118 -lemma face_of_Int_supporting_hyperplane_ge_strong:
1.119 +lemma%unimportant face_of_Int_supporting_hyperplane_ge_strong:
1.120     "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
1.121      \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
1.122    using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
1.123
1.124 -lemma face_of_Int_supporting_hyperplane_le:
1.125 +lemma%unimportant face_of_Int_supporting_hyperplane_le:
1.126      "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
1.127    by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
1.128
1.129 -lemma face_of_Int_supporting_hyperplane_ge:
1.130 +lemma%unimportant face_of_Int_supporting_hyperplane_ge:
1.131      "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
1.132    by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
1.133
1.134 -lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
1.135 +lemma%unimportant face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
1.136    using face_of_def by blast
1.137
1.138 -lemma face_of_imp_compact:
1.139 +lemma%unimportant face_of_imp_compact:
1.140      fixes S :: "'a::euclidean_space set"
1.141      shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
1.142    by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
1.143
1.144 -lemma face_of_Int_subface:
1.145 +lemma%unimportant face_of_Int_subface:
1.146       "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
1.147        \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
1.148    by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
1.149
1.150 -lemma subset_of_face_of:
1.151 +lemma%unimportant subset_of_face_of:
1.152      fixes S :: "'a::real_normed_vector set"
1.153      assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
1.154        shows "u \<subseteq> T"
1.155 @@ -213,7 +213,7 @@
1.156    qed
1.157  qed
1.158
1.159 -lemma face_of_eq:
1.160 +lemma%unimportant face_of_eq:
1.161      fixes S :: "'a::real_normed_vector set"
1.162      assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
1.163        shows "T = u"
1.164 @@ -221,13 +221,13 @@
1.165    apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
1.166    by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
1.167
1.168 -lemma face_of_disjoint_rel_interior:
1.169 +lemma%unimportant face_of_disjoint_rel_interior:
1.170        fixes S :: "'a::real_normed_vector set"
1.171        assumes "T face_of S" "T \<noteq> S"
1.172          shows "T \<inter> rel_interior S = {}"
1.173    by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
1.174
1.175 -lemma face_of_disjoint_interior:
1.176 +lemma%unimportant face_of_disjoint_interior:
1.177        fixes S :: "'a::real_normed_vector set"
1.178        assumes "T face_of S" "T \<noteq> S"
1.179          shows "T \<inter> interior S = {}"
1.180 @@ -238,19 +238,19 @@
1.181      by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
1.182  qed
1.183
1.184 -lemma face_of_subset_rel_boundary:
1.185 +lemma%unimportant face_of_subset_rel_boundary:
1.186    fixes S :: "'a::real_normed_vector set"
1.187    assumes "T face_of S" "T \<noteq> S"
1.188      shows "T \<subseteq> (S - rel_interior S)"
1.189  by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
1.190
1.191 -lemma face_of_subset_rel_frontier:
1.192 +lemma%unimportant face_of_subset_rel_frontier:
1.193      fixes S :: "'a::real_normed_vector set"
1.194      assumes "T face_of S" "T \<noteq> S"
1.195        shows "T \<subseteq> rel_frontier S"
1.196    using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
1.197
1.198 -lemma face_of_aff_dim_lt:
1.199 +lemma%unimportant face_of_aff_dim_lt:
1.200    fixes S :: "'a::euclidean_space set"
1.201    assumes "convex S" "T face_of S" "T \<noteq> S"
1.202      shows "aff_dim T < aff_dim S"
1.203 @@ -268,7 +268,7 @@
1.204      by simp
1.205  qed
1.206
1.207 -lemma subset_of_face_of_affine_hull:
1.208 +lemma%unimportant subset_of_face_of_affine_hull:
1.209      fixes S :: "'a::euclidean_space set"
1.210    assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "~disjnt (affine hull T) (rel_interior U)"
1.211    shows "U \<subseteq> T"
1.212 @@ -277,13 +277,13 @@
1.213    using rel_interior_subset [of U] dis
1.214    using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
1.215
1.216 -lemma affine_hull_face_of_disjoint_rel_interior:
1.217 +lemma%unimportant affine_hull_face_of_disjoint_rel_interior:
1.218      fixes S :: "'a::euclidean_space set"
1.219    assumes "convex S" "F face_of S" "F \<noteq> S"
1.220    shows "affine hull F \<inter> rel_interior S = {}"
1.221    by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
1.222
1.223 -lemma affine_diff_divide:
1.224 +lemma%unimportant affine_diff_divide:
1.225      assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
1.226        shows "(x - y) /\<^sub>R k \<in> S"
1.227  proof -
1.228 @@ -294,10 +294,10 @@
1.229      using \<open>affine S\<close> xy by (auto simp: affine_alt)
1.230  qed
1.231
1.232 -lemma face_of_convex_hulls:
1.233 +lemma%important face_of_convex_hulls:
1.234        assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
1.235        shows  "(convex hull T) face_of (convex hull S)"
1.236 -proof -
1.237 +proof%unimportant -
1.238    have fin: "finite T" "finite (S - T)" using assms
1.239      by (auto simp: finite_subset)
1.240    have *: "x \<in> convex hull T"
1.241 @@ -391,16 +391,16 @@
1.242      using open_segment_commute by (auto simp: face_of_def intro: *)
1.243  qed
1.244
1.245 -proposition face_of_convex_hull_insert:
1.246 +proposition%important face_of_convex_hull_insert:
1.247     "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
1.248    apply (rule face_of_trans, blast)
1.249    apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
1.250    done
1.251
1.252 -proposition face_of_affine_trivial:
1.253 +proposition%important face_of_affine_trivial:
1.254      assumes "affine S" "T face_of S"
1.255      shows "T = {} \<or> T = S"
1.256 -proof (rule ccontr, clarsimp)
1.257 +proof%unimportant (rule ccontr, clarsimp)
1.258    assume "T \<noteq> {}" "T \<noteq> S"
1.259    then obtain a where "a \<in> T" by auto
1.260    then have "a \<in> S"
1.261 @@ -430,16 +430,16 @@
1.262  qed
1.263
1.264
1.265 -lemma face_of_affine_eq:
1.266 +lemma%unimportant face_of_affine_eq:
1.267     "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
1.268  using affine_imp_convex face_of_affine_trivial face_of_refl by auto
1.269
1.270
1.271 -lemma Inter_faces_finite_altbound:
1.272 +lemma%important Inter_faces_finite_altbound:
1.273      fixes T :: "'a::euclidean_space set set"
1.274      assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
1.275      shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
1.276 -proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
1.277 +proof%unimportant (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
1.278    case True
1.279    then obtain c where c:
1.280         "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
1.281 @@ -499,17 +499,17 @@
1.282      by blast
1.283  qed
1.284
1.285 -lemma faces_of_translation:
1.286 +lemma%unimportant faces_of_translation:
1.287     "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
1.288  apply (rule subset_antisym, clarify)
1.289  apply (auto simp: image_iff)
1.290  apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
1.291  done
1.292
1.293 -proposition face_of_Times:
1.294 +proposition%important face_of_Times:
1.295    assumes "F face_of S" and "F' face_of S'"
1.296      shows "(F \<times> F') face_of (S \<times> S')"
1.297 -proof -
1.298 +proof%unimportant -
1.299    have "F \<times> F' \<subseteq> S \<times> S'"
1.300      using assms [unfolded face_of_def] by blast
1.301    moreover
1.302 @@ -531,11 +531,11 @@
1.303      unfolding face_of_def by blast
1.304  qed
1.305
1.306 -corollary face_of_Times_decomp:
1.307 +corollary%important face_of_Times_decomp:
1.308      fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.309      shows "c face_of (S \<times> S') \<longleftrightarrow> (\<exists>F F'. F face_of S \<and> F' face_of S' \<and> c = F \<times> F')"
1.310       (is "?lhs = ?rhs")
1.311 -proof
1.312 +proof%unimportant
1.313    assume c: ?lhs
1.314    show ?rhs
1.315    proof (cases "c = {}")
1.316 @@ -582,13 +582,13 @@
1.317    assume ?rhs with face_of_Times show ?lhs by auto
1.318  qed
1.319
1.320 -lemma face_of_Times_eq:
1.321 +lemma%unimportant face_of_Times_eq:
1.322      fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.323      shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
1.324             F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
1.325  by (auto simp: face_of_Times_decomp times_eq_iff)
1.326
1.327 -lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
1.328 +lemma%unimportant hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
1.329  proof -
1.330    have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
1.331      by auto
1.332 @@ -596,7 +596,7 @@
1.333    show ?thesis by auto
1.334  qed
1.335
1.336 -lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
1.337 +lemma%unimportant hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
1.338  proof -
1.339    have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
1.340      by auto
1.341 @@ -604,12 +604,12 @@
1.342    show ?thesis by auto
1.343  qed
1.344
1.345 -lemma face_of_halfspace_le:
1.346 +lemma%important face_of_halfspace_le:
1.347    fixes a :: "'n::euclidean_space"
1.348    shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
1.349           F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
1.350       (is "?lhs = ?rhs")
1.351 -proof (cases "a = 0")
1.352 +proof%unimportant (cases "a = 0")
1.353    case True then show ?thesis
1.354      using face_of_affine_eq affine_UNIV by auto
1.355  next
1.356 @@ -635,37 +635,37 @@
1.357    qed
1.358  qed
1.359
1.360 -lemma face_of_halfspace_ge:
1.361 +lemma%unimportant face_of_halfspace_ge:
1.362    fixes a :: "'n::euclidean_space"
1.363    shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
1.364           F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
1.365  using face_of_halfspace_le [of F "-a" "-b"] by simp
1.366
1.367 -subsection\<open>Exposed faces\<close>
1.368 +subsection%important\<open>Exposed faces\<close>
1.369
1.370  text\<open>That is, faces that are intersection with supporting hyperplane\<close>
1.371
1.372 -definition exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
1.373 +definition%important exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
1.374                                 (infixr "(exposed'_face'_of)" 50)
1.375    where "T exposed_face_of S \<longleftrightarrow>
1.376           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})"
1.377
1.378 -lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
1.379 +lemma%unimportant empty_exposed_face_of [iff]: "{} exposed_face_of S"
1.381    apply (rule_tac x=0 in exI)
1.382    apply (rule_tac x=1 in exI, force)
1.383    done
1.384
1.385 -lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
1.386 +lemma%unimportant exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
1.387    apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
1.388    apply (rule_tac x=0 in exI)+
1.389    apply force
1.390    done
1.391
1.392 -lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
1.393 +lemma%unimportant exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
1.394    by simp
1.395
1.396 -lemma exposed_face_of:
1.397 +lemma%unimportant exposed_face_of:
1.398      "T exposed_face_of S \<longleftrightarrow>
1.399       T face_of S \<and>
1.400       (T = {} \<or> T = S \<or>
1.401 @@ -688,19 +688,19 @@
1.402    qed
1.403  qed
1.404
1.405 -lemma exposed_face_of_Int_supporting_hyperplane_le:
1.406 +lemma%unimportant exposed_face_of_Int_supporting_hyperplane_le:
1.407     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
1.408  by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
1.409
1.410 -lemma exposed_face_of_Int_supporting_hyperplane_ge:
1.411 +lemma%unimportant exposed_face_of_Int_supporting_hyperplane_ge:
1.412     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
1.413  using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
1.414
1.415 -proposition exposed_face_of_Int:
1.416 +proposition%important exposed_face_of_Int:
1.417    assumes "T exposed_face_of S"
1.418        and "u exposed_face_of S"
1.419      shows "(T \<inter> u) exposed_face_of S"
1.420 -proof -
1.421 +proof%unimportant -
1.422    obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
1.423                 and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
1.424                 and teq: "T = S \<inter> {x. a \<bullet> x = b}"
1.425 @@ -722,12 +722,12 @@
1.426      done
1.427  qed
1.428
1.429 -proposition exposed_face_of_Inter:
1.430 +proposition%important exposed_face_of_Inter:
1.431      fixes P :: "'a::euclidean_space set set"
1.432    assumes "P \<noteq> {}"
1.433        and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
1.434      shows "\<Inter>P exposed_face_of S"
1.435 -proof -
1.436 +proof%unimportant -
1.437    obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
1.438      using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
1.439      by force
1.440 @@ -749,14 +749,14 @@
1.441    qed
1.442  qed
1.443
1.444 -proposition exposed_face_of_sums:
1.445 +proposition%important exposed_face_of_sums:
1.446    assumes "convex S" and "convex T"
1.447        and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
1.448            (is "F exposed_face_of ?ST")
1.449    obtains k l
1.450      where "k exposed_face_of S" "l exposed_face_of T"
1.451            "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
1.452 -proof (cases "F = {}")
1.453 +proof%unimportant (cases "F = {}")
1.454    case True then show ?thesis
1.455      using that by blast
1.456  next
1.457 @@ -805,14 +805,14 @@
1.458    qed
1.459  qed
1.460
1.461 -lemma exposed_face_of_parallel:
1.462 +lemma%important exposed_face_of_parallel:
1.463     "T exposed_face_of S \<longleftrightarrow>
1.464           T face_of S \<and>
1.465           (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
1.466                  (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
1.467                  (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
1.468    (is "?lhs = ?rhs")
1.469 -proof
1.470 +proof%unimportant
1.471    assume ?lhs then show ?rhs
1.472    proof (clarsimp simp: exposed_face_of_def)
1.473      fix a b
1.474 @@ -874,40 +874,40 @@
1.475      unfolding exposed_face_of_def by blast
1.476  qed
1.477
1.478 -subsection\<open>Extreme points of a set: its singleton faces\<close>
1.479 -
1.480 -definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
1.481 +subsection%important\<open>Extreme points of a set: its singleton faces\<close>
1.482 +
1.483 +definition%important extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
1.484                                 (infixr "(extreme'_point'_of)" 50)
1.485    where "x extreme_point_of S \<longleftrightarrow>
1.486           x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
1.487
1.488 -lemma extreme_point_of_stillconvex:
1.489 +lemma%unimportant extreme_point_of_stillconvex:
1.490     "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
1.491    by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
1.492
1.493 -lemma face_of_singleton:
1.494 +lemma%unimportant face_of_singleton:
1.495     "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
1.496  by (fastforce simp add: extreme_point_of_def face_of_def)
1.497
1.498 -lemma extreme_point_not_in_REL_INTERIOR:
1.499 +lemma%unimportant extreme_point_not_in_REL_INTERIOR:
1.500      fixes S :: "'a::real_normed_vector set"
1.501      shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
1.502  apply (simp add: face_of_singleton [symmetric])
1.503  apply (blast dest: face_of_disjoint_rel_interior)
1.504  done
1.505
1.506 -lemma extreme_point_not_in_interior:
1.507 +lemma%important extreme_point_not_in_interior:
1.508      fixes S :: "'a::{real_normed_vector, perfect_space} set"
1.509      shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
1.510  apply (case_tac "S = {x}")
1.512  by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
1.513
1.514 -lemma extreme_point_of_face:
1.515 +lemma%unimportant extreme_point_of_face:
1.516       "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
1.517    by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
1.518
1.519 -lemma extreme_point_of_convex_hull:
1.520 +lemma%unimportant extreme_point_of_convex_hull:
1.521     "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
1.523  using hull_minimal [of S "(convex hull S) - {x}" convex]
1.524 @@ -915,52 +915,52 @@
1.525  apply blast
1.526  done
1.527
1.528 -lemma extreme_points_of_convex_hull:
1.529 +lemma%important extreme_points_of_convex_hull:
1.530     "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
1.531 -using extreme_point_of_convex_hull by auto
1.532 -
1.533 -lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
1.534 +using%unimportant extreme_point_of_convex_hull by auto
1.535 +
1.536 +lemma%unimportant extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
1.538
1.539 -lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
1.540 +lemma%unimportant extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
1.541    using extreme_point_of_stillconvex by auto
1.542
1.543 -lemma extreme_point_of_translation_eq:
1.544 +lemma%unimportant extreme_point_of_translation_eq:
1.545     "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
1.546  by (auto simp: extreme_point_of_def)
1.547
1.548 -lemma extreme_points_of_translation:
1.549 +lemma%important extreme_points_of_translation:
1.550     "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
1.551      (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
1.552 -using extreme_point_of_translation_eq
1.553 -by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
1.554 -
1.555 -lemma extreme_point_of_Int:
1.556 +using%unimportant extreme_point_of_translation_eq
1.557 +by%unimportant auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
1.558 +
1.559 +lemma%unimportant extreme_point_of_Int:
1.560     "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
1.562
1.563 -lemma extreme_point_of_Int_supporting_hyperplane_le:
1.564 +lemma%important extreme_point_of_Int_supporting_hyperplane_le:
1.565     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
1.566  apply (simp add: face_of_singleton [symmetric])
1.567  by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
1.568
1.569 -lemma extreme_point_of_Int_supporting_hyperplane_ge:
1.570 +lemma%unimportant extreme_point_of_Int_supporting_hyperplane_ge:
1.571     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
1.572  apply (simp add: face_of_singleton [symmetric])
1.573  by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
1.574
1.575 -lemma exposed_point_of_Int_supporting_hyperplane_le:
1.576 +lemma%unimportant exposed_point_of_Int_supporting_hyperplane_le:
1.577     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
1.578  apply (simp add: exposed_face_of_def face_of_singleton)
1.579  apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
1.580  done
1.581
1.582 -lemma exposed_point_of_Int_supporting_hyperplane_ge:
1.583 +lemma%unimportant exposed_point_of_Int_supporting_hyperplane_ge:
1.584      "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
1.585  using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
1.586  by simp
1.587
1.588 -lemma extreme_point_of_convex_hull_insert:
1.589 +lemma%unimportant extreme_point_of_convex_hull_insert:
1.590     "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
1.591  apply (case_tac "a \<in> S")
1.593 @@ -968,40 +968,40 @@
1.594  apply (auto simp: face_of_singleton hull_same)
1.595  done
1.596
1.597 -subsection\<open>Facets\<close>
1.598 -
1.599 -definition facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
1.600 +subsection%important\<open>Facets\<close>
1.601 +
1.602 +definition%important facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
1.603                      (infixr "(facet'_of)" 50)
1.604    where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
1.605
1.606 -lemma facet_of_empty [simp]: "~ S facet_of {}"
1.607 +lemma%unimportant facet_of_empty [simp]: "~ S facet_of {}"
1.609
1.610 -lemma facet_of_irrefl [simp]: "~ S facet_of S "
1.611 +lemma%unimportant facet_of_irrefl [simp]: "~ S facet_of S "
1.613
1.614 -lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
1.615 +lemma%unimportant facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
1.617
1.618 -lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
1.619 +lemma%unimportant facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
1.620    by (simp add: face_of_imp_subset facet_of_def)
1.621
1.622 -lemma hyperplane_facet_of_halfspace_le:
1.623 +lemma%unimportant hyperplane_facet_of_halfspace_le:
1.624     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
1.625  unfolding facet_of_def hyperplane_eq_empty
1.626  by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
1.627             DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
1.628
1.629 -lemma hyperplane_facet_of_halfspace_ge:
1.630 +lemma%unimportant hyperplane_facet_of_halfspace_ge:
1.631      "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
1.632  unfolding facet_of_def hyperplane_eq_empty
1.633  by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
1.634             DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
1.635
1.636 -lemma facet_of_halfspace_le:
1.637 +lemma%important facet_of_halfspace_le:
1.638      "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
1.639      (is "?lhs = ?rhs")
1.640 -proof
1.641 +proof%unimportant
1.642    assume c: ?lhs
1.643    with c facet_of_irrefl show ?rhs
1.644      by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
1.645 @@ -1010,26 +1010,26 @@
1.647  qed
1.648
1.649 -lemma facet_of_halfspace_ge:
1.650 +lemma%unimportant facet_of_halfspace_ge:
1.651      "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
1.652  using facet_of_halfspace_le [of F "-a" "-b"] by simp
1.653
1.654 -subsection \<open>Edges: faces of affine dimension 1\<close>
1.655 -
1.656 -definition edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
1.657 +subsection%important \<open>Edges: faces of affine dimension 1\<close>
1.658 +
1.659 +definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
1.660    where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
1.661
1.662 -lemma edge_of_imp_subset:
1.663 +lemma%unimportant edge_of_imp_subset:
1.664     "S edge_of T \<Longrightarrow> S \<subseteq> T"
1.665  by (simp add: edge_of_def face_of_imp_subset)
1.666
1.667 -subsection\<open>Existence of extreme points\<close>
1.668 -
1.669 -lemma different_norm_3_collinear_points:
1.670 +subsection%important\<open>Existence of extreme points\<close>
1.671 +
1.672 +lemma%important different_norm_3_collinear_points:
1.673    fixes a :: "'a::euclidean_space"
1.674    assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
1.675    shows False
1.676 -proof -
1.677 +proof%unimportant -
1.678    obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
1.679               and "a \<noteq> b"
1.680               and u01: "0 < u" "u < 1"
1.681 @@ -1050,11 +1050,11 @@
1.682      using \<open>a \<noteq> b\<close> by force
1.683  qed
1.684
1.685 -proposition extreme_point_exists_convex:
1.686 +proposition%important extreme_point_exists_convex:
1.687    fixes S :: "'a::euclidean_space set"
1.688    assumes "compact S" "convex S" "S \<noteq> {}"
1.689    obtains x where "x extreme_point_of S"
1.690 -proof -
1.691 +proof%unimportant -
1.692    obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
1.693      using distance_attains_sup [of S 0] assms by auto
1.694    have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
1.695 @@ -1099,13 +1099,13 @@
1.696      done
1.697  qed
1.698
1.699 -subsection\<open>Krein-Milman, the weaker form\<close>
1.700 -
1.701 -proposition Krein_Milman:
1.702 +subsection%important\<open>Krein-Milman, the weaker form\<close>
1.703 +
1.704 +proposition%important Krein_Milman:
1.705    fixes S :: "'a::euclidean_space set"
1.706    assumes "compact S" "convex S"
1.707      shows "S = closure(convex hull {x. x extreme_point_of S})"
1.708 -proof (cases "S = {}")
1.709 +proof%unimportant (cases "S = {}")
1.710    case True then show ?thesis   by simp
1.711  next
1.712    case False
1.713 @@ -1155,12 +1155,12 @@
1.714
1.715  text\<open>Now the sharper form.\<close>
1.716
1.717 -lemma Krein_Milman_Minkowski_aux:
1.718 +lemma%important Krein_Milman_Minkowski_aux:
1.719    fixes S :: "'a::euclidean_space set"
1.720    assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
1.721      shows "0 \<in> convex hull {x. x extreme_point_of S}"
1.722  using n S
1.723 -proof (induction n arbitrary: S rule: less_induct)
1.724 +proof%unimportant (induction n arbitrary: S rule: less_induct)
1.725    case (less n S) show ?case
1.726    proof (cases "0 \<in> rel_interior S")
1.727      case True with Krein_Milman show ?thesis
1.728 @@ -1197,11 +1197,11 @@
1.729  qed
1.730
1.731
1.732 -theorem Krein_Milman_Minkowski:
1.733 +theorem%important Krein_Milman_Minkowski:
1.734    fixes S :: "'a::euclidean_space set"
1.735    assumes "compact S" "convex S"
1.736      shows "S = convex hull {x. x extreme_point_of S}"
1.737 -proof
1.738 +proof%unimportant
1.739    show "S \<subseteq> convex hull {x. x extreme_point_of S}"
1.740    proof
1.741      fix a assume [simp]: "a \<in> S"
1.742 @@ -1225,17 +1225,17 @@
1.743  qed
1.744
1.745
1.746 -subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
1.747 -
1.748 -lemma Krein_Milman_polytope:
1.749 +subsection%important\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
1.750 +
1.751 +lemma%important Krein_Milman_polytope:
1.752    fixes S :: "'a::euclidean_space set"
1.753    shows
1.754     "finite S
1.755         \<Longrightarrow> convex hull S =
1.756             convex hull {x. x extreme_point_of (convex hull S)}"
1.757 -by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
1.758 -
1.759 -lemma extreme_points_of_convex_hull_eq:
1.760 +by%unimportant (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
1.761 +
1.762 +lemma%unimportant extreme_points_of_convex_hull_eq:
1.763    fixes S :: "'a::euclidean_space set"
1.764    shows
1.765     "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
1.766 @@ -1243,18 +1243,18 @@
1.767  by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
1.768
1.769
1.770 -lemma extreme_point_of_convex_hull_eq:
1.771 +lemma%unimportant extreme_point_of_convex_hull_eq:
1.772    fixes S :: "'a::euclidean_space set"
1.773    shows
1.774     "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
1.775      \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
1.776  using extreme_points_of_convex_hull_eq by auto
1.777
1.778 -lemma extreme_point_of_convex_hull_convex_independent:
1.779 +lemma%important extreme_point_of_convex_hull_convex_independent:
1.780    fixes S :: "'a::euclidean_space set"
1.781    assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
1.782    shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
1.783 -proof -
1.784 +proof%unimportant -
1.785    have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
1.786    proof -
1.787      obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
1.788 @@ -1265,7 +1265,7 @@
1.789      by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
1.790  qed
1.791
1.792 -lemma extreme_point_of_convex_hull_affine_independent:
1.793 +lemma%unimportant extreme_point_of_convex_hull_affine_independent:
1.794    fixes S :: "'a::euclidean_space set"
1.795    shows
1.796     "~ affine_dependent S
1.797 @@ -1273,7 +1273,7 @@
1.798  by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
1.799
1.800  text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
1.801 -lemma extreme_point_of_convex_hull_2:
1.802 +lemma%unimportant extreme_point_of_convex_hull_2:
1.803    fixes x :: "'a::euclidean_space"
1.804    shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
1.805  proof -
1.806 @@ -1283,13 +1283,13 @@
1.807      by simp
1.808  qed
1.809
1.810 -lemma extreme_point_of_segment:
1.811 +lemma%unimportant extreme_point_of_segment:
1.812    fixes x :: "'a::euclidean_space"
1.813    shows
1.814     "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
1.815  by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
1.816
1.817 -lemma face_of_convex_hull_subset:
1.818 +lemma%unimportant face_of_convex_hull_subset:
1.819    fixes S :: "'a::euclidean_space set"
1.820    assumes "compact S" and T: "T face_of (convex hull S)"
1.821    obtains s' where "s' \<subseteq> S" "T = convex hull s'"
1.822 @@ -1298,11 +1298,11 @@
1.823  by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
1.824
1.825
1.826 -lemma face_of_convex_hull_aux:
1.827 +lemma%important face_of_convex_hull_aux:
1.828    assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
1.829      and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
1.830    shows "p \<in> S"
1.831 -proof -
1.832 +proof%unimportant -
1.833    have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
1.834      by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
1.835    moreover have "affine hull {a,b,c} \<subseteq> S"
1.836 @@ -1317,14 +1317,14 @@
1.837    ultimately show ?thesis by force
1.838  qed
1.839
1.840 -proposition face_of_convex_hull_insert_eq:
1.841 +proposition%important face_of_convex_hull_insert_eq:
1.842    fixes a :: "'a :: euclidean_space"
1.843    assumes "finite S" and a: "a \<notin> affine hull S"
1.844    shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
1.845            F face_of (convex hull S) \<or>
1.846            (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
1.847           (is "F face_of ?CAS \<longleftrightarrow> _")
1.848 -proof safe
1.849 +proof%unimportant safe
1.850    assume F: "F face_of ?CAS"
1.851      and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
1.852    obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
1.853 @@ -1465,18 +1465,18 @@
1.854    qed
1.855  qed
1.856
1.857 -lemma face_of_convex_hull_insert2:
1.858 +lemma%unimportant face_of_convex_hull_insert2:
1.859    fixes a :: "'a :: euclidean_space"
1.860    assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
1.861    shows "convex hull (insert a F) face_of convex hull (insert a S)"
1.862    by (metis F face_of_convex_hull_insert_eq [OF S a])
1.863
1.864 -proposition face_of_convex_hull_affine_independent:
1.865 +proposition%important face_of_convex_hull_affine_independent:
1.866    fixes S :: "'a::euclidean_space set"
1.867    assumes "~ affine_dependent S"
1.868      shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
1.869            (is "?lhs = ?rhs")
1.870 -proof
1.871 +proof%unimportant
1.872    assume ?lhs
1.873    then show ?rhs
1.874      by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
1.875 @@ -1493,7 +1493,7 @@
1.876      by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
1.877  qed
1.878
1.879 -lemma facet_of_convex_hull_affine_independent:
1.880 +lemma%unimportant facet_of_convex_hull_affine_independent:
1.881    fixes S :: "'a::euclidean_space set"
1.882    assumes "~ affine_dependent S"
1.883      shows "T facet_of (convex hull S) \<longleftrightarrow>
1.884 @@ -1540,7 +1540,7 @@
1.885      done
1.886  qed
1.887
1.888 -lemma facet_of_convex_hull_affine_independent_alt:
1.889 +lemma%unimportant facet_of_convex_hull_affine_independent_alt:
1.890    fixes S :: "'a::euclidean_space set"
1.891    shows
1.892     "~affine_dependent S
1.893 @@ -1551,7 +1551,7 @@
1.894  apply (metis Diff_cancel Int_empty_right Int_insert_right_if1  aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty  not_less_eq_eq numeral_2_eq_2)
1.895  done
1.896
1.897 -lemma segment_face_of:
1.898 +lemma%unimportant segment_face_of:
1.899    assumes "(closed_segment a b) face_of S"
1.900    shows "a extreme_point_of S" "b extreme_point_of S"
1.901  proof -
1.902 @@ -1571,12 +1571,12 @@
1.903  qed
1.904
1.905
1.906 -lemma Krein_Milman_frontier:
1.907 +lemma%important Krein_Milman_frontier:
1.908    fixes S :: "'a::euclidean_space set"
1.909    assumes "convex S" "compact S"
1.910      shows "S = convex hull (frontier S)"
1.911            (is "?lhs = ?rhs")
1.912 -proof
1.913 +proof%unimportant
1.914    have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
1.915      using Krein_Milman_Minkowski assms by blast
1.916    also have "... \<subseteq> ?rhs"
1.917 @@ -1593,36 +1593,36 @@
1.918    finally show "?rhs \<subseteq> ?lhs" .
1.919  qed
1.920
1.921 -subsection\<open>Polytopes\<close>
1.922 -
1.923 -definition polytope where
1.924 +subsection%important\<open>Polytopes\<close>
1.925 +
1.926 +definition%important polytope where
1.927   "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
1.928
1.929 -lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
1.930 +lemma%unimportant polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
1.931  apply (simp add: polytope_def, safe)
1.932  apply (metis convex_hull_translation finite_imageI translation_galois)
1.933  by (metis convex_hull_translation finite_imageI)
1.934
1.935 -lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
1.936 +lemma%unimportant polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
1.937    unfolding polytope_def using convex_hull_linear_image by blast
1.938
1.939 -lemma polytope_empty: "polytope {}"
1.940 +lemma%unimportant polytope_empty: "polytope {}"
1.941    using convex_hull_empty polytope_def by blast
1.942
1.943 -lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
1.944 +lemma%unimportant polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
1.945    using polytope_def by auto
1.946
1.947 -lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
1.948 +lemma%unimportant polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
1.949    unfolding polytope_def
1.950    by (metis finite_cartesian_product convex_hull_Times)
1.951
1.952 -lemma face_of_polytope_polytope:
1.953 +lemma%unimportant face_of_polytope_polytope:
1.954    fixes S :: "'a::euclidean_space set"
1.955    shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
1.956  unfolding polytope_def
1.957  by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
1.958
1.959 -lemma finite_polytope_faces:
1.960 +lemma%unimportant finite_polytope_faces:
1.961    fixes S :: "'a::euclidean_space set"
1.962    assumes "polytope S"
1.963    shows "finite {F. F face_of S}"
1.964 @@ -1637,48 +1637,48 @@
1.965      by (blast intro: finite_subset)
1.966  qed
1.967
1.968 -lemma finite_polytope_facets:
1.969 +lemma%unimportant finite_polytope_facets:
1.970    assumes "polytope S"
1.971    shows "finite {T. T facet_of S}"
1.972  by (simp add: assms facet_of_def finite_polytope_faces)
1.973
1.974 -lemma polytope_scaling:
1.975 +lemma%unimportant polytope_scaling:
1.976    assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
1.977  by (simp add: assms polytope_linear_image)
1.978
1.979 -lemma polytope_imp_compact:
1.980 +lemma%unimportant polytope_imp_compact:
1.981    fixes S :: "'a::real_normed_vector set"
1.982    shows "polytope S \<Longrightarrow> compact S"
1.983  by (metis finite_imp_compact_convex_hull polytope_def)
1.984
1.985 -lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
1.986 +lemma%unimportant polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
1.987    by (metis convex_convex_hull polytope_def)
1.988
1.989 -lemma polytope_imp_closed:
1.990 +lemma%unimportant polytope_imp_closed:
1.991    fixes S :: "'a::real_normed_vector set"
1.992    shows "polytope S \<Longrightarrow> closed S"
1.993  by (simp add: compact_imp_closed polytope_imp_compact)
1.994
1.995 -lemma polytope_imp_bounded:
1.996 +lemma%unimportant polytope_imp_bounded:
1.997    fixes S :: "'a::real_normed_vector set"
1.998    shows "polytope S \<Longrightarrow> bounded S"
1.999  by (simp add: compact_imp_bounded polytope_imp_compact)
1.1000
1.1001 -lemma polytope_interval: "polytope(cbox a b)"
1.1002 +lemma%unimportant polytope_interval: "polytope(cbox a b)"
1.1003    unfolding polytope_def by (meson closed_interval_as_convex_hull)
1.1004
1.1005 -lemma polytope_sing: "polytope {a}"
1.1006 +lemma%unimportant polytope_sing: "polytope {a}"
1.1007    using polytope_def by force
1.1008
1.1009 -lemma face_of_polytope_insert:
1.1010 +lemma%unimportant face_of_polytope_insert:
1.1011       "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
1.1012    by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
1.1013
1.1014 -lemma face_of_polytope_insert2:
1.1015 +lemma%important face_of_polytope_insert2:
1.1016    fixes a :: "'a :: euclidean_space"
1.1017    assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
1.1018    shows "convex hull (insert a F) face_of convex hull (insert a S)"
1.1019 -proof -
1.1020 +proof%unimportant -
1.1021    obtain V where "finite V" "S = convex hull V"
1.1022      using assms by (auto simp: polytope_def)
1.1023    then have "convex hull (insert a F) face_of convex hull (insert a V)"
1.1024 @@ -1688,31 +1688,31 @@
1.1025  qed
1.1026
1.1027
1.1028 -subsection\<open>Polyhedra\<close>
1.1029 -
1.1030 -definition polyhedron where
1.1031 +subsection%important\<open>Polyhedra\<close>
1.1032 +
1.1033 +definition%important polyhedron where
1.1034   "polyhedron S \<equiv>
1.1035          \<exists>F. finite F \<and>
1.1036              S = \<Inter> F \<and>
1.1037              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
1.1038
1.1039 -lemma polyhedron_Int [intro,simp]:
1.1040 +lemma%unimportant polyhedron_Int [intro,simp]:
1.1041     "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
1.1042    apply (simp add: polyhedron_def, clarify)
1.1043    apply (rename_tac F G)
1.1044    apply (rule_tac x="F \<union> G" in exI, auto)
1.1045    done
1.1046
1.1047 -lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
1.1048 +lemma%unimportant polyhedron_UNIV [iff]: "polyhedron UNIV"
1.1049    unfolding polyhedron_def
1.1050    by (rule_tac x="{}" in exI) auto
1.1051
1.1052 -lemma polyhedron_Inter [intro,simp]:
1.1053 +lemma%unimportant polyhedron_Inter [intro,simp]:
1.1054     "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
1.1055  by (induction F rule: finite_induct) auto
1.1056
1.1057
1.1058 -lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
1.1059 +lemma%unimportant polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
1.1060  proof -
1.1061    have "\<exists>a. a \<noteq> 0 \<and>
1.1062               (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
1.1063 @@ -1731,7 +1731,7 @@
1.1064      done
1.1065  qed
1.1066
1.1067 -lemma polyhedron_halfspace_le:
1.1068 +lemma%unimportant polyhedron_halfspace_le:
1.1069    fixes a :: "'a :: euclidean_space"
1.1070    shows "polyhedron {x. a \<bullet> x \<le> b}"
1.1071  proof (cases "a = 0")
1.1072 @@ -1743,53 +1743,53 @@
1.1073      by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
1.1074  qed
1.1075
1.1076 -lemma polyhedron_halfspace_ge:
1.1077 +lemma%unimportant polyhedron_halfspace_ge:
1.1078    fixes a :: "'a :: euclidean_space"
1.1079    shows "polyhedron {x. a \<bullet> x \<ge> b}"
1.1080  using polyhedron_halfspace_le [of "-a" "-b"] by simp
1.1081
1.1082 -lemma polyhedron_hyperplane:
1.1083 +lemma%important polyhedron_hyperplane:
1.1084    fixes a :: "'a :: euclidean_space"
1.1085    shows "polyhedron {x. a \<bullet> x = b}"
1.1086 -proof -
1.1087 +proof%unimportant -
1.1088    have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
1.1089      by force
1.1090    then show ?thesis
1.1091      by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
1.1092  qed
1.1093
1.1094 -lemma affine_imp_polyhedron:
1.1095 +lemma%unimportant affine_imp_polyhedron:
1.1096    fixes S :: "'a :: euclidean_space set"
1.1097    shows "affine S \<Longrightarrow> polyhedron S"
1.1098  by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
1.1099
1.1100 -lemma polyhedron_imp_closed:
1.1101 +lemma%unimportant polyhedron_imp_closed:
1.1102    fixes S :: "'a :: euclidean_space set"
1.1103    shows "polyhedron S \<Longrightarrow> closed S"
1.1105  using closed_halfspace_le by fastforce
1.1106
1.1107 -lemma polyhedron_imp_convex:
1.1108 +lemma%unimportant polyhedron_imp_convex:
1.1109    fixes S :: "'a :: euclidean_space set"
1.1110    shows "polyhedron S \<Longrightarrow> convex S"
1.1112  using convex_Inter convex_halfspace_le by fastforce
1.1113
1.1114 -lemma polyhedron_affine_hull:
1.1115 +lemma%unimportant polyhedron_affine_hull:
1.1116    fixes S :: "'a :: euclidean_space set"
1.1117    shows "polyhedron(affine hull S)"
1.1119
1.1120
1.1121 -subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
1.1122 -
1.1123 -lemma polyhedron_Int_affine:
1.1124 +subsection%important\<open>Canonical polyhedron representation making facial structure explicit\<close>
1.1125 +
1.1126 +lemma%important polyhedron_Int_affine:
1.1127    fixes S :: "'a :: euclidean_space set"
1.1128    shows "polyhedron S \<longleftrightarrow>
1.1129             (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
1.1130                  (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
1.1131          (is "?lhs = ?rhs")
1.1132 -proof
1.1133 +proof%unimportant
1.1134    assume ?lhs then show ?rhs
1.1136      apply (erule ex_forward)
1.1137 @@ -1803,13 +1803,13 @@
1.1138      done
1.1139  qed
1.1140
1.1141 -proposition rel_interior_polyhedron_explicit:
1.1142 +proposition%important rel_interior_polyhedron_explicit:
1.1143    assumes "finite F"
1.1144        and seq: "S = affine hull S \<inter> \<Inter>F"
1.1145        and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
1.1146        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
1.1147      shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
1.1148 -proof -
1.1149 +proof%unimportant -
1.1150    have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
1.1151      by (meson IntE mem_rel_interior)
1.1152    moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
1.1153 @@ -1877,7 +1877,7 @@
1.1154  qed
1.1155
1.1156
1.1157 -lemma polyhedron_Int_affine_parallel:
1.1158 +lemma%important polyhedron_Int_affine_parallel:
1.1159    fixes S :: "'a :: euclidean_space set"
1.1160    shows "polyhedron S \<longleftrightarrow>
1.1161           (\<exists>F. finite F \<and>
1.1162 @@ -1885,7 +1885,7 @@
1.1163                (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
1.1164                               (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
1.1165      (is "?lhs = ?rhs")
1.1166 -proof
1.1167 +proof%unimportant
1.1168    assume ?lhs
1.1169    then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
1.1170                    and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
1.1171 @@ -1931,7 +1931,7 @@
1.1172  qed
1.1173
1.1174
1.1175 -proposition polyhedron_Int_affine_parallel_minimal:
1.1176 +proposition%important polyhedron_Int_affine_parallel_minimal:
1.1177    fixes S :: "'a :: euclidean_space set"
1.1178    shows "polyhedron S \<longleftrightarrow>
1.1179           (\<exists>F. finite F \<and>
1.1180 @@ -1940,7 +1940,7 @@
1.1181                               (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
1.1182                (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
1.1183      (is "?lhs = ?rhs")
1.1184 -proof
1.1185 +proof%unimportant
1.1186    assume ?lhs
1.1187    then obtain f0
1.1188             where f0: "finite f0"
1.1189 @@ -1976,7 +1976,7 @@
1.1190  qed
1.1191
1.1192
1.1193 -lemma polyhedron_Int_affine_minimal:
1.1194 +lemma%unimportant polyhedron_Int_affine_minimal:
1.1195    fixes S :: "'a :: euclidean_space set"
1.1196    shows "polyhedron S \<longleftrightarrow>
1.1197           (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
1.1198 @@ -1987,13 +1987,13 @@
1.1199  apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
1.1200  done
1.1201
1.1202 -proposition facet_of_polyhedron_explicit:
1.1203 +proposition%important facet_of_polyhedron_explicit:
1.1204    assumes "finite F"
1.1205        and seq: "S = affine hull S \<inter> \<Inter>F"
1.1206        and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
1.1207        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
1.1208      shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
1.1209 -proof (cases "S = {}")
1.1210 +proof%unimportant (cases "S = {}")
1.1211    case True with psub show ?thesis by force
1.1212  next
1.1213    case False
1.1214 @@ -2198,7 +2198,7 @@
1.1215  qed
1.1216
1.1217
1.1218 -lemma face_of_polyhedron_subset_explicit:
1.1219 +lemma%important face_of_polyhedron_subset_explicit:
1.1220    fixes S :: "'a :: euclidean_space set"
1.1221    assumes "finite F"
1.1222        and seq: "S = affine hull S \<inter> \<Inter>F"
1.1223 @@ -2206,7 +2206,7 @@
1.1224        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
1.1225        and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
1.1226     obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
1.1227 -proof -
1.1228 +proof%unimportant -
1.1229    have "c \<subseteq> S" using \<open>c face_of S\<close>
1.1231    have "polyhedron S"
1.1232 @@ -2245,7 +2245,7 @@
1.1233  qed
1.1234
1.1235  text\<open>Initial part of proof duplicates that above\<close>
1.1236 -proposition face_of_polyhedron_explicit:
1.1237 +proposition%important face_of_polyhedron_explicit:
1.1238    fixes S :: "'a :: euclidean_space set"
1.1239    assumes "finite F"
1.1240        and seq: "S = affine hull S \<inter> \<Inter>F"
1.1241 @@ -2253,7 +2253,7 @@
1.1242        and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
1.1243        and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
1.1244      shows "c = \<Inter>{S \<inter> {x. a h \<bullet> x = b h} | h. h \<in> F \<and> c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}"
1.1245 -proof -
1.1246 +proof%unimportant -
1.1247    let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
1.1248    have "c \<subseteq> S" using \<open>c face_of S\<close>
1.1250 @@ -2359,10 +2359,10 @@
1.1251
1.1252  subsection\<open>More general corollaries from the explicit representation\<close>
1.1253
1.1254 -corollary facet_of_polyhedron:
1.1255 +corollary%important facet_of_polyhedron:
1.1256    assumes "polyhedron S" and "c facet_of S"
1.1257    obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
1.1258 -proof -
1.1259 +proof%unimportant -
1.1260    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
1.1261               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
1.1262               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
1.1263 @@ -2379,10 +2379,10 @@
1.1264      by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
1.1265  qed
1.1266
1.1267 -corollary face_of_polyhedron:
1.1268 +corollary%important face_of_polyhedron:
1.1269    assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
1.1270      shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
1.1271 -proof -
1.1272 +proof%unimportant -
1.1273    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
1.1274               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
1.1275               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
1.1276 @@ -2395,14 +2395,14 @@
1.1277      done
1.1278  qed
1.1279
1.1280 -lemma face_of_polyhedron_subset_facet:
1.1281 +lemma%unimportant face_of_polyhedron_subset_facet:
1.1282    assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
1.1283    obtains F where "F facet_of S" "c \<subseteq> F"
1.1284  using face_of_polyhedron assms
1.1285  by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
1.1286
1.1287
1.1288 -lemma exposed_face_of_polyhedron:
1.1289 +lemma%unimportant exposed_face_of_polyhedron:
1.1290    assumes "polyhedron S"
1.1291      shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
1.1292  proof
1.1293 @@ -2430,12 +2430,12 @@
1.1294    qed
1.1295  qed
1.1296
1.1297 -lemma face_of_polyhedron_polyhedron:
1.1298 +lemma%unimportant face_of_polyhedron_polyhedron:
1.1299    fixes S :: "'a :: euclidean_space set"
1.1300    assumes "polyhedron S" "c face_of S" shows "polyhedron c"
1.1301  by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex)
1.1302
1.1303 -lemma finite_polyhedron_faces:
1.1304 +lemma%unimportant finite_polyhedron_faces:
1.1305    fixes S :: "'a :: euclidean_space set"
1.1306    assumes "polyhedron S"
1.1307      shows "finite {F. F face_of S}"
1.1308 @@ -2459,29 +2459,29 @@
1.1309      by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
1.1310  qed
1.1311
1.1312 -lemma finite_polyhedron_exposed_faces:
1.1313 +lemma%unimportant finite_polyhedron_exposed_faces:
1.1314     "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
1.1315  using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
1.1316
1.1317 -lemma finite_polyhedron_extreme_points:
1.1318 +lemma%unimportant finite_polyhedron_extreme_points:
1.1319    fixes S :: "'a :: euclidean_space set"
1.1320    shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
1.1321  apply (simp add: face_of_singleton [symmetric])
1.1322  apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
1.1323  done
1.1324
1.1325 -lemma finite_polyhedron_facets:
1.1326 +lemma%unimportant finite_polyhedron_facets:
1.1327    fixes S :: "'a :: euclidean_space set"
1.1328    shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
1.1329  unfolding facet_of_def
1.1330  by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
1.1331
1.1332
1.1333 -proposition rel_interior_of_polyhedron:
1.1334 +proposition%important rel_interior_of_polyhedron:
1.1335    fixes S :: "'a :: euclidean_space set"
1.1336    assumes "polyhedron S"
1.1337      shows "rel_interior S = S - \<Union>{F. F facet_of S}"
1.1338 -proof -
1.1339 +proof%unimportant -
1.1340    obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
1.1341               and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
1.1342               and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
1.1343 @@ -2521,19 +2521,19 @@
1.1344      by (force simp: rel)
1.1345  qed
1.1346
1.1347 -lemma rel_boundary_of_polyhedron:
1.1348 +lemma%unimportant rel_boundary_of_polyhedron:
1.1349    fixes S :: "'a :: euclidean_space set"
1.1350    assumes "polyhedron S"
1.1351      shows "S - rel_interior S = \<Union> {F. F facet_of S}"
1.1352  using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
1.1353
1.1354 -lemma rel_frontier_of_polyhedron:
1.1355 +lemma%unimportant rel_frontier_of_polyhedron:
1.1356    fixes S :: "'a :: euclidean_space set"
1.1357    assumes "polyhedron S"
1.1358      shows "rel_frontier S = \<Union> {F. F facet_of S}"
1.1359  by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
1.1360
1.1361 -lemma rel_frontier_of_polyhedron_alt:
1.1362 +lemma%unimportant rel_frontier_of_polyhedron_alt:
1.1363    fixes S :: "'a :: euclidean_space set"
1.1364    assumes "polyhedron S"
1.1365      shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
1.1366 @@ -2544,11 +2544,11 @@
1.1367
1.1368  text\<open>A characterization of polyhedra as having finitely many faces\<close>
1.1369
1.1370 -proposition polyhedron_eq_finite_exposed_faces:
1.1371 +proposition%important polyhedron_eq_finite_exposed_faces:
1.1372    fixes S :: "'a :: euclidean_space set"
1.1373    shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
1.1374           (is "?lhs = ?rhs")
1.1375 -proof
1.1376 +proof%unimportant
1.1377    assume ?lhs
1.1378    then show ?rhs
1.1379      by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
1.1380 @@ -2635,11 +2635,11 @@
1.1381    qed
1.1382  qed
1.1383
1.1384 -corollary polyhedron_eq_finite_faces:
1.1385 +corollary%important polyhedron_eq_finite_faces:
1.1386    fixes S :: "'a :: euclidean_space set"
1.1387    shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
1.1388           (is "?lhs = ?rhs")
1.1389 -proof
1.1390 +proof%unimportant
1.1391    assume ?lhs
1.1392    then show ?rhs
1.1393      by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
1.1394 @@ -2649,7 +2649,7 @@
1.1395      by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
1.1396  qed
1.1397
1.1398 -lemma polyhedron_linear_image_eq:
1.1399 +lemma%unimportant polyhedron_linear_image_eq:
1.1400    fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
1.1401    assumes "linear h" "bij h"
1.1402      shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
1.1403 @@ -2669,19 +2669,19 @@
1.1404      done
1.1405  qed
1.1406
1.1407 -lemma polyhedron_negations:
1.1408 +lemma%unimportant polyhedron_negations:
1.1409    fixes S :: "'a :: euclidean_space set"
1.1410    shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
1.1411    by (subst polyhedron_linear_image_eq)
1.1412      (auto simp: bij_uminus intro!: linear_uminus)
1.1413
1.1414 -subsection\<open>Relation between polytopes and polyhedra\<close>
1.1415 -
1.1416 -lemma polytope_eq_bounded_polyhedron:
1.1417 +subsection%important\<open>Relation between polytopes and polyhedra\<close>
1.1418 +
1.1419 +lemma%important polytope_eq_bounded_polyhedron:
1.1420    fixes S :: "'a :: euclidean_space set"
1.1421    shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
1.1422           (is "?lhs = ?rhs")
1.1423 -proof
1.1424 +proof%unimportant
1.1425    assume ?lhs
1.1426    then show ?rhs
1.1427      by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
1.1428 @@ -2694,28 +2694,28 @@
1.1429      done
1.1430  qed
1.1431
1.1432 -lemma polytope_Int:
1.1433 +lemma%unimportant polytope_Int:
1.1434    fixes S :: "'a :: euclidean_space set"
1.1435    shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
1.1436  by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
1.1437
1.1438
1.1439 -lemma polytope_Int_polyhedron:
1.1440 +lemma%important polytope_Int_polyhedron:
1.1441    fixes S :: "'a :: euclidean_space set"
1.1442    shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
1.1443 -by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
1.1444 -
1.1445 -lemma polyhedron_Int_polytope:
1.1446 +by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
1.1447 +
1.1448 +lemma%important polyhedron_Int_polytope:
1.1449    fixes S :: "'a :: euclidean_space set"
1.1450    shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
1.1451 -by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
1.1452 -
1.1453 -lemma polytope_imp_polyhedron:
1.1454 +by%unimportant (simp add: bounded_Int polytope_eq_bounded_polyhedron)
1.1455 +
1.1456 +lemma%important polytope_imp_polyhedron:
1.1457    fixes S :: "'a :: euclidean_space set"
1.1458    shows "polytope S \<Longrightarrow> polyhedron S"
1.1460 -
1.1461 -lemma polytope_facet_exists:
1.1463 +
1.1464 +lemma%unimportant polytope_facet_exists:
1.1465    fixes p :: "'a :: euclidean_space set"
1.1466    assumes "polytope p" "0 < aff_dim p"
1.1467    obtains F where "F facet_of p"
1.1468 @@ -2732,16 +2732,16 @@
1.1469         all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
1.1470  qed
1.1471
1.1472 -lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
1.1473 +lemma%unimportant polyhedron_interval [iff]: "polyhedron(cbox a b)"
1.1474  by (metis polytope_imp_polyhedron polytope_interval)
1.1475
1.1476 -lemma polyhedron_convex_hull:
1.1477 +lemma%unimportant polyhedron_convex_hull:
1.1478    fixes S :: "'a :: euclidean_space set"
1.1479    shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
1.1480  by (simp add: polytope_convex_hull polytope_imp_polyhedron)
1.1481
1.1482
1.1483 -subsection\<open>Relative and absolute frontier of a polytope\<close>
1.1484 +subsection%important\<open>Relative and absolute frontier of a polytope\<close>
1.1485
1.1486  lemma rel_boundary_of_convex_hull:
1.1487      fixes S :: "'a::euclidean_space set"
1.1488 @@ -3194,9 +3194,9 @@
1.1489    qed (use C in auto)
1.1490  qed
1.1491
1.1492 -subsection\<open>Simplicial complexes and triangulations\<close>
1.1493 -
1.1494 -definition simplicial_complex where
1.1495 +subsection%important \<open>Simplicial complexes and triangulations\<close>
1.1496 +
1.1497 +definition%important simplicial_complex where
1.1498   "simplicial_complex \<C> \<equiv>
1.1499          finite \<C> \<and>
1.1500          (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
1.1501 @@ -3204,7 +3204,7 @@
1.1502          (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
1.1503                  \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
1.1504
1.1505 -definition triangulation where
1.1506 +definition%important triangulation where
1.1507   "triangulation \<T> \<equiv>
1.1508          finite \<T> \<and>
1.1509          (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
1.1510 @@ -3212,9 +3212,9 @@
1.1511                  \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
1.1512
1.1513
1.1514 -subsection\<open>Refining a cell complex to a simplicial complex\<close>
1.1515 -
1.1516 -lemma convex_hull_insert_Int_eq:
1.1517 +subsection%important\<open>Refining a cell complex to a simplicial complex\<close>
1.1518 +
1.1519 +lemma%important convex_hull_insert_Int_eq:
1.1520    fixes z :: "'a :: euclidean_space"
1.1521    assumes z: "z \<in> rel_interior S"
1.1522        and T: "T \<subseteq> rel_frontier S"
1.1523 @@ -3222,7 +3222,7 @@
1.1524        and "convex S" "convex T" "convex U"
1.1525    shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
1.1526      (is "?lhs = ?rhs")
1.1527 -proof
1.1528 +proof%unimportant
1.1529    show "?lhs \<subseteq> ?rhs"
1.1530    proof (cases "T={} \<or> U={}")
1.1531      case True then show ?thesis by auto
1.1532 @@ -3294,7 +3294,7 @@
1.1533      by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
1.1534  qed
1.1535
1.1536 -lemma simplicial_subdivision_aux:
1.1537 +lemma%important simplicial_subdivision_aux:
1.1538    assumes "finite \<M>"
1.1539        and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1540        and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
1.1541 @@ -3306,7 +3306,7 @@
1.1542                  (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
1.1543                  (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
1.1544    using assms
1.1545 -proof (induction n arbitrary: \<M> rule: less_induct)
1.1546 +proof%unimportant (induction n arbitrary: \<M> rule: less_induct)
1.1547    case (less n)
1.1548    then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1549        and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
1.1550 @@ -3756,7 +3756,7 @@
1.1551  qed
1.1552
1.1553
1.1554 -lemma simplicial_subdivision_of_cell_complex_lowdim:
1.1555 +lemma%important simplicial_subdivision_of_cell_complex_lowdim:
1.1556    assumes "finite \<M>"
1.1557        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1558        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
1.1559 @@ -3765,7 +3765,7 @@
1.1560                    "\<Union>\<T> = \<Union>\<M>"
1.1561                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
1.1562                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
1.1563 -proof (cases "d \<ge> 0")
1.1564 +proof%unimportant (cases "d \<ge> 0")
1.1565    case True
1.1566    then obtain n where n: "d = of_nat n"
1.1567      using zero_le_imp_eq_int by blast
1.1568 @@ -3822,7 +3822,7 @@
1.1569    qed auto
1.1570  qed
1.1571
1.1572 -proposition simplicial_subdivision_of_cell_complex:
1.1573 +proposition%important simplicial_subdivision_of_cell_complex:
1.1574    assumes "finite \<M>"
1.1575        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1576        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
1.1577 @@ -3830,9 +3830,9 @@
1.1578                    "\<Union>\<T> = \<Union>\<M>"
1.1579                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
1.1580                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
1.1581 -  by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
1.1582 -
1.1583 -corollary fine_simplicial_subdivision_of_cell_complex:
1.1584 +  by%unimportant (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
1.1585 +
1.1586 +corollary%important fine_simplicial_subdivision_of_cell_complex:
1.1587    assumes "0 < e" "finite \<M>"
1.1588        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1589        and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
1.1590 @@ -3841,7 +3841,7 @@
1.1591                    "\<Union>\<T> = \<Union>\<M>"
1.1592                    "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
1.1593                    "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
1.1594 -proof -
1.1595 +proof%unimportant -
1.1596    obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>"
1.1597                and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
1.1598                 and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
1.1599 @@ -3880,13 +3880,13 @@
1.1600    qed
1.1601  qed
1.1602
1.1603 -subsection\<open>Some results on cell division with full-dimensional cells only\<close>
1.1604 -
1.1605 -lemma convex_Union_fulldim_cells:
1.1606 +subsection%important\<open>Some results on cell division with full-dimensional cells only\<close>
1.1607 +
1.1608 +lemma%important convex_Union_fulldim_cells:
1.1609    assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
1.1610        and eq: "\<Union>\<S> = U"and  "convex U"
1.1611   shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
1.1612 -proof -
1.1613 +proof%unimportant -
1.1614    have "closed U"
1.1615      using \<open>finite \<S>\<close> clo eq by blast
1.1616    have "?lhs \<subseteq> U"
1.1617 @@ -3935,7 +3935,7 @@
1.1618    ultimately show ?thesis by blast
1.1619  qed
1.1620
1.1621 -proposition fine_triangular_subdivision_of_cell_complex:
1.1622 +proposition%important fine_triangular_subdivision_of_cell_complex:
1.1623    assumes "0 < e" "finite \<M>"
1.1624        and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
1.1625        and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
1.1626 @@ -3944,7 +3944,7 @@
1.1627                   "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
1.1628                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
1.1629                   "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
1.1630 -proof -
1.1631 +proof%unimportant -
1.1632    obtain \<T> where "simplicial_complex \<T>"
1.1633               and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
1.1634               and "\<Union>\<T> = \<Union>\<M>"
```