--- a/src/HOL/Analysis/Convex.thy Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Tue Nov 05 21:07:03 2019 +0100
@@ -14,7 +14,7 @@
"HOL-Library.Set_Algebras"
begin
-subsection \<open>Convexity\<close>
+subsection \<open>Convex Sets\<close>
definition\<^marker>\<open>tag important\<close> convex :: "'a::real_vector set \<Rightarrow> bool"
where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
@@ -340,7 +340,7 @@
done
-subsection \<open>Functions that are convex on a set\<close>
+subsection \<open>Convex Functions on a Set\<close>
definition\<^marker>\<open>tag important\<close> convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
where "convex_on s f \<longleftrightarrow>
@@ -1865,7 +1865,7 @@
qed
-subsection \<open>Affine dependence and consequential theorems\<close>
+subsection \<open>Affine Dependence\<close>
text "Formalized by Lars Schewe."