mathlib

c38ab356 - feat(analysis/convex/combination): The convex hull of `s + t` (#14160)

feat(analysis/convex/combination): The convex hull of `s + t` (#14160) `convex_hull` distributes over pointwise addition of sets and commutes with pointwise scalar multiplication. Also delete `linear_map.image_convex_hull` because it duplicates `linear_map.convex_hull_image`.