src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 68607 67bb59e49834
parent 68527 2f4e2aab190a
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -2005,9 +2005,9 @@
     1.4    shows "c *\<^sub>R x \<in> cone hull S"
     1.5    by (metis assms cone_cone_hull hull_inc mem_cone)
     1.6  
     1.7 -proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
     1.8 +proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
     1.9    (is "?lhs = ?rhs")
    1.10 -proof%unimportant -
    1.11 +proof -
    1.12    {
    1.13      fix x
    1.14      assume "x \<in> ?rhs"
    1.15 @@ -2089,7 +2089,7 @@
    1.16     "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
    1.17  by (meson Diff_subset affine_dependent_subset)
    1.18  
    1.19 -proposition%important affine_dependent_explicit:
    1.20 +proposition affine_dependent_explicit:
    1.21    "affine_dependent p \<longleftrightarrow>
    1.22      (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
    1.23  proof -
    1.24 @@ -2524,7 +2524,7 @@
    1.25  
    1.26  subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
    1.27  
    1.28 -proposition%important convex_hull_indexed:
    1.29 +proposition convex_hull_indexed:
    1.30    fixes S :: "'a::real_vector set"
    1.31    shows "convex hull S =
    1.32      {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
    1.33 @@ -4020,11 +4020,11 @@
    1.34      by (auto simp: convex_hull_explicit)
    1.35  qed
    1.36  
    1.37 -theorem%important caratheodory:
    1.38 +theorem caratheodory:
    1.39    "convex hull p =
    1.40      {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
    1.41        card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
    1.42 -proof%unimportant safe
    1.43 +proof safe
    1.44    fix x
    1.45    assume "x \<in> convex hull p"
    1.46    then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
    1.47 @@ -5871,10 +5871,10 @@
    1.48      done
    1.49  qed
    1.50  
    1.51 -theorem%important radon:
    1.52 +theorem radon:
    1.53    assumes "affine_dependent c"
    1.54    obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
    1.55 -proof%unimportant -
    1.56 +proof -
    1.57    from assms[unfolded affine_dependent_explicit]
    1.58    obtain s u where
    1.59        "finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
    1.60 @@ -5965,12 +5965,12 @@
    1.61    qed 
    1.62  qed
    1.63  
    1.64 -theorem%important helly:
    1.65 +theorem helly:
    1.66    fixes f :: "'a::euclidean_space set set"
    1.67    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
    1.68      and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
    1.69    shows "\<Inter>f \<noteq> {}"
    1.70 -  apply%unimportant (rule helly_induct)
    1.71 +  apply (rule helly_induct)
    1.72    using assms
    1.73    apply auto
    1.74    done