src/HOL/Analysis/Polytope.thy
changeset 68074 8d50467f7555
parent 68073 fad29d2a17a5
child 68833 fde093888c16
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Thu May 03 15:07:14 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu May 03 16:17:44 2018 +0200
     1.3 @@ -1188,7 +1188,7 @@
     1.4      qed
     1.5      then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
     1.6        by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
     1.7 -           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_superset)
     1.8 +           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_base)
     1.9      then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
    1.10        by (rule less.IH) (auto simp: co less.prems)
    1.11      then show ?thesis