Define convex_hull

[urkud]

Define convex_hull s as

def convex_hull (s : set E) = ⋂₀ {t : set E | s ⊆ t ∧ convex t}

and prove that every element of convex_hull s is a center of mass of some points from s. The proof should probably include some lemma stating that a center of mass of a collection of center of masses is a center of mass with appropriate weights.

It might make sense to also define center of mass for multiset (E × ℝ), and rewrite the old definition using some map. This way we can avoid introducing an extra type just to avoid duplicates.