mathlib3

7c9a8113 - feat(analysis/convex/basic): missing lemmas (#7946)

feat(analysis/convex/basic): missing lemmas (#7946) - the union of a set/indexed family of convex sets is convex - `open_segment a b` is convex - a set is nonempty iff its convex hull is