Commit 2020-06-04 18:38 2ceb7f7f

feat(analysis/convex): preparatory statement for caratheodory (#2944) Proves

lemma convex_hull_eq_union_convex_hull_finite_subsets (s : set E) :
  convex_hull s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull ↑t